INRIA Grenoble-Rhône-Alpes, 655 Avenue de l'Europe, Montbonnot, 38334 St Ismier Cedex, France.
BMC Bioinformatics. 2009 Dec 30;10:450. doi: 10.1186/1471-2105-10-450.
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.
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.
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.
生物网络的研究导致了越来越大且详细的模型的发展。计算机工具对于从模型模拟网络的动态行为至关重要。然而，随着模型规模的增长，手动验证对实验数据的预测或在大量模拟轨迹中识别有趣的特征变得不可行。基于时态逻辑和模型检查的形式验证提供了自动化和扩展模型分析的有希望的方法。然而，在概念和实现层面上，目前缺少一种将建模和模拟工具与模型检查器紧密集成的框架。
我们基于面向服务的架构开发了一种通用的和模块化的 Web 服务，用于集成遗传调控网络的建模和形式验证。该架构在定性建模和模拟工具 GNA 以及模型检查器 NUSMV 和 CADP 的上下文中实现。GNA 已通过用于规范和检查生物属性的验证模块进行了扩展。验证模块还允许显示和可视化检查验证结果。
通过涉及大肠杆菌碳饥饿反应的定性模型分析的场景，说明了所提出的 Web 服务的实际使用。面向服务的架构允许建模人员通过统一的图形用户界面定义模型，并继续规范和正式验证生物属性。这为遗传调控网络的建模人员提供了对形式验证技术的透明访问。
