Model checking of apoptosis signaling pathways in lung cancers

Date

2011

Author

Parlak, Mehtap Ayfer

Metadata

Show full item record

Item Usage Stats

114
views

0
downloads

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.

Subject Keywords

Lungs

URI

hhttp://etd.lib.metu.edu.tr/upload/12613808/index.pdf
https://hdl.handle.net/11511/20815

Collections

Graduate School of Informatics, Thesis

Suggestions

OpenMETU
Core

Highly dependable concurrent programming using design for verification Betin Can, Aysu (2007-06-01) There has been significant progress in automated verification techniques based on model checking. However, scalable software model checking remains a challenging problem. We believe that this problem can be addressed using a design for verification approach based on design patterns that facilitate scalable automated verification. In this paper, we present a design for verification approach for highly dependable concurrent programming using a design pattern for concurrency controllers. A concurrency controll...
Scalable Software Model Checking Using Design for Verification TEVFİK, Bultan; Betin Can, Aysu (2005-11-13) There has been significant progress in automated verification techniques based on model checking. However, scalable software model checking remains a challenging problem. We believe that this problem can be addressed using a design for verification approach based on design patterns that facilitate scalable automated verification. We have been investigating a design for verification approach based on the following principles: 1) use of stateful, behavioral interfaces which isolate the behavior and enable mod...
Topic-centric querying of web information resources Altıngövde, İsmail Sengör; Ulusoy, O; Ozsoyoglu, G; Ozsoyoglu, ZM (2001-01-01) This paper deals with the problem of modeling web information resources using expert knowledge and personalized user information, and querying them in terms of topics and topic relationships. We propose a model for web information resources, and a query language SQL-TC (Topic-Centric SQL) to query the model. The model is composed of web-based information resources (XML or HTML documents on the web), expert advice repositories (domain-expert-specified metadata for information resources), and personalized inf...
New Distinguishers Based on Random Mappings against Stream Ciphers Turan, Meltem Sonmez; Calik, Cagdas; Saran, Nurdan Buz; Doğanaksoy, Ali (2008-09-18) Statistical randomness testing plays an important role in security analysis of cryptosystems. In this study, we aim to propose a new framework of randomness testing based on random mappings. Considering the probability distributions of coverage and P-lengths, we present three new distinguishers; (i) coverage test, (ii) p-test and (iii) DP-coverage test and applied them on Phase III Candidates of eSTREAM project. We experimentally observed some statistical weaknesses of Po-maranch using the coverage test.
Apply Quantitative Management Now TARHAN, AYÇA; Demirörs, Onur (Institute of Electrical and Electronics Engineers (IEEE), 2012-05-01) The Assessment Approach for Quantitative Process Management (A2QPM) helps identify software process measures for quantitative analysis even when organizations lack formal systems for process measurement. A2QPM is the first approach to quantitative management that offers software organizations a well-defined, detailed guideline for assessing their software processes and applying beneficial quantitative techniques to improve them. All the A2QPM applications we've described resulted in quantitative analysis im...

Citation Formats

M. A. Parlak, “Model checking of apoptosis signaling pathways in lung cancers,” M.S. - Master of Science, Middle East Technical University, 2011.