Automatic selection of verification tools for efficient analysis of biochemical models.
Automatic selection of verification tools for efficient analysis of biochemical models.
复制标题
DOI：
10.1093/bioinformatics/bty282
复制
发表时间：
2018-09-15
期刊：
影响因子：
--
通讯作者：
Stannett M
中科院分区：
文献类型：
--
作者：
Bakir ME;Konur S;Gheorghe M;Krasnogor N;Stannett M
形式验证是一种检查系统正确性（与期望的功能相关）的计算方法。它已广泛应用于工程应用中，以验证系统是否正常工作。模型检查，一种验证的算法方法，检查系统模型是否满足其需求规范。这种方法已经应用于系统和合成生物学以及系统医学中的大量模型。然而，模型检查在计算上是非常昂贵的，并且不能扩展到大型模型和系统。因此，引入了统计模型检查（SMC）来解决这个缺点，它放宽了模型检查的一些约束。已经开发了几种SMC工具；然而，每个工具的性能根据所讨论的系统模型和被验证的需求类型有很大的不同。这使得我们很难先验地知道在给定的模型和需求中使用哪一种工具，因为为任何生物应用选择最有效的工具都需要相当程度的计算专业知识，而这在生物实验室中通常是不可能的。本文的目的是介绍一种方法，并提供一种工具，用于为感兴趣的系统自动选择最合适的模型检查器。我们提供了一个系统，可以自动预测最快的模型检查工具，为给定的生物模型。我们的结果表明，人们可以做出高可信度的预测，准确率超过90%。这意味着验证时间的显著性能提高，并大大降低了“可用性障碍”，使生物学家能够使用这种强大的计算技术。SMC预测工具可在http://www.smcpredictor.com上获得。补充数据可在生物信息学网站获得。
Formal verification is a computational approach that checks system correctness (in relation to a desired functionality). It has been widely used in engineering applications to verify that systems work correctly. Model checking, an algorithmic approach to verification, looks at whether a system model satisfies its requirements specification. This approach has been applied to a large number of models in systems and synthetic biology as well as in systems medicine. Model checking is, however, computationally very expensive, and is not scalable to large models and systems. Consequently, statistical model checking (SMC), which relaxes some of the constraints of model checking, has been introduced to address this drawback. Several SMC tools have been developed; however, the performance of each tool significantly varies according to the system model in question and the type of requirements being verified. This makes it hard to know, a priori, which one to use for a given model and requirement, as choosing the most efficient tool for any biological application requires a significant degree of computational expertise, not usually available in biology labs. The objective of this article is to introduce a method and provide a tool leading to the automatic selection of the most appropriate model checker for the system of interest. We provide a system that can automatically predict the fastest model checking tool for a given biological model. Our results show that one can make predictions of high confidence, with over 90% accuracy. This implies significant performance gain in verification time and substantially reduces the ‘usability barrier’ enabling biologists to have access to this powerful computational technology. SMC Predictor tool is available at http://www.smcpredictor.com. Supplementary data are available at Bioinformatics online.
登录
查看更多内容
影响因子：
--
作者：
Friedman, M
通讯作者：
Friedman, M
影响因子：
7.5
作者：
Geurts, P;Ernst, D;Wehenkel, L
通讯作者：
Wehenkel, L
DOI：
10.1007/978-1-61779-361-5_22
发表时间：
2012-01-01
期刊：
BACTERIAL MOLECULAR NETWORKS: METHODS AND PROTOCOLS
影响因子：
--
作者：
Batt, Gregory;Besson, Bruno;Ropers, Delphine
通讯作者：
Ropers, Delphine
影响因子：
1.1
作者：
Ciocchetta, Federica;Hillston, Jane
通讯作者：
Hillston, Jane
DOI：
10.1093/bioinformatics/btr571
发表时间：
2011-12-01
期刊：
Bioinformatics (Oxford, England)
影响因子：
--
作者：
Blakes J;Twycross J;Romero-Campero FJ;Krasnogor N
通讯作者：
Krasnogor N