Model checking is a formal verification technique which is widely used in different
areas for automated verification and analysis. In this study, we applied a Model
Checking method to a biological system. Firstly we constructed a single-cell,
Boolean network model for the signaling pathways of apoptosis (programmed cell
death) in lung cancers by combining the intrinsic and extrinsic Apoptosis pathways,
p53 signaling pathway and p53 - DAP Kinase pathway in Lung cancers. We
translated this model to the NuSMV input language. Then we converted known
experimental results to CTL properties and checked the conformance of our model
with respect to biological experimental results. We examined the dynamics of the
apoptosis in lung cancer using NuSMV symbolic model checker and identified the
relationship between apoptosis and lung cancer. Finally we generalized the whole
process by introducing translation rules and CTL property patterns for biological
queries so that model checking any signaling pathway can be automated.
| Identifer | oai:union.ndltd.org:METU/oai:etd.lib.metu.edu.tr:http://etd.lib.metu.edu.tr/upload/12613808/index.pdf |
| Date | 01 October 2011 |
| Creators | Parlak, Mehtap Ayfer |
| Contributors | Betin Can, Aysu |
| Publisher | METU |
| Source Sets | Middle East Technical Univ. |
| Language | English |
| Detected Language | English |
| Type | M.S. Thesis |
| Format | text/pdf |
| Rights | To liberate the content for METU campus |
Page generated in 0.0126 seconds