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.

Calinescu, R., Ghezzi, C., Johnson, K., Pezze', M., Rafiq, Y., Tamburrelli, G. (2016). Formal Verification with Confidence Intervals to Establish Quality of Service Properties of Software Systems. IEEE TRANSACTIONS ON RELIABILITY, 65(1), 107-125 [10.1109/TR.2015.2452931].

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

PEZZE', MAURO;
2016

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.
Articolo in rivista - Articolo scientifico
Markov chains; probabilistic model checking; quality-of-service requirements; quantitative verification; Software systems;
Quality of Service, Formal Methods, Confidence intrval
English
2016
2016
65
1
107
125
7177126
reserved
Calinescu, R., Ghezzi, C., Johnson, K., Pezze', M., Rafiq, Y., Tamburrelli, G. (2016). Formal Verification with Confidence Intervals to Establish Quality of Service Properties of Software Systems. IEEE TRANSACTIONS ON RELIABILITY, 65(1), 107-125 [10.1109/TR.2015.2452931].
File in questo prodotto:
File Dimensione Formato  
07177126.pdf

Solo gestori archivio

Tipologia di allegato: Publisher’s Version (Version of Record, VoR)
Dimensione 2.8 MB
Formato Adobe PDF
2.8 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/172065
Citazioni
  • Scopus 51
  • ???jsp.display-item.citation.isi??? 44
Social impact