Abstract
Semantics for synchronous programming languages are well known. They capture the execution behaviour of reactive systems using precise formal operational or denotational models for verification and unambiguous semantics-preserving compilation. As synchronous programs are highly time critical, there is an imminent need for the development of an execution time aware semantics that can be used as the formal basis of WCET tools. To this end we propose such a compositional semantics for synchronous programs. Our approach, which is algebraic and based on formal power series in min-max-plus algebra, combines in one setting both the linear system theory for timing and constructive Gödel-Dummet logic for functional specification of synchronisation behaviour. The developed semantics is illustrated using a running example in the SCCharts language.
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
Similar content being viewed by others
Notes
- 1.
In [3] the constants \(-\infty \) and 0 are symbolised as \(\epsilon \) and e, respectively. Alain Girault suggested to us the notation
and
which we find more suggestive.
References
Andalam, S., Roop, P.S., Girault, A.: Pruning infeasible paths for tight wcrt analysis of synchronous programs. In: Design, Automation Test in Europe Conference (DATE), pp. 1–6, March 2011
André, C.: Synccharts: A visual representation of reactive behaviors. Rapport de recherche tr95-52, Université de Nice-Sophia Antipolis (1995)
Baccelli, F.L., Cohen, G., Olsder, G.J., Quadrat, J.-P.: Synchronisation and Linearity. Wiley, Chichester (1992)
Benvenist, A., Caspi, P., Edwards, S.A., Halbwachs, N., Le Guernic, P., de Simone, R.: The synchronous languages 12 years later. Proc. IEEE 91(1), 64–83 (2003)
Berry, G.: The foundations of Esterel. In: Proof, Language, and Interaction, pp. 425–454 (2000)
Blieberger, J.: Data-flow frameworks for worst-case execution time analysis. Real-Time Syst. 22(3), 183–227 (2002)
Cassez, F., Béchennec, J.-L.: Timing analysis of binary programs with UPPAAL. In: ACSD, pp. 41–50 (2013)
Dalsgaard, A.E., Olesen, M., Toft, M., Hansen, R.R., Larsen, K.G.: Metamoc: modular execution time analysis using model checking. In: OASIcs-OpenAccess Series in Informatics, vol. 15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2010)
Dummett, M.: A propositional calculus with a denumerable matrix. J. Symbolic Logic 24, 97–106 (1959)
Edwards, S.A., Lee, E.A.: The case for the precision timed (PRET) machine. In: Proceedings of the 44th Annual Design Automation Conference, pp. 264–265. ACM (2007)
Fuhrmann, I., Broman, D., Smyth, S., von Hanxleden, R.: Towards interactive timing analysis for designing reactive systems. Reconciling performace and predictability (RePP 2014) satellite event of ETAPS 2014. Technical report, Also as Technical report: EECS Department, University of California, Berkeley, UCB/EECS-2014-26 (2014)
Geilen, M., Stuijk, S.: Worst-case performance analysis of synchronous dataflow networks. In: CODES+ISSS 2010, Scottsdale, Arizona, USA, ACM, October 2010
De Groote, R., Hölzenspies, P.K.F., Kuper, J., Smit, G.J.M.: Incremental analysis of cyclo-static synchronous dataflow graphs. ACM Trans. Embed. Comput. Syst. (TECS) 14(4), 68 (2015)
Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)
Ju, L., Huynh, B.K., Chakraborty, S., Roychoudhury, A.: Context-sensitive timing analysis of Esterel programs. In: Proceedings of the 46th Annual Design Automation Conference, DAC 2009, pp. 870–873. ACM, New York, NY, USA (2009)
Logothetis, G., Schneider, K., Metzler, C.: Generating formal models for real-time verification by exact low-level runtime analysis of synchronous programs. In: International Real-Time Systems Symposium (RTSS), pp. 256–264. IEEE Computer Society, Cancun, Mexico (2003)
Maraninchi, F., Rémond, Y.: Argos: an automaton-based synchronous language. Comput. Lang. 27(1), 61–92 (2001)
Mendler, M., Roop, P.S., Bodin, B.: A novel wcert semantics of synchronous programs. Technical report, University of Bamberg, Nr. 101 (2016)
Mendler, M., von Hanxleden, R., Traulsen, C.: WCRT algebra and interfaces for Esterel-style synchronous processing. In: Proceedings of the Design, Automation and Test in Europe Conference (DATE 2009), Nice, France, April 2009
Raymond, P., Maiza, C., Parent-Vigouroux, C., Carrier, F., Asavoae, M.: Timing analysis enhancement for synchronous programs. Real-Time Syst. 51, 192–220 (2015)
Roop, P.S., Andalam, S., von Hanxleden, R., Yuan, S., Traulsen, C.: Tight WCRT analysis of synchronous C programs. In: Proceedings of the 2009 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems - CASES 2009, p. 205 (2009)
van Dalen, D.: Intuitionistic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. III, pp. 225–339. Reidel, Dordrecht (1986). Chap. 4
von Hanxleden, R., Duderstadt, B., Motika, C., Smyth, S., Mendler, M., Aguado, J., Mercer, S., O’Brien, O.: SCCharts: sequentially constructive statecharts for safety-critical applications. In: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2014). ACM, Edinburgh, UK, June 2014
Wang, J.J., Roop, P.S., Andalam, S.: ILPc: a novel approach for scalable timing analysis of synchronous programs. In: CASE 2013 (2013)
Acknowledgment
We thank our anonymous reviewers and Insa Fuhrmann for the constructive feedback. We acknowledge the Precision-Timed Synchronous Reactive Processing (PRETSY2) project by the German Research Foundation DFG (ME 1427/6-2, HA 4407/6-2). Partha Roop acknowledges the research and study leave from Auckland University. Bruno Bodin acknowledges funding from the EPSRC grant PAMELA EP/K008730/1.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Mendler, M., Roop, P.S., Bodin, B. (2016). A Novel WCET Semantics of Synchronous Programs. In: Fränzle, M., Markey, N. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2016. Lecture Notes in Computer Science(), vol 9884. Springer, Cham. https://doi.org/10.1007/978-3-319-44878-7_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-44878-7_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-44877-0
Online ISBN: 978-3-319-44878-7
eBook Packages: Computer ScienceComputer Science (R0)