MOSEL Research team
Proof-oriented development of computer-based systems
- Leader : Dominique Méry
- Research center(s) : CRI Nancy - Grand Est
- Field : Algorithmics, Programming, Software and Architecture
- Theme : Programs, Verification and Proofs
- Partner(s) : Université de Lorraine,CNRS
- Collaborator(s) : CNRS, INRIA
Proof-oriented system development aims to reinforce standard methods for the design of computer-based systems by formal description and analysis techniques that can help to ensure higher levels of reliability and correctness. Based on a precise mathematical semantics, it offers powerful techniques for the validation and analysis of system models, including comprehensive testing and verification, that accompany and guide the development process. We are interested in a class of systems that includes reactive, distributed, real-time, and mobile systems, possibly concerning both hardware and software aspects. The design of systems of realistic scale requires models to be built at different levels of abstraction and detail. In a formal approach to system development, these models are related by the key concept of refinement, which ensures that properties established at an abstract level are preserved by the implementation. The refinement relationship between system specifications is established by a rigorous proof showing that the class of models of the detailed specification is contained in the class of models of the abstract one.
The benefits of an approach based on refinement are numerous: from the point of view of the system developer, system requirements can be addressed in several steps (or cycles) of system development, and feedback on the properties of the current model of the system or on design errors is obtained quite early. From the point of view of the verifier, the burden of proof is spread over the development process, and the preservation of key properties such as safety, security or availability is guaranteed. The presence of intermediate system models both reduces the complexity of the proof obligations (allowing for a higher degree of automation) and produces a trace of ``milestones'' produced during the development of a system, documenting the design. Validation techniques such as tests and simulation can be applied to the intermediary models and enable the early detection of design faults.
- Foundations and methodology.
- A credible formal design method must take into account the typical development life cycle from requirement engineering through component design to integration. These phases result in different system models; refinement ensures that these models are coherent. We believe that the basic elements of the theory of refinement are well-established and we propose to base our approach on existing theories (specifically, Abrial's B method, especially in its event-based variant, and Lamport's TLA+. However, we will not refrain from foundational research where necessary. In particular, new system paradigms such as agent-based and mobile systems require appropriate extensions. Moreover, serious consideration of proofs as artefacts of system design requires conceptual work on proof engineering, including the representation, management, and reuse of proofs and of entire developments, based on composition and genericity.
- Notation and tools.
- A second line of research derives concrete notations, methods, and associated tools from our conceptual work. We have previously defined the framework of predicate diagrams and have shown how system verification and refinement can be carried out (and can partly be automated) within this framework. We want to further develop this approach, support it by tools that we and others can use, and also relate it to semi-formal notations and methods that are widely used in practice. Finally, we see interesting pedagogical applications of our approach, which can in turn reinforce the design of new systems.
- Academic and industrial case studies, which have always been an important element of our work, serve to validate our ideas and lay the basis for their transfer to actual use by practitioners. In turn, realistic case studies require the availability of (semi-)automatic tools that generate and, where possible, discharge the relevant proof obligations. Although we do not view the development of new tools as our primary focus of research, we envisage to integrate and adapt existing tools for our approach.
These research subjects are strongly interrelated and mutually dependent. The originality of our approach resides in the combination of the following aspects:
- Our work relies on refinement and abstraction as a methodological basis for system development as well as, more technically, to combat the state explosion problem in algorithmic verification techniques.
- Our notion of proof is based on an integration of different verification techniques (e.g., model checking, abstract interpretation, and interactive proof). We try to find the right balance, both methodologically and technically, between automatic and interactive proof methods.
- We aim at a large class of systems that includes reactive, distributed, real-time, and mobile, possibly embedded systems, and we intend our approach to scale to systems of realistic size.
- Part of our work aims at an integration with standard, ``semi-formal'' description techniques such as UML or hardware description languages.
International and industrial relations
- Project RNRT EQUAST with TDF, Thalès, LIEN-UHP
- Joint work with researchers from the University of Munich we are
studying logics for mobile computation as well as the application of
model checking techniques to UML designs.
- Joint works with ClearSY and J.-R. Abrial on the B event-based method and related tools (Click'n'Prove).