We welcome applications for a post-doctoral position on :
Compilation techniques and programming methodologies using controller synthesis
contact us : Gwenael.Delaval@inria.fr
applications must be made there before march 31 !
https://jobs.inria.fr/public/classic/en/offres/2018-00550
This post-doc is proposed by Gwenaël Delaval, in the Inria Ctrl-A team,
a common team between Lig (Laboratoire d’Informatique de Grenoble) and Inria,
located in Grenoble.
keywords
Compilation, programming languages, reactive systems, formal methods,
discrete controller synthesis
Scientific context:
Computing systems are more and more ubiquitous, at scales from tiny
embedded systems to large-scale cloud infrastructures. They are more
and more adaptive and reconfigurable, for resource management, energy
efficiency, or by functionality. Furthermore, these systems are
increasingly complex and autonomous: their administration cannot any
longer rely on a strong interaction with a human administrator. The
correct design and implementation of automated control of the
reconfigurations and/or their tuning is recognized as a key issue for
the effectiveness of these adaptive systems. The Ctrl-A team builds
methods and tools for the design of safe controllers for autonomic,
adaptive, reconfigurable computing systems, by combining Computer
Science and Control Theory.
Our main design language and tool is Heptagon/BZR (http://bzr.inria.fr), 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 takes the form of a behavioral
contract mechanism, 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 synthesized controller, which will act on free
controllable variables given by the programmer. This is done using
Discrete Controller Synthesis (DCS) : 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.
Heptagon/BZR is currently applied in different domains:
component-based design and the Fractal framework; operating systems
and administration loops in data-centers; hardware and reconfigurable
architecture (FPGAs); smart environments and the Internet of Things.
Post-doc topic
The post-doc work will contribute in extending the Heptagon/BZR language (http://bzr.inria.fr) with novel features, in order to consolidate its usability as well as enabling enabling implementations of the controllers on distributed execution architectures.
One axis will focus on 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.
Another axis will focus on the problem of diagnosis of Heptagon/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.
Additionally, approaches will be explored for the integration in the language of mechanisms of adaptive discrete control, where the controller itself can be reconfigured at runtime, in order to enforce different objectives, or to accomodate changes in the controlled system or environment.
expected skills
The applicant should have good knowledge in:
* semantics, programming languages, compilation
* formal methods for the validation of programs or systems
The applicant should also have good programming skills. Knowledge about
programming languages and design methods for reactive systems would be preferable.
more info
The post-doc will be supervised by Gwenaël Delaval (Ctrl-A Lig/Inria team).
Ctrl-A team web page : https://team.inria.fr/ctrl-a/
Heptagon web page : http://heptagon.gforge.inria.fr
Personal web page : http://pop-art.inrialpes.fr/people/delaval/
Bibliography :
G. Delaval, S. M.-K. Gueye and E. Rutten. Distributed Execution of
Modular Discrete Controllers for Data Center Management. 5th IFAC
international workshop on Dependable Control of Discrete Systems
(DCDS’15), 2015, Cancun, Mexico.
G. Delaval, E. Rutten and H. Marchand. Integrating Discrete Controller Synthesis
into a Reactive Programming Language Compiler. In Discrete Event Dynamic
Systems, 2013, vol. 23(4).
G. Delaval. Modular distribution and application to discrete controller
synthesis. In International Workshop on Model-driven High-level Programming of
Embedded Systems (SLA++P’08), Budapest, Hungary, April 2008.
