research-article

Contracts for modular discrete controller synthesis

Authors:

Gwenaël Delaval,

Hervé Marchand,

Eric RuttenAuthors Info & Claims

ACM SIGPLAN Notices, Volume 45, Issue 4

Pages 57 - 66

https://doi.org/10.1145/1755951.1755898

Published: 13 April 2010 Publication History

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.

References

[1]

S. Abdelwahed and W. Wonham. Supervisory control of interacting discrete event systems. In 41th IEEE Conference on Decision and Control, pages 1175--1180, Las Vegas, USA, December 2002.

[2]

S. Aboubekr, G. Delaval, and E. Rutten. A programming language for adaptation control: Case study. In 2nd Workshop on Adaptive and Reconfigurable Embedded Systems (APRES 2009). ACM SIGBED Review, volume 6, Grenoble, France, Oct. 2009.

Digital Library

[3]

K. Akesson, H. Flordal, and M. Fabian. Exploiting modularity for synthesis and verification of supervisors. In Proc. of the IFAC, 2002.

[4]

K. Altisen, A. Clodic, F. Maraninchi, and E. Rutten. Using controller synthesis to build property-enforcing layers. In Proceedings of the European Symposium on Programming (ESOP'03), number 2618 in LNCS, Warsaw, Poland, Apr. 2003.

Digital Library

[5]

R.-J. Back and C. C. Seceleanu. Contracts and games in controller synthesis for discrete systems. In IEEE Int. Conf. on Engineering of Computer-Based Systems, page 307, 2004.

Digital Library

[6]

A. Benveniste, B. Caillaud, and R. Passerone. A generic model of contracts for embedded systems. Res. Rep. RR-6214, INRIA, 2007.

[7]

A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. L. Guernic, and R. de Simone. The synchronous languages twelve years later. Proc. of the IEEE, 91(1):64--83, Jan. 2003.

[8]

C. Cassandras and S. Lafortune. Introduction to Discrete Event Systems. Kluwer Academic Publishers, 1999.

Digital Library

[9]

A. Chakrabarti, L. de Alfaro, T. Henzinger, and F. Mang. Synchronous and bidirectional component interfaces. In CAV 2002: 14th Int. Conf. on Computer Aided Verification, LNCS, 2002.

Digital Library

[10]

J.-L. Colaço, B. Pagano, and M. Pouzet. A Conservative Extension of Synchronous Data-flow with State Machines. In ACM Int. Conf. on Embedded Software (EMSOFT'05), Jersey city, New Jersey, USA, September 2005.

Digital Library

[11]

M. De Queiroz and J. Cury. Modular control of composed systems. In Proceedings of the American Control Conference, pages 4051--4055, Chicago, Illinois, June 2000.

[12]

G. Delaval and E. Rutten. A domain-specific language for multi-task systems, applying discrete controller synthesis. J. on Embedded Systems, 2007(84192):17, Jan. 2007. www.hindawi.com/journals/es.

[13]

Y. Hietter, J.-M. Roussel, and J.-J. Lesage. Algebraic Synthesis of Transition Conditions of a State Model. In Proc. of 9th Int. Workshop On Discrete Event Systems (WODES'08), Göteborg, June 2008.

[14]

R. Leduc, W. Wonham, and M. Lawford. Hierarchical interface-based supervisory control: Parallel case. In Proc. of the 39th Allerton Conf. on Comm., Contr., and Comp., pages 386--395, October 2001.

[15]

C. Ma and W. Wonham. A symbolic approach to the supervision of state tree structures. In 13th Mediterranean Conference on Control and Automation, Limassol, Cyprus, June 2005.

[16]

F. Maraninchi and L. Morel. Logical-time contracts for the development of reactive embedded software. In 30th Euromicro Conference, Component-Based Software Engineering Track (ECBSE), Rennes, France, Sept. 2004.

Digital Library

[17]

H. Marchand, P. Bournai, M. L. Borgne, and P. L. Guernic. Synthesis of discrete-event controllers based on the Signal environment. Discrete Event Dynamic System: Theory and Applications, 10(4), Oct. 2000.

Digital Library

[18]

H. Marchand and B. Gaudin. Supervisory control problems of hierarchical finite state machines. In 41th IEEE Conference on Decision and Control, Las Vegas, USA, December 2002.

[19]

B. Meyer. Applying "design by contract". Computer, 25(10):40--51, Oct 1992.

Digital Library

[20]

P. J. Ramadge and W. M. Wonham. The control of discrete event systems. Proceedings of the IEEE; Special issue on Dynamics of Discrete Event Systems, 77(1):81--98, 1989.

[21]

Y. Wang, S. Lafortune, T. kelly, M. Kudlur, and S. Mahlke. The Theory of Deadlock Avoidance via Discrete Control. In ACM Symposium on Principles of Programming Languages (POPL'09), Savannah, Georgia, USA, January 2009.

Digital Library

[22]

Y. Willner and M. Heymann. Supervisory control of concurrent discrete-event systems. Int. J. of Control, 54(5):1143--1169, 1991.

Cited By

Gatouillat ABadr YMassot B(2019)Smart and safe self‐adaption of connected devices based on discrete controllersIET Software10.1049/iet-sen.2018.502913:1(49-59)Online publication date: Feb-2019
https://doi.org/10.1049/iet-sen.2018.5029
Gatouillat ABadr YMassot B(2017)QoS-Driven Self-adaptation for Critical IoT-Based SystemsService-Oriented Computing – ICSOC 2017 Workshops10.1007/978-3-319-91764-1_8(93-105)Online publication date: 13-Nov-2017
https://dl.acm.org/doi/10.1007/978-3-319-91764-1_8
Louvel MPacull FRutten ESylla A(2017)Development Tools for Rule-Based Coordination Programming in LINCCoordination Models and Languages10.1007/978-3-319-59746-1_5(78-96)Online publication date: 27-May-2017
https://doi.org/10.1007/978-3-319-59746-1_5
Show More Cited By

Index Terms

Recommendations

Contracts for modular discrete controller synthesis
LCTES '10: Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systems

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 ...
Integrating discrete controller synthesis into a reactive programming language compiler

We define a mixed imperative/declarative programming language: declarative contracts are enforced upon imperatively described behaviors. This paper describes the semantics of the language, making use of the notion of Discrete Controller Synthesis (DCS). ...
QoS and energy management coordination using discrete controller synthesis
GCM '10: Proceedings of the 1st Workshop on Green Computing

Green computing is nowadays a major challenge for most IT organizations. Administrators have to manage the trade-off between system performances and energy saving goals. Autonomic computing is a promising approach to control the QoS and the energy ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 45, Issue 4

LCTES '10

April 2010

170 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1755951

Issue’s Table of Contents

LCTES '10: Proceedings of the ACM SIGPLAN/SIGBED 2010 conference on Languages, compilers, and tools for embedded systems
April 2010
184 pages
ISBN:9781605589534
DOI:10.1145/1755888
General Chair:
Jaejin Lee
Seoul National University, Korea
,
Program Chair:
Bruce B. Childers
University of Pittsburgh, USA

Copyright © 2010 ACM.

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. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 April 2010

Published in SIGPLAN Volume 45, Issue 4

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

42
Total Citations
View Citations
271
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gatouillat ABadr YMassot B(2019)Smart and safe self‐adaption of connected devices based on discrete controllersIET Software10.1049/iet-sen.2018.502913:1(49-59)Online publication date: Feb-2019
https://doi.org/10.1049/iet-sen.2018.5029
Gatouillat ABadr YMassot B(2017)QoS-Driven Self-adaptation for Critical IoT-Based SystemsService-Oriented Computing – ICSOC 2017 Workshops10.1007/978-3-319-91764-1_8(93-105)Online publication date: 13-Nov-2017
https://dl.acm.org/doi/10.1007/978-3-319-91764-1_8
Louvel MPacull FRutten ESylla A(2017)Development Tools for Rule-Based Coordination Programming in LINCCoordination Models and Languages10.1007/978-3-319-59746-1_5(78-96)Online publication date: 27-May-2017
https://doi.org/10.1007/978-3-319-59746-1_5
Ochoa-Ruiz GGuillet SLamotte FRutten EBourennane EDiguet JGogniat G(2015)An MDE Approach for Rapid Prototyping and Implementation of Dynamic Reconfigurable SystemsACM Transactions on Design Automation of Electronic Systems10.1145/280078421:1(1-25)Online publication date: 2-Dec-2015
https://dl.acm.org/doi/10.1145/2800784
Dalbouchi RTrabelsi CElhajji MZitouni A(2023)A Model-Driven Platform for Dynamic Partially Reconfigurable Architectures: A Case Study of a Watermarking SystemMicromachines10.3390/mi1402048114:2(481)Online publication date: 19-Feb-2023
https://doi.org/10.3390/mi14020481
Anwar MRashid MAzam FKashif MButt W(2019)A model-driven framework for design and verification of embedded systems through SystemVerilogDesign Automation for Embedded Systems10.1007/s10617-019-09229-y23:3-4(179-223)Online publication date: 8-Nov-2019
https://doi.org/10.1007/s10617-019-09229-y
Gatouillat ABadr YMassot BHaddad HWainwright RChbeir R(2018)Hybrid controller synthesis for the IoTProceedings of the 33rd Annual ACM Symposium on Applied Computing10.1145/3167132.3167219(783-790)Online publication date: 9-Apr-2018
https://dl.acm.org/doi/10.1145/3167132.3167219
Rutten EMarchand NSimon D(2018)Feedback Control as MAPE-K Loop in Autonomic ComputingSoftware Engineering for Self-Adaptive Systems III. Assurances10.1007/978-3-319-74183-3_12(349-373)Online publication date: 18-Jan-2018
https://doi.org/10.1007/978-3-319-74183-3_12
Zhou NDelaval GRobu BRutten ÉMéhaut J(2018)An autonomic‐computing approach on mapping threads to multi‐cores for software transactional memoryConcurrency and Computation: Practice and Experience10.1002/cpe.450630:18Online publication date: 27-May-2018
https://doi.org/10.1002/cpe.4506
An XRutten EDiguet JGamatié A(2016)Model-Based Design of Correct Controllers for Dynamically Reconfigurable ArchitecturesACM Transactions on Embedded Computing Systems10.1145/287305615:3(1-27)Online publication date: 23-May-2016
https://dl.acm.org/doi/10.1145/2873056
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents