Refinement-based Validation of Event-B Specifications

Atif Mashkoor 1 Faqing Yang 2 Jean-Pierre Jacquot 3
2 DEDALE - Development of specifications
LORIA - FM - Department of Formal Methods
3 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 the models. We 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 result- ing from non-deterministic features by either modifying the model or provid- ing ad-hoc implementations. We have defined a formal notion, called fidelity, which guarantees that all the observable behaviors of the executable models are indeed specified by the original (non-deterministic) model. Fidelity can be expressed in terms of proof obligations.
Type de document :
Article dans une revue
Software and Systems Modeling, Springer Verlag, 2016, pp.33. 〈10.1007/s10270-016-0514-4〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01262106
Contributeur : Jean-Pierre Jacquot <>
Soumis le : mardi 26 janvier 2016 - 11:29:45
Dernière modification le : mardi 24 avril 2018 - 13:54:35

Identifiants

Collections

Citation

Atif Mashkoor, Faqing Yang, Jean-Pierre Jacquot. Refinement-based Validation of Event-B Specifications . Software and Systems Modeling, Springer Verlag, 2016, pp.33. 〈10.1007/s10270-016-0514-4〉. 〈hal-01262106〉

Partager

Métriques

Consultations de la notice

203