Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Integrating discrete controller synthesis into a reactive programming language compiler

  • Published:
Discrete Event Dynamic Systems Aims and scope Submit manuscript

Abstract

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). We target the application domain of adaptive and reconfigurable systems: our language can serve programming closed-loop adaptation controllers, enabling flexible execution of functionalities w.r.t. changing resource and environment conditions. DCS is integrated into a1 programming language compiler, which facilitates its use by users and programmers, performing executable code generation. The tool is concretely built upon the basis of a reactive programming language compiler, where the nodes describe behaviors that can be modeled in terms of transition systems. Our compiler integrates this with a DCS tool, making it a new environment for formal methods. We define the trace semantics of our contracts language, describe its compilation and establish its correctness, and discuss implementation and examples.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17
Fig. 18

Similar content being viewed by others

Notes

  1. Such emissions on transitions, used here for simplicity, are easily translated to equations associated with states, as in Fig. 4.

  2. Note that there exists a one to one mapping from a node f (only handling Boolean variables) to \({\cal S}_f\).

  3. An observer is simply an STS allowing to capture a safety property over the sequences of the systems (e.g. the event a does not occur twice in a row in the system). As usual, we assume that an observer is complete so that when performing the composition with the STS of the system, the behavior of the resulting STS is not changed.

  4. Experiments carried out on a 64 bits dual-core PC, 2.93 GHz, with 3.8 Gb of RAM.

