Our Projects in the Past
Broadly, our research activities concern the development and application of formal methods for the design and analysis of computerized systems. More specifically, our work targets the verified development of safety- and security-critical systems, advocating a process based on refinement that starts with an abstract, high-level model of the system under development and successively adds detail until a final implementation is obtained. Critical correctness properties are established early on, over a relatively simple model. Later development steps are guaranteed to preserve these properties, so they never need to be reproven.
Our favorite formalisms are B and TLA+ because of their conceptual clarity, their expressiveness, and their maturity in terms of both theoretical background and tool support. We are participating in the further development of these formalisms and of the tools that support them. In particular, we are exploring how to address new system paradigms or application areas such as embedded, real-time, and mobile systems. Our research is complemented by the development of academic and industrial case studies that help us to validate our ideas in practice. Finally, we attempt to transfer some of the knowledge acquired by the formal-methods community by applying our techniques to models expressed in state-of-the-art description languages such as the UML.