François PESSAUX
Contact
| Address: | ENSTA paris - U2IS 828, Boulevard des Maréchaux 91762 Palaiseau Cedex France |  |
| Office: | R223 | |
| Email: | ||
| Tel.: | +33 1 8187 2073 |
Research
My work mainly aims at providing development tools for the design of software requiring high-level integrity, using formal methods. This project follows my previous work on the FoCaLize environment started at LIP6 and aims at continuing the design, implementation and support of this environment. The main page of FoCaLiZe can be reached here, providing access to news, downloads, documentation, resources and bug tracker. The underlying idea is to avoid usage of several different tools between the software specification, its implementation and the proofs that safety requirements hold. The ability to state properties (specifications), algorithms (implementation) and proofs that these latter really fulfill specifications, all of this in a same language, allows increasing the confidence one can have in a development. These 3 elements have to be transformed into both an executable model and an formal model, this latter being checked by a formal proof tool. One strong constraint drives this work: the programming language has to remain simple enough and close to those usually practiced in the world of software development. The complexity of dealing with a formal system has to be handled as far as possible by the compiler of the language. The FoCaLiZe compiler takes a "program" as input in which are stated properties, algorithms and proofs that these properties really hold, usually on the basis of the written algorithms. It generates two outputs. First, an OCaml program to become an executable (if the FoCaLiZe "program" is not only a specification model). Second, a complete formal model (containing the properties, algorithms and proofs) in Coq. This latter, a proof assistant, is in charge of verifying the consistency of this model in order to assess its formal correction. Hence, the proof assistant doesn't guess the proofs: it only checks their correction. Writing proofs remains the user's responsibility, using the FoCaLiZe language, but this process is greatly helped by automated provers interfaced with FoCaLiZe. Currently, only one is used: zenon, developed by Damien Doligez at INRIA, but the architecture of the FoCaLiZe language and compiler is designed to fit any other prover dedicated to particular shapes of properties. As previously stated, constructs offered by FoCaLiZe can be used for modelling purposes without "programming" objectives, which allows to integrate the environment in a design cycle more "system" than "software" oriented ("specifications-oriented"). In the current state, FoCaLiZe, allows to state first order logic properties through the language syntax. Nothing forbids a priori to imagine interfaces with other description formalisms (UML, SysML, etc.) as long as properties these latter can express remain in this logical class. Extension of FoCaLiZe to other shapes of properties (temporal, synchronous), hence other logical formalisms is currently an open problem and is one of the research axis for the future. Indeed, in the context of embedded systems, it would be nice to be able to write and prove properties involving "state" (technically, mutable values), synchronization properties (aspects à la Lustre, Lucid Synchrone...). Beyond issues of extending the language constructs, the choice of the logic, hence of the checker for the generated model will probably arise. This may even impact the model that FoCaLiZe uses to formally represent the system. In effect, trying to encompass a wider class of properties to state and prove (in order to increase the modelling expressivity) presents strong risks to impact the way a system is modelled to finally be implemented and verified.Teaching
- 2012-2013, Algorithmic and Programmation (IN101, ENSTA 1A)
- 2011-2013, Principles of Programming Languages (INE11, ENSTA 2A). With Michel Mauny.