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.Applications.
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.