YAGA

automated analysis of quantitative safety specifications in probabilistic B

Ukachukwu Ndukwu*, A. K. McIver

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

2 Citations (Scopus)

Abstract

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 importance, for example according to the probability of occurrence.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Proceedings
EditorsAhmed Bouajjani, Wei-Ngan Chin
Place of PublicationBerlin; Heidelberg
PublisherSpringer, Springer Nature
Pages378-386
Number of pages9
Volume6252 LNCS
ISBN (Print)3642156428, 9783642156427
DOIs
Publication statusPublished - 2010
Event8th International Symposium on Automated Technology for Verification and Analysis, ATVA 2010 - Singapore, Singapore
Duration: 21 Sep 201024 Sep 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6252 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other8th International Symposium on Automated Technology for Verification and Analysis, ATVA 2010
CountrySingapore
CitySingapore
Period21/09/1024/09/10

Keywords

  • diagnostic information
  • failures
  • Probabilistic B
  • quantitative safety
  • rewards

Fingerprint Dive into the research topics of 'YAGA: automated analysis of quantitative safety specifications in probabilistic B'. Together they form a unique fingerprint.

Cite this