Title
Automatic selection of verification tools for efficient analysis of biochemical models.
Abstract
Motivation: 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. Results: 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. Availability and implementation: SMC Predictor tool is available at http://www.smcpredictor.com. Contact: mebakir1@sheffield.ac.uk Supplementary information: Supplementary data are available at Bioinformatics online.
Year
DOI
Venue
2018
10.1093/bioinformatics/bty282
BIOINFORMATICS
Field
DocType
Volume
Data mining,Model checking,Computer science,Correctness,Usability,Artificial intelligence,Statistical model,Software requirements specification,System model,Machine learning,Scalability,Formal verification
Journal
34
Issue
ISSN
Citations 
18
1367-4803
0
PageRank 
References 
Authors
0.34
9
5
Name
Order
Citations
PageRank
Mehmet E. Bakir1123.77
Savas Konur213113.40
Marian Gheorghe389374.31
Natalio Krasnogor4121385.53
Mike Stannett58319.67