About MOSEL: Formal Methods and Applications
The annual report of the year 2014 is available.
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. The MOSEL research team develops such concepts, and applies them 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.
A new project is starting in the MOSEL team, namely VeriDis. It gathers researchers from MOSEL and from the SaarMax-Planck-Institut für Informatik,Saarland University. The VeriDis project aims to exploit and further develop the advances and integration of interactive and automated theorem proving applied to the area of concurrent and distributed systems. The goal of our project is to assist algorithm and system designers to carry out formally proved developments, where proofs of relevant properties as well as bugs can be found fully automatically. Automated as well as interactive deduction techniques have seen spectacular progress over the last decade, and these techniques have had substantial impact. In particular, they have been successfully applied to the verification and analysis of sequential programs, often in combination with static analysis and software model checking. Among others, several INRIA teams are working in this area. In an ideal world, systems and their properties are specified in high-level, expressive languages, errors in specifications are discovered automatically, and finally, full verification is also performed completely automatically. Due to the inherent complexity of the problem this cannot be achieved in general. However, we have observed important advances in automated and interactive theorem proving in recent years, to which we have also participated, in particular concerning the integration of relevant theories such as arithmetic in automated theorem proving. These advances suggest that a substantially higher degree of automation can be achieved in system verification over what is available in today's verification tools.