Abstract
The synchronous paradigm provides a logical abstraction of time for reactive system design which allows automatic synthesis of embedded programs that behave in a predictable, timely and reactive manner. According to the synchrony hypothesis, a synchronous model reacts to input events and generates outputs that are immediately made available. But even though synchrony greatly simplifies design of complex systems, it often leads to rejecting models when data dependencies within a reaction are ill-specified, leading to causal cycles. Constructivity is a key property to guarantee that the output during each reaction can be algorithmically determined. Polychrony deviates from perfect synchrony by using a partially ordered or relational model of time. It captures the behaviors of (implicitly) multi-clocked data-flow networks and can analyze and synthesize them to GALS systems or to Kahn process networks (KPNs). In this paper, we provide a unified constructive semantic framework, using structural operational semantics, which captures the behavior of both synchronous modules and multi-clocked polychronous processes. Along the way, we define the very first operational semantics of Signal.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berry, G.: The foundations of Esterel. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 425–454. MIT Press (1998)
Schneider, K.: The synchronous programming language Quartz. Internal Report 375, Department of Computer Science, University of Kaiserslautern (December 2009)
Halbwachs, N.: A synchronous language at work: the story of Lustre. In: Formal Methods and Models for Codesign (MEMOCODE), pp. 3–11. IEEE Computer Society (2005)
Titzer, B., Palsberg, J.: Nonintrusive precision instrumentation of microcontroller software. In: Paek, Y., Gupta, R. (eds.) Languages, Compilers, and Tools for Embedded Systems (LCTES), Chicago, Illinois, USA, pp. 59–68. ACM (2005)
Berry, G.: A hardware implementation of pure Esterel. Sadhana 17(1), 95–130 (1992)
Rocheteau, F., Halbwachs, N.: Pollux: A Lustre-based hardware design environment. In: Quinton, P., Robert, Y. (eds.) Algorithms and Parallel VLSI Architectures II, Gers, France, pp. 335–346. Elsevier (1992)
Schneider, K., Brandt, J., Schuele, T.: A verified compiler for synchronous programs with local declarations. Electronic Notes in Theoretical Computer Science 153, 71–97 (2006)
Logothetis, G., Schneider, K.: Exact high level WCET analysis of synchronous programs by symbolic state space exploration. In: Design, Automation and Test in Europe (DATE), pp. 10196–10203. IEEE Computer Society (2003)
Boldt, M., Traulsen, C., von Hanxleden, R.: Compilation and worst-case reaction time analysis for multithreaded Esterel processing. EURASIP Journal on Embedded Systems (2008)
Stok, L.: False loops through resource sharing. In: International Conference on Computer-Aided Design (ICCAD), pp. 345–348. IEEE Computer Society (1992)
Berry, G.: The constructive semantics of pure Esterel (July 1996), http://www-sop.inria.fr/meije/esterel/esterel-eng.html
Shiple, T., Berry, G., Touati, H.: Constructive analysis of cyclic circuits. In: European Design Automation Conference (EDAC), Paris, France, pp. 328–333. IEEE Computer Society (1996)
Edwards, S.: Making cyclic circuits acyclic. In: Design Automation Conference (DAC), Anaheim, California, USA, pp. 159–162. ACM (2003)
Schneider, K., Brandt, J., Schuele, T.: Causality analysis of synchronous programs with delayed actions. In: Compilers, Architecture, and Synthesis for Embedded Systems (CASES), Washington, District of Columbia, USA, pp. 179–189. ACM (2004)
Brzozowski, J., Seger, C.J.: Asynchronous Circuits. Springer (1995)
Le Guernic, P., Gauthier, T., Le Borgne, M., Le Maire, C.: Programming real-time applications with SIGNAL. Proceedings of the IEEE 79(9), 1321–1336 (1991)
Le Guernic, P., Benveniste, A.: Real-time, synchronous, data-flow programming: The language SIGNAL and its mathematical semantics. Research Report 533, INRIA (June 1986)
Besnard, L., Gautier, T., Le Guernic, P., Talpin, J.P.: Compilation of polychronous data flow equations. In: Shukla, S., Talpin, J.P. (eds.) Synthesis of Embedded Software – Frameworks and Methodologies for Correctness by Construction. Springer (2010)
Kautz, W.: The necessity of closed circuit loops in minimal combinational circuits. IEEE Transactions on Computers (T-C) C-19(2), 162–166 (1970)
Rivest, R.: The necessity of feedback in minimal monotone combinational circuits. IEEE Transactions on Computers (T-C) C-26(6), 606–607 (1977)
Malik, S.: Analysis of cycle combinational circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (T-CAD) 13(7), 950–956 (1994)
Bryant, R.: A switch level model and simulator for MOS digital systems. IEEE Transactions on Computers (T-C) C-33(2), 160–177 (1984)
Schneider, K., Brandt, J., Schuele, T., Tuerk, T.: Maximal causality analysis. In: Desel, J., Watanabe, Y. (eds.) Application of Concurrency to System Design (ACSD), Saint-Malo, France, pp. 106–115. IEEE Computer Society (2005)
Jose, B., Gamatie, A., Ouy, J., Shukla, S.: SMT based false causal loop detection during code synthesis from polychronous specifications. In: Singh, S. (ed.) Formal Methods and Models for Codesign (MEMOCODE), Cambridge, UK, pp. 109–118. IEEE Computer Society (2011)
Nanjundappa, M., Kracht, M., Ouy, J., Shukla, S.: Synthesizing embedded software with safety wrappers through polyhedral analysis in a polychronous framework. In: Electronic System Level Synthesis Conference (ESLsyn), pp. 1–6 (2012)
Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2), 285–309 (1955)
Brandt, J., Schneider, K.: Separate translation of synchronous programs to guarded actions. Internal Report 382/11, Department of Computer Science, University of Kaiserslautern, Kaiserslautern, Germany (March 2011)
SYNCHRON: The common format of synchronous languages - the declarative code DC. Technical report, C2A-SYNCHRON project (1998)
Dijkstra, E.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM (CACM) 18(8), 453–457 (1975)
Chandy, K., Misra, J.: Parallel Program Design. Addison-Wesley (May 1989)
Dill, D.: The Murφ Verification System. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 390–393. Springer, Heidelberg (1996)
Gamatié, A., Gautier, T., Le Guernic, P., Talpin, J.: Polychronous design of embedded real-time applications. ACM Transactions on Software Engineering and Methodology (TOSEM) 16(2) (2007)
Le Guernic, P., Talpin, J.P., Le Lann, J.C.: Polychrony for system design. Journal of Circuits, Systems, and Computers (JCSC) 12(3), 261–304 (2003)
Potop-Butucaru, D., Sorel, Y., de Simone, R., Talpin, J.P.: Correct-by-construction asynchronous implementation of modular synchronous specifications. Fundamenta Informaticae 108(1-2), 91–118 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Talpin, JP., Brandt, J., Gemünde, M., Schneider, K., Shukla, S. (2013). Constructive Polychronous Systems. In: Artemov, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 2013. Lecture Notes in Computer Science, vol 7734. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35722-0_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-35722-0_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35721-3
Online ISBN: 978-3-642-35722-0
eBook Packages: Computer ScienceComputer Science (R0)