Home // COMPUTATION TOOLS 2022, The Thirteenth International Conference on Computational Logics, Algebras, Programming, Tools, and Benchmarking // View article

Efficient Formal Verification with Confidence Intervals

Authors:
Naif Alasmari
Radu Calinescu

Keywords: confidence intervals; formal verification; non-functional software requirements; probabilistic model checking.

Abstract:
Formal verification with confidence intervals is a model checking technique that computes confidence intervals for parametric Markov model properties when observations of the unknown transition probabilities of these models are available. However, the high computational costs of the technique limit its scalability severely. To address this limitation, we introduce efficient formal verification with confidence intervals (eFACT), a model checking tool that enables the efficient analysis of parametric discrete-time Markov chains. eFACT supports the verification of reliability, performance, and other non-functional requirements for larger systems than currently possible. To that end, eFACT integrates recent advances in parametric model checking into a previous tool for formal verification with confidence intervals, and employs an efficient binary search technique to further speed up the determination of the highest confidence level at which a non-functional requirement can be deemed violated or satisfied.

Pages: 1 to 6

Copyright: Copyright (c) IARIA, 2022

Publication date: April 24, 2022

Published in: conference

ISSN: 2308-4170

ISBN: 978-1-61208-954-6

Location: Barcelona, Spain

Dates: from April 24, 2022 to April 28, 2022