Skip to main page content
U.S. flag

An official website of the United States government

Dot gov

The .gov means it’s official.
Federal government websites often end in .gov or .mil. Before sharing sensitive information, make sure you’re on a federal government site.

Https

The site is secure.
The https:// ensures that you are connecting to the official website and that any information you provide is encrypted and transmitted securely.

Access keys NCBI Homepage MyNCBI Homepage Main Content Main Navigation
. 2009 Dec 30:10:450.
doi: 10.1186/1471-2105-10-450.

A service-oriented architecture for integrating the modeling and formal verification of genetic regulatory networks

Pedro T Monteiro  1 , Estelle Dumas, Bruno Besson, Radu Mateescu, Michel Page, Ana T Freitas, Hidde de Jong
Affiliations

A service-oriented architecture for integrating the modeling and formal verification of genetic regulatory networks

Pedro T Monteiro et al. BMC Bioinformatics. .

Abstract

Background: The study of biological networks has led to the development of increasingly large and detailed models. Computer tools are essential for the simulation of the dynamical behavior of the networks from the model. However, as the size of the models grows, it becomes infeasible to manually verify the predictions against experimental data or identify interesting features in a large number of simulation traces. Formal verification based on temporal logic and model checking provides promising methods to automate and scale the analysis of the models. However, a framework that tightly integrates modeling and simulation tools with model checkers is currently missing, on both the conceptual and the implementational level.

Results: We have developed a generic and modular web service, based on a service-oriented architecture, for integrating the modeling and formal verification of genetic regulatory networks. The architecture has been implemented in the context of the qualitative modeling and simulation tool GNA and the model checkers NUSMV and CADP. GNA has been extended with a verification module for the specification and checking of biological properties. The verification module also allows the display and visual inspection of the verification results.

Conclusions: The practical use of the proposed web service is illustrated by means of a scenario involving the analysis of a qualitative model of the carbon starvation response in E. coli. The service-oriented architecture allows modelers to define the model and proceed with the specification and formal verification of the biological properties by means of a unified graphical user interface. This guarantees a transparent access to formal verification technology for modelers of genetic regulatory networks.

PubMed Disclaimer

Figures

Figure 1
Figure 1
Service-oriented architecture. Service-oriented architecture for the integration of tools for the modeling and simulation of genetic regulatory networks with formal verification (FV) tools. In particular, the architecture has been implemented for the connection of GNA with the model checkers NUSMV and CADP. GNA is extended with a verification module responsible for the transformation of the model and properties into a format specific to a formal verification tool, and for the communication with the other components of the service-oriented architecture.
Figure 2
Figure 2
Pattern-based property editor. Graphical user interface for the specification of biological properties. The modeler can use a pattern-based property editor for frequently-asked questions, and a text editor for the specification of more complex biological properties (expert mode).
Figure 3
Figure 3
Carbon starvation response network in E. coli. Network of key genes, proteins and regulatory interactions involved in the carbon starvation response network in E. coli [37,38].
Figure 4
Figure 4
Verification result. Result of the verification of the biological property specified in Figure 3, consisting of a false verdict and the corresponding counterexample composed of a subgraph of the FSTS (see left panel). The qualitative evolution of the concentration variables of the selected states of the counterexample is visualized (see right panel).
See this image and copyright information in PMC

References

    1. Jamshidi N, Palsson B. Formulating genome-scale kinetic models in the post-genome era. Mol Syst Biol. 2008;4(171) - PMC - PubMed
    1. Chen WW, Schoeberl B, Jasper PJ, Niepel M, Nielsen UB, Lauffenburger DA, Sorger PK. Input-output behavior of ErbB signaling pathways as revealed by a mass action model trained against dynamic data. Mol Syst Biol. 2009;5(239) - PMC - PubMed
    1. Chen KC, Calzone L, Csikasz-Nagy A, Cross FR, Novak B, Tyson JJ. Integrative analysis of cell cycle control in budding yeast. Mol Biol Cell. 2004;15(8):3841–3862. doi: 10.1091/mbc.E03-11-0794. - DOI - PMC - PubMed
    1. Forger DB, Peskin CS. A detailed predictive model of the mammalian circadian clock. Proc Natl Acad Sci USA. 2003;100(25):14806–14811. doi: 10.1073/pnas.2036281100. - DOI - PMC - PubMed
    1. Klipp E, Nordlander B, Krüger R, Gennemark P, Hohmann S. Integrative model of the response of yeast to osmotic shock. Nat Biotechnol. 2005;23(8):975–982. doi: 10.1038/nbt1114. - DOI - PubMed

Publication types

LinkOut - more resources