François PESSAUX
Contact
| Address: | ENSTA - 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.
Publications
