A framework for verification of software with time and probabilities

Abstract. Quantitative verification techniques are able to establish sys-tem properties such as “the probability of an airbag failing to deploy on demand ” or “the expected time for a network protocol to success-fully send a message packet”. In this paper, we describe a framework for quantitative verification of software that exhibits both real-time and probabilistic behaviour. The complexity of real software, combined with the need to capture precise timing information, necessitates the use of abstraction techniques. We outline a quantitative abstraction refinement approach, which can be used to automatically construct and analyse ab-stractions of probabilistic, real-time programs. As a concrete example of the potential applicability of our framework, we discuss the challenges involved in applying it to the quantitative verification of SystemC, an increasingly popular system-level modelling language.