Subscribe

Issue No.07 - July (2013 vol.39)

pp: 917-929

Jens Brandt , University of Kaiserslautern, Kaiserslautern

Mike Gemunde , University of Kaiserslautern, Kaiserslautern

Klaus Schneider , University of Kaiserslautern, Kaiserslautern

Sandeep K. Shukla , Virginia Polytechnic and State University, Blacksburg

Jean-Pierre Talpin , INRIA Rennes-Bretagne-Atlantique, Rennes

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2012.85

ABSTRACT

This paper presents an embedding of polychronous programs into synchronous ones. Due to this embedding, it is not only possible to deepen the understanding of these different models of computation, but, more importantly, it is possible to transfer compilation techniques that were developed for synchronous programs to polychronous programs. This transfer is nontrivial because the underlying paradigms differ more than their names suggest: Since synchronous systems react deterministically to given inputs in discrete steps, they are typically used to describe reactive systems with a totally ordered notion of time. In contrast, polychronous system models entail a partially ordered notion of time, and are most suited to interface a system with an asynchronous environment by specifying input/output constraints from which a deterministic controller may eventually be refined and synthesized. As particular examples for the mentioned cross fertilization, we show how a simulator and a verification backend for synchronous programs can be made available to polychronous specifications, which is a first step toward integrating heterogeneous models of computation.

INDEX TERMS

Clocks, Computational modeling, Synchronization, Embedded systems, Hardware, Unified modeling language, synchronous guarded commands, Model-driven embedded software, synchronous programming, polychronous programming, programming models, synchrony hypothesis

CITATION

Jens Brandt, Mike Gemunde, Klaus Schneider, Sandeep K. Shukla, Jean-Pierre Talpin, "Embedding Polychrony into Synchrony",

*IEEE Transactions on Software Engineering*, vol.39, no. 7, pp. 917-929, July 2013, doi:10.1109/TSE.2012.85REFERENCES

