Cargando…

Automatic selection of verification tools for efficient analysis of biochemical models

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...

Descripción completa

Detalles Bibliográficos
Autores principales: Bakir, Mehmet Emin, Konur, Savas, Gheorghe, Marian, Krasnogor, Natalio, Stannett, Mike
Formato: Online Artículo Texto
Lenguaje:English
Publicado: Oxford University Press 2018
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6137970/
https://www.ncbi.nlm.nih.gov/pubmed/29688313
http://dx.doi.org/10.1093/bioinformatics/bty282
_version_ 1783355267630497792
author Bakir, Mehmet Emin
Konur, Savas
Gheorghe, Marian
Krasnogor, Natalio
Stannett, Mike
author_facet Bakir, Mehmet Emin
Konur, Savas
Gheorghe, Marian
Krasnogor, Natalio
Stannett, Mike
author_sort Bakir, Mehmet Emin
collection PubMed
description 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.
format Online
Article
Text
id pubmed-6137970
institution National Center for Biotechnology Information
language English
publishDate 2018
publisher Oxford University Press
record_format MEDLINE/PubMed
spelling pubmed-61379702018-09-24 Automatic selection of verification tools for efficient analysis of biochemical models Bakir, Mehmet Emin Konur, Savas Gheorghe, Marian Krasnogor, Natalio Stannett, Mike Bioinformatics Original Papers 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. Oxford University Press 2018-09-15 2018-04-24 /pmc/articles/PMC6137970/ /pubmed/29688313 http://dx.doi.org/10.1093/bioinformatics/bty282 Text en © The Author(s) 2018. Published by Oxford University Press. http://creativecommons.org/licenses/by-nc/4.0/ This is an Open Access article distributed under the terms of the Creative Commons Attribution Non-Commercial License (http://creativecommons.org/licenses/by-nc/4.0/), which permits non-commercial re-use, distribution, and reproduction in any medium, provided the original work is properly cited. For commercial re-use, please contact journals.permissions@oup.com
spellingShingle Original Papers
Bakir, Mehmet Emin
Konur, Savas
Gheorghe, Marian
Krasnogor, Natalio
Stannett, Mike
Automatic selection of verification tools for efficient analysis of biochemical models
title Automatic selection of verification tools for efficient analysis of biochemical models
title_full Automatic selection of verification tools for efficient analysis of biochemical models
title_fullStr Automatic selection of verification tools for efficient analysis of biochemical models
title_full_unstemmed Automatic selection of verification tools for efficient analysis of biochemical models
title_short Automatic selection of verification tools for efficient analysis of biochemical models
title_sort automatic selection of verification tools for efficient analysis of biochemical models
topic Original Papers
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6137970/
https://www.ncbi.nlm.nih.gov/pubmed/29688313
http://dx.doi.org/10.1093/bioinformatics/bty282
work_keys_str_mv AT bakirmehmetemin automaticselectionofverificationtoolsforefficientanalysisofbiochemicalmodels
AT konursavas automaticselectionofverificationtoolsforefficientanalysisofbiochemicalmodels
AT gheorghemarian automaticselectionofverificationtoolsforefficientanalysisofbiochemicalmodels
AT krasnogornatalio automaticselectionofverificationtoolsforefficientanalysisofbiochemicalmodels
AT stannettmike automaticselectionofverificationtoolsforefficientanalysisofbiochemicalmodels