Date Added: Sep 2010
Quantitative verification techniques are able to establish system properties such as "The probability of an airbag failing to deploy on demand" or "The expected time for a network protocol to successfully send a message packet". In this paper, the authors 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. They outline a quantitative abstraction refinement approach, which can be used to automatically construct and analyze abstractions of probabilistic, real-time programs.