Department of Computer Science, University of Sheffield, Sheffield, UK.
School of Electrical Engineering & Computer Science, University of Bradford, Bradford, UK.
Bioinformatics. 2018 Sep 15;34(18):3187-3195. doi: 10.1093/bioinformatics/bty282.
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.
形式验证是一种计算方法，用于检查系统的正确性（与所需功能有关）。它已被广泛应用于工程应用中，以验证系统是否正常工作。模型检查是一种验证算法，用于检查系统模型是否满足其需求规范。这种方法已被应用于许多系统和合成生物学以及系统医学中的模型。然而，模型检查在计算上非常昂贵，并且不能扩展到大型模型和系统。因此，引入了统计模型检查（SMC）来解决这一缺点，SMC 放宽了模型检查的一些约束。已经开发了几种 SMC 工具；但是，每个工具的性能根据所讨论的系统模型和要验证的需求类型而有很大差异。这使得很难事先知道对于给定的模型和需求应该使用哪个工具，因为为任何生物应用选择最有效的工具都需要一定程度的计算专业知识，而生物学实验室通常不具备这种知识。本文的目的是介绍一种方法，并提供一个工具，用于自动选择最适合感兴趣系统的模型检查器。
我们提供了一个系统，可以自动预测给定生物模型的最快模型检查工具。我们的结果表明，可以进行高度置信度的预测，准确率超过 90%。这意味着在验证时间方面可以获得显著的性能提升，并大大降低了生物学家长期以来面临的“可用性障碍”，使他们能够获得这种强大的计算技术。
SMC Predictor 工具可在 http://www.smcpredictor.com 上获得。
补充数据可在 Bioinformatics 在线获得。
