Show/Hide Menu
Hide/Show Apps
Logout
Türkçe
Türkçe
Search
Search
Login
Login
OpenMETU
OpenMETU
About
About
Open Science Policy
Open Science Policy
Open Access Guideline
Open Access Guideline
Postgraduate Thesis Guideline
Postgraduate Thesis Guideline
Communities & Collections
Communities & Collections
Help
Help
Frequently Asked Questions
Frequently Asked Questions
Guides
Guides
Thesis submission
Thesis submission
MS without thesis term project submission
MS without thesis term project submission
Publication submission with DOI
Publication submission with DOI
Publication submission
Publication submission
Supporting Information
Supporting Information
General Information
General Information
Copyright, Embargo and License
Copyright, Embargo and License
Contact us
Contact us
Model checking of apoptosis signaling pathways in lung cancers
Date
2011
Author
Parlak, Mehtap Ayfer
Metadata
Show full item record
Item Usage Stats
160
views
0
downloads
Cite This
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
IEEE
ACM
APA
CHICAGO
MLA
BibTeX
M. A. Parlak, “Model checking of apoptosis signaling pathways in lung cancers,” M.S. - Master of Science, Middle East Technical University, 2011.