Contracts for modular discrete controller synthesis

Abstract : 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.
Type de document :
Communication dans un congrès
Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systems, Apr 2010, Stockholm, Sweden. pp.57-66, 2010, <http://portal.acm.org/citation.cfm?doid=1755888.1755898>. <10.1145/1755888.1755898>
Liste complète des métadonnées


https://hal.inria.fr/inria-00476910
Contributeur : Hervé Marchand <>
Soumis le : mardi 27 avril 2010 - 15:21:31
Dernière modification le : vendredi 3 juin 2016 - 01:06:26
Document(s) archivé(s) le : mardi 28 septembre 2010 - 13:14:54

Fichier

lctes2010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Gwenaël Delaval, Hervé Marchand, Éric Rutten. Contracts for modular discrete controller synthesis. Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systems, Apr 2010, Stockholm, Sweden. pp.57-66, 2010, <http://portal.acm.org/citation.cfm?doid=1755888.1755898>. <10.1145/1755888.1755898>. <inria-00476910>

Partager

Métriques

Consultations de
la notice

295

Téléchargements du document

257