General informations

6 months
Gwenaël Delaval (UJF/Lig), Éric Rutten (Inria)
Expected skills and background:
programming languages and compilation, reactive systems, use and application of automata-based specifications


Discrete Controller Synthesis (DCS) is a formal method which operates on a non-deterministic program containing controllable variables, and a behavioral property a priori not verified by this program. From this, DCS computes a controller, which, composed with the original program, will enforce the behavioral property on it.

BZR is a reactive language, belonging to the synchronous languages family. It is based on data-flow and automata styles, and its main feature is to include discrete controller synthesis within its compilation. This feature allows to describe programs in an imperative part, which describes possible behaviors, and a declarative part, which specifies behavioral constraints to be respected.

The latter is a behavioral contract mechanisms, where assumptions can be described, as well as an "enforce" property part: the semantics of this latter is that the property should be enforced by controlling the behaviour of the node equipped with the contract. This property will be enforced by an automatically built controller, which will act on free controllable variables given by the programmer.

This Masters will focus on the problem of diagnosis of BZR programs, which is made special by the fact that discrete controller synthesis can find a solution when it exists, but it is not easy to precisely diagnose cases where no solution can be found. This will be studied in relation with related work in declarative and constraints languages, and diagnosis techniques will be defined, and integrated with the imperative aspects in the language.

Expected work

Formalization of a diagnosis methodology, and implementation of this methodology in the BZR compiler.