General informations

Location:
Inria Grenoble-Rhône-Alpes, Montbonnot, and gipsa-lab
Length:
6 months
Advisors:
Gwenaël Delaval, Stéphane Mocanu, Eric Rutten
Expected skills and background:
discrete and probabilistic control, formal methods for the design of reactive systems

This work proposal focuses on extending the existing methodology of discrete control synthesis in an environment described by behavioral contracts with the introduction of probabilistic transitions in the subsequent synchronized automata. The application framework for this research are the reactive and adaptive environments.

Smart enviroments

Smart environments, like smart homes or smart buildings, are environments designed to react and adapt themselves to their environmental context: users behavior, time or climate change, etc. The prospects of such environments goes from improved safety and wellbeing to ecological concerns.

These environments are supplied with sensors and actuators, and with computing facilities allowing the design of autonomic loops, implementing smart policies. The increasing size and complexity of such systems, together with the need of safety properties for the user (e.g., physical safety or privacy), lead to the need of design methodologies able to answer to these safety concerns.

Instead of the classical implementation/validation process, we propose to use a method stemming from control theory: discrete controller synthesis [1]. However, this method does not allow easily to express and use probabilistic events or degraded mode.

Discrete Control and the Heptagon/BZR language

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.

Heptagon/BZR [2] 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.

Heptagon/BZR has been used for the design of autonomic managers for smart environments [3].

However, this language allows only the expression of Boolean safety properties, and the controlled resulting system is purely deterministic. Then, the expression of probabilistic events or transitions, degraded modes, is not directly possible.

The probabilistic model

As pointed out in the previous paragraphs there are two development directions (though strongly connected) of the probabilistic model.

Firstly we are interested in modelling random behaviors and events in the smart environment. The main concerns are : random sojourn time into the states of the automata, transition uncertainties characterised by probabilistic choice of the next state or probabilistic occurrence of the events and random trajectories through subset of states corresponding to degraded modes. The main theoretical tool that will be used for the model extension are the Markov chains and stochastic automata [4]. The probabilistic behavior of the new model has to be taken into account in the controller synthesis procedure. We will firstly use the DCS method for the probabilistic system and evaluate the probabilistic performance of the controller. In a fast research advancement hypotheses we may assume that we’ll then tackle with a probabilistic controller synthesis and finally compare the performances of the two approaches.

The second research direction is the extension of the Heptagon/BZR language to the probabilistic model. Of course, the achievement of this second objective is conditioned by a successful solution of the first point.

The research topic proposed in this work is positioned in a promising exploratory field. A PhD position is probable in the sequel of the Master Thesis.

Bibliography

[1]
Peter J. Ramadge and W. Murray Wonham. The Control of Discrete Event Systems. Proceedings of the IEEE 77(1), pages 81-98, 1989
[2]
Gwenaël Delaval, Eric Rutten and Hervé Marchand. Integrating Discrete Controller Synthesis in a Reactive Programming Language Compiler. In journal of Discrete Events Dynamical Systems, 2013. See http://bzr.inria.fr
[3]
Mengxuan Zhao, Gilles Privat, Eric Rutten and Hassane Alla. Discrete Control for the Internet of Things and Smart Environments. In Handouts (no Proc.) of the 8th International Workshop on Feedback Computing, in conjunction with ICAC 2013, San Jose, California, June 25, 2013.
[4]
Christos G. Cassandras and Stéphane Lafortune. Introduction to discrete event systems, Kluwer Academic Publishers, Boston, 1999
Ce document a été traduit de LATEX par HEVEA