General informations
- Location:
-
- Lig, NanoSim team
- Inria Grenoble-Rhône-Alpes, Ctrl-A team, 38330 Montbonnot.
- Length:
- 6 months
- Advisors:
- Gwenaël Delaval, Éric Rutten
- Expected skills and background:
- programming languages and compilation, reactive systems, use and application of automata-based specifications
Context
Discrete Controller Synthesis (DCS) is a formal method which operates on a
non-deterministic program containing controllable variables, and a
behavioral property
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 programming and modelling methodologies, in order to obtain logical (Boolean) abstractions which can improve the use of dicrete controller synthesis. This is needed for example, in order to program the controllers for systems where the useful data for control can be of arbitrary types (integer, real, ...) , or also for systems which are naturally distributed, and require a decentralized controller. On the basis of our previous experiments on this topic, the work consist in generalizing manual techniques and defining methods to construct these abstractions.
Expected work
Formalization and implementation in the BZR compiler of an automated abstraction methodology.