References

  • Aboubekr S, Delaval G, Pissard-Gibollet R, Rutten E, Simon D (2011) Automatic generation of discrete handlers of real-time continuous control tasks. In: Proc. 18th World congress of the international federation of automatic control (IFAC). Milano, Italy, pp 786–793

  • Altisen K, Clodic A, Maraninchi F, Rutten E (2003) Using controller synthesis to build property-enforcing layers. In: European symposium on programming. LNCS, vol 2618. Warsaw, Poland, pp 126–141

  • Auer A, Dingel J, Rudie K (2009) Concurrency control generation for dynamic threads using discrete-event systems. In: 47th Annual allerton conference on communication, control, and computing, 2009. Allerton 2009, pp 927–934

  • Benveniste A, Caspi P, Edwards S, Halbwachs N, Le Guernic P, de Simone R (2003) The synchronous languages twelve years later. Proc IEEE 91(1):64–83

    Article  Google Scholar 

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

  • Bodik R, Chandra S, Galenson J, Kimelman D, Tung N, Barman S, Rodarmor C (2010) Programming with angelic nondeterminism. In: Principles of programming languages, POPL, pp 339–352

  • Bouhadiba T, Sabah Q, Delaval G, Rutten E (2011) Synchronous control of reconfiguration in fractal component-based systems—a case study. In: Int. conf. on embedded software. EMSOFT 2011. Taipei, Taiwan, pp 309–318

  • Cassandras C, Lafortune S (2007) Introduction to discrete event systems. Springer

  • Cassez F, David A, Fleury E, Larsen K, Lime D (2005) Efficient on-the-fly algorithms for the analysis of timed games. In: Conf. on concurrency theory (CONCUR). LNCS, vol 3653, pp 66–80

  • Chakrabarti A, de Alfaro L, Henzinger TA, Mang FYC (2002) Synchronous and bidirectional component interfaces. In: Computer aided verification. LNCS, vol 2404. Copenhagen, Denmark, pp 414–427

  • Colaço J-L, Pagano B, Pouzet M (2005) A conservative extension of synchronous data-flow with state machines. In: Embedded software (EMSOFT). New Jersey, USA, pp 173–182

  • Delaval G, Rutten E (2010) Reactive model-based control of reconfiguration in the fractal component-based model. In: Component based software engineering. LNCS, vol 6092. Prague, Czech R., pp 93–112

  • Delaval G, Marchand H, Rutten E (2010) Contracts for modular discrete controller synthesis. In: Languages, compilers and tools for embedded systems. Stockholm, Sweden, pp 57–66

  • deQueiroz MH, Cury JER (2002) Synthesis and implementation of local modular supervisory control for a manufacturing cell. In: Proceedings of the 6th international workshop on discrete event systems, pp 377–382

  • Dragert C, Dingel J, Rudie K (2008) Generation of concurrency control code using discrete-event systems theory. In: Proceedings of the 16th ACM SIGSOFT international symposium on foundations of software engineering, SIGSOFT ’08/FSE-16. ACM, New York, NY, USA, pp 146–157

    Chapter  Google Scholar 

  • Hamon G (2002) Calcul d’horloge et structures de contrôle dans Lucid Synchrone, un langage de flots synchrones à la ML. PhD thesis, Univ. P. et M. Curie, Paris, France

  • Harel D (2008) Can programming be liberated, period? Computer 41(1):28–37

    Article  Google Scholar 

  • Harel D, Naamad A (1996) The STATEMATE semantics of statecharts. ACM Trans Softw Eng Methodol 5(4):293–333

    Article  Google Scholar 

  • Harel D, Kugler H, Pnueli A (2005) Synthesis revisited: generating statechart models from scenario-based requirements. In: Formal methods in software and systems modeling. LNCS, vol 3393, pp 309–324

  • Hellerstein J, Diao Y, Parekh S, Tilbury D (2004) Feedback control of computing systems. Wiley-IEEE

  • Hietter Y, Roussel J-M, Lesage J-J (2008) Algebraic synthesis of transition conditions of a state model. In: Proc. of 9th int. workshop on discrete event systems (WODES’08), Göteborg, pp 187–192

  • Iordache MV, Antsaklis PJ (2009) Petri nets and programming: a survey. In: Proceedings of the 2009 American control conference, pp 4994–4999

  • Iordache M, Antsaklis P (2010) Concurrent program synthesis based on supervisory control. In: 2010 American control conference

  • Jiang S, Kumar R (2000) Decentralized control of discrete event systems with specializations to local control and concurrent systems. IEEE Trans Syst Man Cybern, Part B 30(5):653–660

    Article  Google Scholar 

  • Komenda J, van Schuppen JH (2005) Supremal sublanguages of general specification languages arising in modular control of discrete-event systems. In: 44th IEEE conference on decision and control, pp 2775–2780

  • Komenda J, Masopust T, van Schuppen JH (2010) Synthesis of safe sublanguages satisfying global specification using coordination scheme for discrete-event systems. Discrete Event Dyn Syst 10:426–431

    Google Scholar 

  • Kugler H, Plock C, Pnueli A (2009) Controller synthesis from LSC requirements. In: Fundamental approaches to software engineering, FASE’09, York, UK, 22–29 March 2009

  • Le Gall T, Jeannet B, Marchand H (2005) Supervisory control of infinite symbolic systems using abstract interpretation. In: 44nd IEEE conference on decision and control (CDC’05) and control and European control conference ECC 2005. Seville, Spain, pp 31–35

  • Lee S-H, Wong KC (2002) Structural decentralized control of concurrent discrete-event systems. Eur J Control 8(5):477–491

    Article  Google Scholar 

  • Liu C, Kondratyev A, Watanabe Y, Desel J, Sangiovanni-Vincentelli A (2006) Schedulability analysis of petri nets based on structural properties. In: Sixth international conference on application of concurrency to system design, 2006. ACSD 2006, pp 69–78

  • Maraninchi F, Morel L (2004) Logical-time contracts for the development of reactive embedded software. In: 30th Euromicro conference, component-based software engineering track (ECBSE). Rennes, France, pp 48–55

  • Marchand H (1997) Méthodes de synthèse d’automatismes décrits par des systèmes à événements discrets finis. PhD thesis, Université de Rennes 1, IFSIC

  • Marchand H, Gaudin B (2002) Supervisory control problems of hierarchical finite state machines. In: 41th IEEE conference on decision and control. Las Vegas, USA, pp 1199–1204

  • Marchand H, Bournai P, Le Borgne M, Le Guernic P (2000) Synthesis of discrete-event controllers based on the signal environment. Discrete Event Dynamic Systems: Theory Appl 10(4):325–346

    Article  MATH  Google Scholar 

  • Meyer B (1992) Applying “design by contract”. Computer 25(10):40–51

    Article  Google Scholar 

  • Phoha VV, Nadgar AU, Ray A, Phoha S (2004) Supervisory control of software systems. IEEE Trans Comput 53(9):1187–1199

    Article  Google Scholar 

  • Ramadge PJ, Wonham WM (1987) Supervisory control of a class of discrete event processes. SIAM J Control Optim 25(1):206–230

    Article  MathSciNet  MATH  Google Scholar 

  • Schmidt K, Breindl C (2008) On maximal permissiveness of hierarchical and modular supervisory control approaches for discrete event systems. In: 9th international workshop on discrete event systems, 2008. WODES 2008, pp 462–467. IEEE

  • Wallace C, Jensen P, Soparkar N (1996) Supervisory control of workflow scheduling. In: Advanced transaction models and architectures workshop (ATMA), Goa, India

  • Wang Y, Lafortune S, Kelly T, Kudlur M, Mahlke S (2009) The theory of deadlock avoidance via discrete control. In Principles of programming languages, POPL. Savannah, USA, pp 252–263

Download references

Author information

Authors and Affiliations

  1. Univ. Grenoble, LIG, Grenoble, France

    Gwenaël Delaval

  2. INRIA/LIG, Grenoble, France

    Eric Rutten

  3. INRIA, Rennes, France

    Hervé Marchand

Authors
  1. Gwenaël Delaval
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eric Rutten
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Hervé Marchand
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hervé Marchand.

Additional information

This work was partly supported by the Minalogic project MIND and the ANR project Ctrl-Green.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Delaval, G., Rutten, E. & Marchand, H. Integrating discrete controller synthesis into a reactive programming language compiler. Discrete Event Dyn Syst 23, 385–418 (2013). https://doi.org/10.1007/s10626-013-0163-5

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10626-013-0163-5

Keywords

Search

Navigation