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...

• Type: Conference
• Year: 2007
• Where: SIGSOFT
• Authors: Marta Z. Kwiatkowska
• Keywords: Mechanical Verification, PRISM Model Checker, Quantitative Verification, SIGSOFT 2007, Software Engineering