The Dedale team focuses on two topics, closely related to the recent emergence of effective tools (Rodin for instance): the first topic concerns the development techniques to validate formal specifications through their construction; the second topic is the integration of semi-formal requirements into the development process of formal models. 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:
– Requirements. The aim is to understand and describe methodologically how to break an informal requirement document into a set of highly rigourous semi-formal sentences consistent with a refinement approach. The application of this work on Event-B and ProR facilitates the association our validation plugins.
– Refinement and specification languages. A refinement is the verifiable transformation of an abstract formal specification into a concrete executable program. A stepwise refinement allows this process to be done in stages.
– Development methods. Their aim is to help the specifier during the elaboration of the specification. At every step, they offer guidance by suggesting tasks to do and how to approach them, using graphical notations.
– Development environments. Their aim is to provide developers with tools to support the requirement and specification process.
– Verification and validation tools. They are done early in the life cycle and increase the quality of models and software. Tools for verification are type checkers, theorem provers, and systematic analysis of specification. Validation tools include prototype generators, specification animators, and test generators. Proofs can be done to assert some properties, to refute unwanted behaviors, as well as to check the correctness of a refinement step.
