title: A service-oriented architecture for integrating the modeling and formal verification of genetic regulatory networks.
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.
authors.affiliation: INRIA Grenoble-Rhône-Alpes, 655 Avenue de l'Europe, Montbonnot, 38334 St Ismier Cedex, France. Pedro.Monteiro@inria.fr
authors.forename: Pedro T
authors.initials: PT
authors.lastname: Monteiro
authors.forename: Estelle
authors.initials: E
authors.lastname: Dumas
authors.forename: Bruno
authors.initials: B
authors.lastname: Besson
authors.forename: Radu
authors.initials: R
authors.lastname: Mateescu
authors.forename: Michel
authors.initials: M
authors.lastname: Page
authors.forename: Ana T
authors.initials: AT
authors.lastname: Freitas
authors.forename: Hidde
authors.initials: H
authors.lastname: de Jong
mesh_terms: D019295:Computational Biology / Q000379:methods*; D030541:Databases, Genetic; D053263:Gene Regulatory Networks / Q000235:genetics*; D012984:Software; D014584:User-Computer Interface