- [1] A. Benveniste, B. Caillaud, and P. Le Guernic, "Compositionality in Dataflow Synchronous Languages: Specification and Distributed Code Generation,"
Information and Computation, vol. 163, pp. 125-171, 2000.- [2] A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone, "The Synchronous Languages Twelve Years Later,"
Proc. IEEE, vol. 91, no. 1, pp. 64-83, Jan. 2003.- [3] G. Berry, "A Hardware Implementation of Pure Esterel,"
Formal Methods in VLSI Design, 1991.- [4] G. Berry, "Preemption and Concurrent Systems,"
Proc. 13th Conf. Foundations of Software Technology and Theoretical Computer Science, pp. 72-93, 1993.- [5] G. Berry, "The Foundations of Esterel,"
Proof, Language and Interaction: Essays in Honour of Robin Milner, G. Plotkin, C. Stirling, and M. Tofte, eds., MIT Press, 1998.- [6] G. Berry, "The Constructive Semantics of Pure Esterel," July 1999.
- [7] G. Berry and E. Sentovich, "Multiclock Esterel,"
Proc. 11th IFIP WG 10.5 Advanced Research Working Conf. Correct Hardware Design and Verification Methods, pp. 110-125, 2001.- [8] L. Besnard, T. Gautier, P. Le Guernic, and J.-P. Talpin, "Compilation of Polychronous Data Flow Equations,"
Synthesis of Embedded Software—Frameworks and Methodologies for Correctness by Construction, S.K. Shukla and J.-P. Talpin, eds., Springer, 2010.- [9] M. Boldt, C. Traulsen, and R. von Hanxleden, "Compilation and Worst-Case Reaction Time Analysis for Multithreaded Esterel Processing,"
EURASIP J. Embedded Systems, vol. 2008, Article ID 594129, 2008.- [10] J. Brandt and K. Schneider, "How Different Are Esterel and SystemC?"
Forum on Specification and Design Languages, Electronic Chips and Systems Design Initiative, pp. 98-103, 2007.- [11] J. Brandt and K. Schneider, "Separate Translation of Synchronous Programs to Guarded Actions," Internal Report 382/11, Dept. of Computer Science, Univ. of Kaiserslautern, Mar. 2011.
- [12] C.G. Cassandras and S. Lafortune,
Introduction to Discrete Event Systems, second ed. Springer, 2008.- [13] K.M. Chandy and J. Misra,
Parallel Program Design. Addison-Wesley, May 1989.- [14] D.L. Dill, "The Murphi Verification System,"
Proc. Eighth Int'l Conf. Computer Aided Verification, pp. 390-393, 1996.- [15] A. Gamatie,
Designing Embedded Systems with the SIGNAL Programming Language. Springer, 2010.- [16] A. Gamatié, T. Gautier, P. Le Guernic, and J.P. Talpin, "Polychronous Design of Embedded Real-Time Applications,"
ACM Trans. Software Eng. and Methodology, vol. 16, no. 2, Apr. 2007.- [17] A. Girault, B. Lee, and E.A. Lee, "Hierarchical Finite State Machines with Multiple Concurrency Models,"
IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 18, no. 6, pp. 742-760, June 1999.- [18] N. Halbwachs,
Synchronous Programming of Reactive Systems. Kluwer, 1993.- [19] N. Halbwachs, "A Synchronous Language at Work: The Story of Lustre,"
Proc. ACM/IEEE Second Int'l Conf. Formal Methods and Models for Co-Design, pp. 3-11, 2005.- [20] N. Halbwachs and S. Baghdadi, "Synchronous Modelling of Asynchronous Systems,"
Proc. Second Int'l Conf. Embedded Software, pp. 240-251, 2002.- [21] N. Halbwachs and L. Mandel, "Simulation and Verification of Asynchronous Systems by Means of a Synchronous Model,"
Proc. Sixth Int'l Conf. Application of Concurrency to System Design, pp. 3-14, 2006.- [22] D. Harel and A. Naamad, "The STATEMATE Semantics of Statecharts,"
ACM Trans. Software Eng. and Methodology, vol. 5, no. 4, pp. 293-333, 1996.- [23] A. Jantsch,
Modeling Embedded Systems and SoCs. Morgan Kaufmann, 2004.- [24] B.A. Jose and S.K. Shukla, "An Alternative Polychronous Model and Synthesis Methodology for Model-Driven Embedded Software,"
Proc. Asia and South Pacific Design Automation Conf., vol. 24, pp. 13-18, 2010.- [25] H. Järvinen and R. Kurki-Suonio, "The DisCo Language and Temporal Logic of Actions," Technical Report 11, Tampere Univ. of Technology, Software Systems Laboratory, 1990.
- [26] P. Le Guernic, T. Gauthier, M. Le Borgne, and C. Le Maire, "Programming Real-Time Applications with SIGNAL,"
Proc. IEEE, vol. 79, no. 9, pp. 1321-1336, Sept. 1991.- [27] P. Le Guernic, J.-P. Talpin, and J.-C. Le Lann, "Polychrony for System Design,"
J. Circuits, Systems, and Computers, vol. 12, no. 3, pp. 261-304, June 2003.- [28] E.A. Lee and T. Parks, "Dataflow Process Networks,"
Proc. IEEE, vol. 83, no. 5, pp. 773-801, May 1995.- [29] E.A. Lee and A. Sangiovanni-Vincentelli, "A Framework for Comparing Models of Computation,"
IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 17, no. 12, pp. 1217-1229, Dec. 1998.- [30] G. Logothetis and K. Schneider, "Exact High Level WCET Analysis of Synchronous Programs by Symbolic State Space Exploration,"
Proc. Conf. Design, Automation and Test in Europe, pp. 10196-10203, 2003.- [31] R. Milner, "On Relating Synchrony and Asynchrony," Technical Report CSR- 75-80, Dept. of Computer Science, Univ. of Edinburgh, 1981.
- [32] R. Milner, "Calculi for Synchrony and Asynchrony,"
Theoretical Computer Science, vol. 25, no. 3, pp. 267-310, 1983.- [33] Object Management Group, "Modeling and Analysis of Real-Time and Embedded Systems (MARTE)," http://www.omg.org/ omgmarte/DocumentsSpecifications , June 2008.
- [34] F. Rocheteau and N. Halbwachs, "Implementing Reactive Programs on Circuits: A Hardware Implementation of LUSTRE,"
Real-Time: Theory in Practice, J.W. de Bakker, C. Huizing, W.P. de Roever, and G. Rozenberg, eds., pp. 195-208, Springer, 1992.- [35] K. Schneider, "A Verified Hardware Synthesis for Esterel,"
Proc. Int'l Workshop Distributed and Parallel Embedded Systems, pp. 205-214, 2000.- [36] K. Schneider, "Embedding Imperative Synchronous Languages in Interactive Theorem Provers,"
Proc. Second Int'l Conf. Application of Concurrency to System Design, pp. 143-154, 2001.- [37] K. Schneider, "Improving Automata Generation for Linear Temporal Logic by Considering the Automata Hierarchy,"
Proc. Int'l Conf. Logic for Programming, Artificial Intelligence, and Reasoning, vol. 2250, pp. 39-54, 2001.- [38] K. Schneider, "Proving the Equivalence of Microstep and Macrostep Semantics,"
Proc. Int'l Conf. Theorem Proving in Higher Order Logics, vol. 2410, pp. 314-331, 2002.- [39] K. Schneider, "The Synchronous Programming Language Quartz," Internal Report 375, Dept. of Computer Science, Univ. of Kaiserslautern, Dec. 2009.
- [40] K. Schneider, J. Brandt, and T. Schuele, "Causality Analysis of Synchronous Programs with Delayed Actions,"
Proc. Int'l Conf. Compilers, Architecture, and Synthesis for Embedded Systems, pp. 179-189, 2004.- [41] K. Schneider, J. Brandt, and T. Schuele, "A Verified Compiler for Synchronous Programs with Local Declarations,"
Electronic Notes in Theoretical Computer Science, vol. 153, no. 4, pp. 71-97, 2006.- [42] B.L. Titzer and J. Palsberg, "Nonintrusive Precision Instrumentation of Microcontroller Software,"
Proc. ACM SIGPLAN/SIGBED Conf. Languages, Compilers, and Tools for Embedded Systems, pp. 59-68, 2005. |