Automating refinement checking in probabilistic system design

C. Gonzalia*, A. McIver

*Corresponding author for this work

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

Abstract

Refinement plays a crucial role in "top-down" styles of verification, such as the refinement calculus, but for probabilistic systems proof of refinement is a particularly challenging task due to the combination of probability and nondeterminism which typically arises in partially-specified systems. Whilst the theory of probabilistic refinement is well-known [18] there are few tools to help with establishing refinements between programs. In this paper we describe a tool which provides partial support during refinement proofs. The tool essentially builds small models of programs using an algebraic rewriting system to extract the overall probabilistic behaviour. We use that behaviour to recast refinement-checking as a linear satisfiability problem, which can then be exported to a linear arithmetic solver. One of the major benefits of this approach is the ability to generate counterexamples, alerting the prover to a problem in a proposed refinement. We demonstrate the technique on a small case study based on Schneider et al.'s Tank Monitoring [26].

Original languageEnglish
Title of host publicationFormal Methods and Software Engineering - 9th International Conference on Formal Engineenng Methods, ICFEM 2007, Proceedings
EditorsMichael Butler, Michael G. Hinchey, Maria M. Larrondo-Petrie
Place of PublicationBerlin; New York
PublisherSpringer, Springer Nature
Pages212-231
Number of pages20
Volume4789 LNCS
ISBN (Electronic)9783540766506
ISBN (Print)9783540766483
DOIs
Publication statusPublished - 2007
Event9th International Conference on Formal Engineering Methods, ICFEM 2007 - Boca Raton, FL, United States
Duration: 14 Nov 200715 Nov 2007

Publication series

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

Other

Other9th International Conference on Formal Engineering Methods, ICFEM 2007
CountryUnited States
CityBoca Raton, FL
Period14/11/0715/11/07

Keywords

  • Algebraic rewriting system for probability
  • Linear satisfiability
  • Probabilistic systems
  • Probabilistic verification
  • Refinement

Fingerprint Dive into the research topics of 'Automating refinement checking in probabilistic system design'. Together they form a unique fingerprint.

Cite this