Developement of Specifications
An effective assistance to the process of building specifications needs a better understanding of the different stages of the specification’s development process. This understanding must lead to model this process. Several directions in current research concur to this task:
- Development methods. Their aim is to help the specifier during the elaboration of the specification. At every step, they offer specifiers some guidance by suggesting tasks to do and how to approach them. Some existing methods use graphical notations. Their relative simplicity makes the dialog between users and developers easier. However, they often lack rigor when their descriptions rely on informal languages.
- Refinement. In formal methods, a refinement is the verifiable transformation of an abstract (high-level) formal specification into a concrete (low-level) executable program. A stepwise refinement allows this process to be done in stages.
- Specification languages. They must offer specifiers understandable notations as well as abstractions close to their cognitive work model. Representations proposed by semi-formal approaches provide an interesting help to the specifiers’ intuition. These languages are confronted with the difficult trade-off between offering a minimal set of central concepts and offering a richer expressiveness, then introducing more constructs in the language and making the validation work more difficult.
- Verification and validation tools. Validation and verification done early in the life cycle increase the quality of models and thus of software. The tools for verification are type checkers, theorem provers, and systematic analysis of specification. Validation tools include prototype generators, specification animators, and test gen- erators. Proofs can be done to assert some properties, to refute unwanted behaviors, as well as to check the correctness of a refinement step (i.e., that a specification is coherent with the one of the previous step)
- Development environments. Their aim is to provide specifiers with tools to support the specification process. They have been touted as a solution to improve the quality and the documentation of software. Unfortunately, most of the existing environments lack a formal basis which is needed to assess the correctness both of the product and the process.
Verification versus Validation
As the complexity of the systems developed with formal methods increases, the complexity of the abstract models used during the development increases too. This obvious observation hides the fact that the validation of the formal models becomes a crucial issue both for the correction of the final software and for the trust one can have in formally developed software.
The refinement-based development process advocated in B or Event-B is similar to a waterall process: the initial model fixes the invariant the implementation must guarantee and each refinement is proved against this abstract invariant. Such approaches assume three properties: we have all the requirements to write the initial model, the initial model is an adequate formal description of the safety and functional requirements, and all decisions during refinement can be backed up by a requirement. In practice, few developments fully enjoy such properties: requirements evolve with the developement, not all requirements can be expressed in the initial model, many refinements introduce new information into the model.
One way to address the problem above is to associate with each refinement step a validation activity along with the verification activity. Among the techniques used to validate models, their execution is the most appealing, particularly for model-based modeling framework such as Event-B. The biggest difficulty comes from the non-determinism of most of the models along the refinement chain. In fact, good practice recommands to reduce abstraction and non-determinism very slowly. While current tools such as ProB, can animate models with a moderate amount of non-determinism, they are still unable to deal with many. Exhaustive exploration strategies blow quickly into combinatorial explosion.
For such abstract models, a reasonable approach is to validate a restricted part the specified space which corresponds to “the interesting part” of the model. Users, either developers or validers, can provide their own solutions to the non-deterministic traits. This raises two questions: is the validation extensive enough? Is the execution really specified by the model? The former question is beyond our reach. The latter can be answered formally by the notion of fidelity we have developed.
Assessment of the usability of Event-B
As the maturity of Event-B and its environment is increasing, it becomes needed to assess its usability on practical systems. Practioners must have a clear view on the type of systems where this refinement-base method is amenable. When using it, developers must have patterns and techniques to deal with typical kinds of structures in their problem at hand. To address this issue, an important part of our work is devoted to the development of case-studies with two characteristics: a size consistent with real-life problems, and some features which are at out of Event-B “natural” expressiveness.
In the recent years, we have modeled two systems: a platooning control algorithm and the domain of land transportation. The platooning case-study addressed the modeling of situated Multi-Agents Systems (MAS). The particular MAS can be formulated within the Influence/Reaction model as proposed by Ferber & Muller. A first model of a simplified version uncovered usefull techniques and patterns to use Event-B for modeling MAS. A second model studied the scaling-up of the 1D simplified to a 2D more real- istic model. An important feature of the new model is the treatment of trigonometric functions in a modeling environment which knows only integers. Several observations have been made during this case study:
- the patterns previously developed are solid and scale well,
- several techniques have been devised to introduce and discretize the trigonometric funcitons so the specificastion is still fully provable,
- during the development, the validation of the refinements is essential to prevent the apparition of un- wanted behaviors, such as partial dead-locks or emerging “bad” behaviors.
The tranport domain case-study addressed the modeling of a domain with time properties. The main lessons form this study where:
- a transformation technique to use animation tools to validate the model,
- the notion of “observation level” to help structure and explain the development.