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.

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.

This paper explores the possibility to incorporate validation in the stepwise development process of formal specifications. Formal methods based on refinement break the intractable proof of the correctness of implementation into a sequence of many smaller proofs. Likewise, the validation of the specification could be broken into smaller steps associated to refinements with the technique of animation. Animating an abstract specification often requires to alter it in ways that proof obligations cannot be discharged anymore. So, we have developed a process and a set of transformation rules whose application produces an anima table specification which may be non-provable, but which is assured to have the same behavior. Guaranteeing behavioral preservation requires us to define an ad-hoc relationship between specifications based on a kind of trace semantics. 10 rules have been identified and proven to preserve behavior. Observations on the use of the technique on two case-studies are presented.

Well specified requirements are crucial for good software design and domain engineering helps better understanding and specification of requirements. Safety critical domains, such as transportation, exhibit interesting features, such as high levels of non-determinism, complex interactions, stringent safety properties, multifaceted timing attributes, etc. The formal representation of these features is a challenging task. This paper presents our experience of modeling land transportation domain in the formal framework of Event-B. We explore the possibility of using Event-B as a domain engineering tool. We discuss the problems posed by the introduction of time and how we tackle it. We design a technique based on animation to validate domain models.

The paper presents our work in the domain of formal specification of user-interfaces.We think that engineering user-interfaces would greatly benefit from the use of formal techniques.To achieve this goal, we need a framework with two properties.First, it must be based on a formal model which expresses interesting features.Second, it must lead to the implementation of tools to help validate the specification.Our approach has been to define and to formalize, with VDM, a model focusing on dialogue structures based on the notion of planning.This model provides us with the semantic foundation of a specification language which can be used as the first formal description of a user-interface.This semantics, in turn, has allowed us to implement a prototyping tool which produces an executable instance of the interface along with an interactive visualization of the dialogue structures.Such prototypes can be used during the validation process of the specification.

Ideally, a requirement specification language should lead to highly readable text while being implementable. Unfortunately, current technology does not offer good support for features which enhance legibility such as elisions, flexible syntaxes, and more generally incomplete texts. GLIDER's designers have deliberately included those features in the language, thus forbidding some texts to be processed. This study is a rigorous assessment, both qualitative and quantitative, of this decision on the first step of processing: the parsing of terms.

The paper addresses the issue of safe modification of code, as required in maintenance or in development by reuse. It presents a framework for modeling and recording program development. The framework is based on the notion of planning, workplan, and product. An example of program modification using the development record is detailed; it shows how the framework and the records can be used to drive consistent developments of new functions. We conclude by discussing how development techniques based on analogy and process capture can give a pragmatic and effective answer to the problems of code reuse and program evolution.>