## François Pessaux

### Contact

Address: | ENSTA ParisTech - U2IS 828, Boulevard des Maréchaux 91762 Palaiseau Cedex France | |

Office: | R226 | |

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.