YAGA: Automated Analysis of Quantitative Safety Specifications in Probabilistic B

Probabilistic B (pB) [2, 8] extends classical B [7] to incorporate probabilistic updates together with the specification of quantitative safety properties. As for classical B, probabilistic B formulates safety as inductive invariants which can be checked mechanically relative to the program code. In the case that the invariants cannot be shown to be inductive, classical B uses model checking to allow experimental investigation, returning a counterexample execution trace in the case that the safety condition is violated. In this paper we introduce YAGA which provides similar support for probabilistic B and quantitative safety specifications. YAGA automatically interprets quantitative safety and the pB machine as a model checking problem to investigate the presence of counterexamples. Since inductive invariants characterise a strong form of safety, we are able to identify the specific point at which failure occurs as individual counterexample traces, which can then be ranked for importan...

• Type: Conference
• Year: 2010
• Where: ATVA
• Authors: Ukachukwu Ndukwu, A. K. McIver
• Keywords: ATVA 2010, Hardware, Inductive Invariants, Probabilistic, Quantitative Safety