delaval10a

G. Delaval, H. Marchand, E. Rutten. Contracts for Modular Discrete Controller Synthesis. In Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2010, Pages 57-66, Stockholm, Sweden, April 2010.

Download [help]

Download paper: Doi page

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

Abstract

We describe the extension of a reactive programming language with a behavioral contract construct. It is dedicated to the pro- gramming of reactive control of applications in embedded sys- tems, and involves principles of the supervisory control of discrete event systems. Our contribution is in a language approach where modular discrete controller synthesis (DCS) is integrated, and it is concretized in the encapsulation of DCS into a compilation pro- cess. From transition system specifications of possible behaviors, DCS automatically produces controllers that make the controlled system satisfy the property given as objective. Our language fea- tures and compiling technique provide correctness-by-construction in that sense, and enhance reliability and verifiability. Our appli- cation domain is adaptive and reconfigurable systems: closed-loop adaptation mechanisms enable flexible execution of functionalities w.r.t. changing resource and environment conditions. Our language can serve programming such adaption controllers. This paper par- ticularly describes the compilation of the language. We present a method for the modular application of discrete controller synthesis on synchronous programs, and its integration in the BZR language. We consider structured programs, as a composition of nodes, and first apply DCS on particular nodes of the program, in order to re- duce the complexity of the controller computation; then, we allow the abstraction of parts of the program for this computation; and finally, we show how to recompose the different controllers com- puted from different abstractions for their correct co-execution with the initial program. Our work is illustrated with examples, and we present quantitative results about its implementation

Contact

Hervé Marchand http://www.irisa.fr/prive/hmarchan

BibTex Reference

@InProceedings{delaval10a,
   Author = {Delaval, G. and Marchand, H. and Rutten, E.},
   Title = {Contracts for Modular Discrete Controller Synthesis},
   BookTitle = {Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2010},
   Pages = {57--66},
   Address = {Stockholm, Sweden},
   Month = {April},
   Year = {2010}
}

EndNote Reference [help]

Get EndNote Reference (.ref)