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.

A major hindrance to the use of formal methods is the difficulty to validate the models, particularly at the early stages of the development. We propose to build simulations: programs automatically generated from the specifications but with user-provided implementations of the non-executable traits of the models. We present such a simulation. Of course, the question of the fidelity of the simulation to the model is raised in such a setting. We provide a formal definition of fidelity and the proof obligations that can be attached to each hand-coded element so that fidelity can be proven.

The validation of formal models is a challenge for formal methods. We propose JeB, a framework which generates and executes simulations of Event-B models, even highly non-deterministic ones. JeB allows users to safely insert pieces of code to supply deterministic computations where the automatic translation fails. We present how JeB translates Event-B model into JavaScript. We define Fidelity as the formal notion which captures the idea of the correctness of a simulation. We define it through proof-obligations.

Ce papier presente un outil, JeB, qui peut automatiquement generer des simulateurs de modeles B evenementiel. Il fournit un environnement graphique d'execution et l'interface pour combiner les codes ecrits par l'utilisateur. Il peut etre utilise pour la visualisation et la validation des modeles B evenementiel. Les simulateurs sont implantes en HTML et JavaScript. On peut simuler les modeles B evenementiel dans les navigateurs actuels.

This paper addresses the validation of formal specifications in Event-B through the execution of the specification. Current tools for Event-B, animators and translators, can execute only a restricted set of specifications. So, we propose a third technique, simulation, in which users and tools co-operate to produce an executable instance of the model. After a short presentation of Event-B and our simulation framework, JeB, we show how to use it on two reasonably complex specifications. Observations and analysis from the point of view of validation are presented and discussed.

Ability to scale up from toy examples to real life problems is a crucial issue for formal methods. Formalizing a algorithm used in vehicle automation (platooning control) in a certification perspective, we had the opportunity to study the scaling up when going from a (toy) model in 1D to a (more realistic) model in 2D. The formalism, Event-B, belongs to the family of mathematical state based methods. Increase was quantitative: 3 times more events and 4 times more proofs; and qualitative: trigonometric functions and integrals are used. Edition and verification of the specification scale up well. The crucial part of the work was the adaptation of the mathematical and physical model through standard heuristics. The validation of temporal properties and behaviors do not scale up so well. Analysis of the difficulties suggests improvements in both tool support and formalism.

This paper presents DFT-generator, a small tool to generate Deadlock-Freeness Theorems (DFT) in Event-B specifications. Event-B, a companion to the B-method, allows specifiers to model systems and environments with the help states, invariants, and events. Events are guarded generalized substitutions which are fired non-deterministically. Assessing temporal properties such as termination or as non-blocking cycle is then a necessity. To overcome the lack of deadlock checking in the core of Event-B and of its supporting environment, Rodin, we have developed a practical little tool which generates the necessary theorems to prove that a model is free of deadlocks. We explain what are the deadlock theorems, why we need a tool to help generating the theorems, what problems were encountered during development. We conclude on a quick comparison with model-checking.

Formal methods such as B [1] or Event-B [2] are designed around the idea that a piece of code can be “correct per construction.” They use the usual notion of correctness: the program is a mathematically proven implementation of the specification. They are good candidates for industrial use for two major reasons: they embody a development process, refinement, which breaks the notoriously difficult correctness proof into many small and manageable proof obligations, and they have effective tool support. Through the realization and the analysis of two important case-studies using EventB in the area of transportation [6,5,8,9], we have discovered that proofs alone are not sufficient to produce a “good” software: we need also to execute, i.e., to test, the software. Two main reasons justify this proposition. Some properties, notably temporal, are virtually impossible to model with constructs such as states, invariants, or events which Event-B provides us. We need to ensure that the specification is an adequate model of the problem we want to solve. Software must be verified and validated. Waiting to have an executable program to begin the validation leads to the same difficulties as proving a program against its specification: costly, very complex, soon unmanageable. The strategy which works with the verification of specifications built by a stepwise refinement process could also work for validation. We should be able to enrich the development process by adding validation activities to each refinement step. Such an enhancement is discussed in [8]. The idea of executing specifications is not new [3]. Some tools have already been developed and integrated into Rodin, ProB [4] or Brama1, for instance. However, these tools are often unable to animate well written abstract specifications. In fact, qualities sought after for a well written specification, such as abstractness, non determinism, non constructive definitions, are contradictory with what is required for effective computation. To use validation early in the development cycle, which in our opinion is highly desirable, we need to find techniques to adapt the existing tools. The cost of the technique should be minimal so that it can be frequently used during refinement process. The first approach to the problem is based on the observation that being provable and being animatable are distinct qualities for specifications: they can be one, the other, or both. It is then possible, in many cases, to “downgrade” a proven, non animatable, specification into a “behaviorally equivalent” animatable, but non provable, specification. In [7], we have proposed several transformations to realize this idea. The validity of such a technique depends on the semantics of the transformations. Since ours are not

Dans un contexte de certification, la relation entre methodes formelles et logiciel correct n'est pas claire. Pour le formaliste, c'est la coherence lo- gique (preuve), pour le certificateur, c'est la bonne adequation aux besoins et contraintes de l'usage prevu (validation). Nous presentons et discutons une ana- lyse des difficultes et de leur resolution que nous avons rencontrees lors de la redaction de specifications en B evenementiel. Nous proposons un processus de developpement qui prend en compte la certification. Il est toujours fonde sur la notion de raffinement des proprietes fonctionnelles proposee par B evenemen- tiel. Les etapes de raffinement doivent etre completees par des sous-processus qui raffinent le modele physico-mathematique pour l'amener a une forme ac- ceptable par les outils de preuve, qui verifient les contraintes non-fonctionnelles, principalement temporelles, et qui valident le comportement de la specification.