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

Pedro Monteiro 1, 2, * Estelle Dumas 2, * Bruno Besson 2, * Radu Mateescu 3 Michel Page 2, 4, * Ana Freitas 1 Hidde De Jong 2, *
* Auteur correspondant
2 IBIS - Modeling, simulation, measurement, and control of bacterial regulatory networks
LAPM - Laboratoire Adaptation et pathogénie des micro-organismes [Grenoble], Inria Grenoble - Rhône-Alpes, Institut Jean Roget
3 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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.
Liste complète des métadonnées

https://hal.inria.fr/hal-00784446
Contributeur : Ed. Bmc <>
Soumis le : lundi 4 février 2013 - 13:11:03
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : lundi 17 juin 2013 - 18:45:49

Identifiants

Citation

Pedro Monteiro, Estelle Dumas, Bruno Besson, Radu Mateescu, Michel Page, et al.. A service-oriented architecture for integrating the modeling and formal verification of genetic regulatory networks. BMC Bioinformatics, BioMed Central, 2009, 10 (1), pp.450. 〈10.1186/1471-2105-10-450〉. 〈hal-00784446〉

Partager

Métriques

Consultations de la notice

771

Téléchargements de fichiers

600