Contracts for modular discrete controller synthesis

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 programmi...

• Type: Conference
• Year: 2010
• Where: LCTRTS
• Authors: Gwenaël Delaval, Hervé Marchand, Éric Rutten
• Keywords: Discrete Controller Synthesis, LCTRTS 2010, Programming Languages, Reactive Programming Language, Software Engineering