Skip to Main content Skip to Navigation
Conference papers

A Framework for Verification of Software with Time and Probabilities

Abstract : 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, 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 abstractions 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [45 references]  Display  Hide  Download

https://hal.inria.fr/hal-00767473
Contributor : Hongyang Qu Connect in order to contact the contributor
Submitted on : Wednesday, December 19, 2012 - 10:47:29 PM
Last modification on : Wednesday, November 25, 2020 - 5:06:03 PM
Long-term archiving on: : Wednesday, March 20, 2013 - 11:38:24 AM

File

formats10inv.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00767473, version 1

Collections

Citation

Marta Kwiatkowska, Gethin Norman, David Parker. A Framework for Verification of Software with Time and Probabilities. 8th International Conference on Formal Modelling and Analysis of Timed Systems, Sep 2010, Klosterneuburg, Austria. pp.25-45. ⟨hal-00767473⟩

Share

Metrics

Record views

137

Files downloads

314