We describe the extension of a reactive programming language with a behavioral contract construct. It is dedicated to the programming of reactive control of applications in embedded systems, 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 process. From transition system specifications of possible behaviors, DCS automatically produces controllers that make the controlled system satisfy the property given as objective. Our language features and compiling technique provide correctness-by-construction in that sense, and enhance reliability and verifiability. Our application 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 particularly 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 reduce 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 computed 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. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. To copy otherwise, to republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. LCTES'10, April 13-15, 2010, Stockholm, Sweden. Copyright c 2010 ACM 978-1-60558-953-4/10/04. . . $10.00 Categories and Subject Descriptors We integrate discrete controller synthesis (DCS) into a modular compilation process for a synchronous language: BZR, with motivations concerning the design of programming languages, the use of DCS, and the control of adaptive and reconfigurable systems. Programming languages. We propose a compilation concretely exploiting a representation of the dynamical behavior of the program. Classically, compilation considers properties holding for all states (i.e., static); but we propose to consider state and path-dependent aspects (i.e., dynamical) [21] . DCS is a constructive operation, as it computes not a diagnostic about correctness, but a correct solution. A few works exist about its integration into a programming language framework [4] . We associate it to a contract mechanism, making it easier to use by programmers and favoring scalability (see further). Symmetrically, we propose a new point of view on the design by contracts principle: our programming language allows contracts to be enforced in nondeterministic programs, instead of being checked or proved correct. Discrete controller synthesis. The modular application of DCS, which we are addressing in this paper, is based on contract enforcement and abstraction of components, with the aim of improving the scalability of the techniques devoted to DCS. Furthermore, the integration of these techniques in a high-level programming language also contributes to make it more widely usable in computer systems, and to study implementations of the controllers at a higher level than programmable logic controllers used in automation. Control of adaptive and reconfigurable systems. Embedded systems have to be predictable, for safety-criticality issues. They also have to be able of dynamical adaptivity and reconfiguration, in reaction to environment changes, related to resources or dependability. This requires abilities for sensing the state of a system, deciding, based on a representation of the system, upon reconfiguration actions, and performing and executing them. These functionalities are assembled into a decision loop as illustrated in Figure 1 (a). Approach followed in our work. We want to combine these two different requirements, i.e., to be adaptive and predictable. Our  57
It has been integrated in a synchronous language named BZR REF ].
Contracts for modular discrete controller synthesis
LCTES '10
Computer Science