By the same authors

From the same journal

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

Research output: Contribution to journalArticle

Author(s)

Department/unit(s)

Publication details

JournalIEEE Transactions on Reliability
DateAccepted/In press - 30 Jun 2015
DateE-pub ahead of print (current) - 4 Aug 2015
Issue number1
Volume65
Number of pages19
Pages (from-to)107-125
Early online date4/08/15
Original languageEnglish

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.

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

    Research areas

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

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations