Formal Verification with Confidence Intervals to Establish Quality of Service Properties of Software Systems

Radu Calinescu, Carlo Ghezzi, Kenneth Harold Anthony Johnson, Mauro Pezze, Yasmeen Rafiq, Giordano Tamburrelli

Research output: Contribution to journalArticlepeer-review


Formal verification is used to establish the compliance of software and hardware systems with important classes of requirements. System compliance with functional requirements is frequently analyzed using techniques such as model checking, and theorem proving. In addition, a technique called quantitative verification supports the analysis of the reliability, performance, and other quality-of-service (QoS) properties of systems that exhibit stochastic behavior. In this paper, we extend the applicability of quantitative verification to the common scenario when the probabilities of transition between some or all states of the Markov models analyzed by the technique are unknown, but observations of these transitions are available. To this end, we introduce a theoretical framework, and a tool chain that establish confidence intervals for the QoS properties of a software system modelled as a Markov chain with uncertain transition probabilities. We use two case studies from different application domains to assess the effectiveness of the new quantitative verification technique. Our experiments show that disregarding the above source of uncertainty may significantly affect the accuracy of the verification results, leading to wrong decisions, and low-quality software systems.

Original languageEnglish
Pages (from-to)107-125
Number of pages19
JournalIEEE Transactions on Reliability
Issue number1
Early online date4 Aug 2015
Publication statusE-pub ahead of print - 4 Aug 2015

Bibliographical note

© 2015, IEEE. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details


  • Markov chains
  • Software systems
  • probabilistic model checking
  • quality-of-service requirements
  • quantitative verification

Cite this