Abstract
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 language | English |
|---|---|
| Pages (from-to) | 107-125 |
| Number of pages | 19 |
| Journal | IEEE Transactions on Reliability |
| Volume | 65 |
| Issue number | 1 |
| Early online date | 4 Aug 2015 |
| DOIs | |
| Publication status | E-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 detailsKeywords
- Markov chains
- Software systems
- probabilistic model checking
- quality-of-service requirements
- quantitative verification
