Refinement-based validation of Event-B specifications

F. Yang, J. Jacquot. Refinement-based validation of Event-B specifications. Software and Systems Modelling, volume 16, number 3, pages 789-808, DOI 10.1007/s10270-016-0514-4, 7, 2017.

Autoren
  • Faqing Yang
  • Jean-Pierre Jacquot
TypArtikel
JournalSoftware and Systems Modelling
Nummer3
Band16
DOI10.1007/s10270-016-0514-4
ISSN1619-1366
Monat7
Jahr2017
Seiten789-808
Abstract

The validation of formal specifications is a challenging task. It is one of the factors that impede the penetration of formal methods into the common practices of software development. This paper discusses the issue of validating formal models by executing them in the context of Event-B. The most important problem lies in the non-determinism which often prevents purely automatic tools to execute models. In this paper, we first present and discuss the techniques we have created to allow the execution of models at all levels of abstraction. These techniques rely on users to overcome the barriers resulting from non-deterministic features by either modifying the model or providing ad hoc implementations. Then, we present our main contribution, the formal definition of the notion of fidelity that guarantees that all the observable behaviors of the executable models are indeed specified by the original (non-deterministic) models. The notion of fidelity can be expressed in terms of proof obligations.