Synchronous objects with scheduling policies: introducing safe shared memory in lustre

ABSTRACT

This paper addresses the problem of designing and implementing complex control systems for real-time embedded software. Typical applications involve different control laws corresponding to different phases or modes, e.g., take-off, full flight and landing in a fly-by-wire control system. On one hand, existing methods such as the combination of Simulink/Stateflow provide powerful but unsafe mechanisms by means of imperative updates of shared variables. On the other hand, synchronous languages and tools such as Esterel or SCADE/Lustre are too restrictive and forbid to fully separate the specification of modes from their actual instantiation with a particular control automaton.

In this paper, we introduce a conservative extension of a synchronous data-flow language close to Lustre, in order to be able to define systems with modes in a more modular way, while insuring the absence of data-races. We show that such a system can be viewed as an object where modes are methods acting on a shared memory. The object is associated to a scheduling policy which specifies the ways methods can be called to build a valid synchronous reaction. We show that the verification of the proper use of an object reduces to a type inference problem using row types introduced by Wand, Rémy and Vouillon. We define the semantics of the extended synchronous language and the type system. The proposed extension has been implemented and we illustrate its use through several examples.

REFERENCES

• 1: Rajeev Alur , Thomas A. Henzinger, Reactive Modules, Formal Methods in System Design, v.15 n.1, p.7-48, July 1999 [doi>10.1023/A:1008739929481]
• 2: A. Benveniste, P. Caspi, S.A. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone. The synchronous languages 12 years later. Proceedings of the IEEE, 91(1), January 2003.
• 3: Albert Benveniste , Paul Le Guernic , Christian Jacquemot, Synchronous programming with events and relations: the SIGNAL language and its semantics, Science of Computer Programming, v.16 n.2, p.103-149, Sept. 1991 [doi>10.1016/0167-6423(91)90001-E]
• 4: Gerard Berry. The constructive semantics of pure esterel. Draft book, 1999.
• 5: Stavros Tripakis , Christos Sofronis , Paul Caspi , Adrian Curic, Translating discrete-time simulink to lustre, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.4, p.779-818, November 2005 [doi>10.1145/1113830.1113834]
• 6: Jean-Louis Colaço , Grégoire Hamon , Marc Pouzet, Mixing signals and modes in synchronous data-flow systems, Proceedings of the 6th ACM & IEEE International conference on Embedded software, October 22-25, 2006, Seoul, Korea [doi>10.1145/1176887.1176899]
• 7: Jean-Louis Colaço , Bruno Pagano , Marc Pouzet, A conservative extension of synchronous data-flow with state machines, Proceedings of the 5th ACM international conference on Embedded software, September 18-22, 2005, Jersey City, NJ, USA [doi>10.1145/1086228.1086261]
• 8: Luca de Alfaro , Thomas A. Henzinger, Interface automata, Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering, September 10-14, 2001, Vienna, Austria
• 9: Gregoire Hamon. Calcul d'horloge et Structures de Contrôle dans Lucid Synchrone, un langage de ots synchrones à la ML. PhD thesis, Université Pierre et Marie Curie, Paris, France, 14 novembre 2002.
• 10: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 11: Florence Maraninchi , Tayeb Bouhadiba, 42: programmable models of computation for a component-based approach to heterogeneous embedded systems, Proceedings of the 6th international conference on Generative programming and component engineering, October 01-03, 2007, Salzburg, Austria [doi>10.1145/1289971.1289981]
• 12: Florence Maraninchi , Yann Rémond, Mode-automata: a new domain-specific construct for the development of safe critical systems, Science of Computer Programming, v.46 n.3, p.219-254, March 2003 [doi>10.1016/S0167-6423(02)00093-X]
• 13: Bertrand Meyer. Eiffel: An Introduction. Interactive Software Eng, 1988.
• 14: Daniel Pilaud. Personnal communication, March 2009.
• 15: Didier Rémy , Jérôme Vouillon, Objective ML: an effective object-oriented extension to ML, Theory and Practice of Object Systems, v.4 n.1, p.27-50, 1998 [doi>10.1002/(SICI)1096-9942(1998)4:1<27::AID-TAPO3>3.0.CO;2-4]
• 16: Jean-Pierre Talpin , Pierre Jouvelot, The type and effect discipline, Information and Computation, v.111 n.2, p.245-296, June 1994 [doi>10.1006/inco.1994.1046]

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Data-flow languages

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
block-diagrams, compilation, real-time systems, semantics, synchronous languages, type systems