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

BMC Bioinformatics. 2009;10(1):450 DOI 10.1186/1471-2105-10-450


Journal Homepage

Journal Title: BMC Bioinformatics

ISSN: 1471-2105 (Online)

Publisher: BMC

LCC Subject Category: Medicine: Medicine (General): Computer applications to medicine. Medical informatics | Science: Biology (General)

Country of publisher: United Kingdom

Language of fulltext: English

Full-text formats available: PDF, HTML



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


Blind peer review

Editorial Board

Instructions for authors

Time From Submission to Publication: 19 weeks


Abstract | Full Text

<p>Abstract</p> <p>Background</p> <p>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.</p> <p>Results</p> <p>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 G<smcaps>NA</smcaps> and the model checkers N<smcaps>U</smcaps>SMV and C<smcaps>ADP</smcaps>. G<smcaps>NA</smcaps> 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.</p> <p>Conclusions</p> <p>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 <it>E. coli</it>. 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.</p>