%0 Conference Proceedings
%F delaval10a
%A Delaval, G.
%A Marchand, H.
%A Rutten, E.
%T Contracts for Modular Discrete Controller Synthesis
%B Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2010
%P 57-66
%C Stockholm, Sweden
%X 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
%U http://www.irisa.fr/vertecs/Publis/Ps/2010-LCTES.pdf
%U http://dx.doi.org/10.1145/1755888.1755898
%8 April
%D 2010