Quantitative verification: models techniques and tools

11 years 5 months ago
Quantitative verification: models techniques and tools
Automated verification is a technique for establishing if certain properties, usually expressed in temporal logic, hold for a system model. The model can be defined using a high-level formalism or extracted directly from software using methods such as abstract interpretation. The verification proceeds through exhaustive exploration of the state-transition graph of the model and is therefore more powerful than testing. Quantitative verification is an analogous technique for establishing quantitative properties of a system model, such as the probability of battery power dropping below minimum, the expected time for message delivery and the expected number of messages lost before protocol termination. Models analysed through this method are typically variants of Markov chains, annotated with costs and rewards that describe resources and their usage during execution. Properties are expressed in temporal logic extended with probabilistic and reward operators. Quantitative verification invo...
Marta Z. Kwiatkowska
Added 20 Nov 2009
Updated 20 Nov 2009
Type Conference
Year 2007
Authors Marta Z. Kwiatkowska
Comments (0)