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.

Supplementary information: Supplementary data are available at Bioinformatics online.

Fig. 1.

Computational time and feature importance. Average computational time and feature importance associated with model topological properties

Fig. 2.

Fastest SMC tools verifying each model against each property pattern. The X-axis represents logarithmic scale of model size; the Y-axis shows the property patterns. For each model a one-unit vertical line is drawn against each pattern. The line’s colour shows the fastest SMC

Fig. 3.

Performance comparison. For each property pattern, each tool performance is compared against the best performance. Here, X-axes represent the model size (species × reactions) in logarithmic scale (log₂), Y-axes show the relative performance of each SMC tool in comparison with the fastest one, and Z-axes show (log₁₀ scale) the consumed time in nanoseconds

Fig. 4.

Predictive accuracies. Accuracies (S1) for the fastest SMC prediction with different algorithms

Fig. 5.

Total time consumed for verifying all models

Fig. 6.

The mean performance loss when the best classifiers predict incorrectly