Abstract
Synchronous languages, such as the recently proposed SCCharts language, have been designed for the rigorous specification of real-time systems. Their sound semantics, which build on an abstraction from physical execution time, make these languages appealing, in particular for safety-critical systems. However, they traditionally lack built-in support for physical time. This makes it rather cumbersome to express things like timeouts or periodic executions within the language.
We here propose several mechanisms to reconcile the synchronous paradigm with physical time. Specifically, we propose extensions to the SCCharts language to express clocks and execution periods within the model. We draw on several sources, in particular timed automata, the Clock Constraint Specification Language, and the recently proposed concept of dynamic ticks. We illustrate how these extensions can be mapped to the SCChart language core, with minimal requirements on the runtime system, and we argue that the same concepts could be applied to other synchronous languages such as Esterel, Lustre, or SCADE.
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 SCCharts float is an abstract floating point number without actual precision limitations. We consider the choice of an actual data type orthogonal to the general concept presented here.
- 2.
References
Altisen, K., & Tripakis, S. (2005). Implementation of timed automata: An issue of semantics or modeling? In Formal Modeling and Analysis of Timed Systems (pp. 273–288). Berlin: Springer.
Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P.-H., Nicollin, X., et al. (1995). The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138(1), 3–34.
Alur, R., & Dill, D. L. (1994). A theory of timed automata. Theoretical Computer Science, 126, 183–235.
André, C. (2009). Syntax and semantics of the clock constraint specification language (CCSL). Research Report RR-6925, INRIA.
Benveniste, A., Caspi, P., Edwards, S. A., Halbwachs, N., Le Guernic, P., & de Simone, R. (2003, January). The synchronous languages twelve years later. In Proceedings of the IEEE, Special Issue on Embedded Systems (Vol. 91, pp. 64–83), Piscataway, NJ: IEEE.
Berry, G., & Sentovich, E. (2001). Multiclock Esterel. In CHARME ’01: Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (pp. 110–125), London: Springer.
Bourke, T., & Pouzet, M. (2013, April). Zélus: A synchronous language with odes. In Proceedings of the 16th international Conference on Hybrid Systems: Computation and Control, HSCC 2013, Philadelphia, PA (pp. 113–118).
Bourke, T., & Sowmya, A. (2009, November). Delays in Esterel. In SYNCHRON’09—Proceedings of Dagstuhl Seminar 09481, number 09481 in Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl (pp. 22–27).
Colaço, J.-L., Pagano, B., & Pouzet, M. (2017, September). SCADE 6: A formal language for embedded critical software development (invited paper). In 11th International Symposium on Theoretical Aspects of Software Engineering TASE, Sophia Antipolis (pp. 1–11).
Deantoni, J., & Mallet, F. (2012). Timesquare: Treat your models with logical time. In 50th International Conference on Objects, Models, Components, Patterns (TOOLS). Lecture Notes in Computer Science (Vol. 7304, pp. 34–41). Berlin: Springer.
Eidson, J., Lee, E. A., Matic, S., Seshia, S., & Zou, J. (2012, January). Distributed real-time software for cyber-physical systems. Proceedings of the IEEE, 100(1), 45–59.
Gamatié, A., & Gautier, T. (2010). The Signal synchronous multiclock approach to the design of distributed embedded systems. IEEE Transactions on Parallel and Distributed Systems, 21(5), 641–657.
Harel, D. (1987, June). Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3), 231–274.
Henzinger, T. A., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic model checking for real-time systems. Information and Computation, 111(2), 193–244.
Jourdan, M., Maraninchi, F., & Olivero, A. (1993, June/July). Verifying quantitative real-time properties of synchronous programs. In Proceedings of Computer Aided Verification (CAV’93). LNCS (Vol. 697, pp. 347–358).
Lamport, L. (1978, July). Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7), 558–565.
Le Guernic, P., Talpin, J.-P., & Le Lann, J.-C. ( 2003). POLYCHRONY for system design. Journal of Circuits, Systems, and Computers, 12(3), 261–304.
Lee, E. A. (2006). The problem with threads. IEEE Computer, 39(5), 33–42.
Lee, E. A., & Seshia, S. A. (2017). Introduction to Embedded Systems, A Cyber-Physical Systems Approach (2nd ed.). Cambridge: MIT Press.
Mallet, F., & de Simone, R. (2015). Correctness issues on MARTE/CCSL constraints. Science of Computer Programming, 106, 78–92.
Olivero, A., Sifakis, J., & Yovine, S. (1994). Using abstractions for the verification of linear hybrid systems. In Proceedings of the 6th Annual Conference on Computer-Aided Verification, Lecture Notes in Computer Science 818 (pp. 81–94). Berlin: Springer.
Schulz-Rosengarten, A., Smyth, S., von Hanxleden, R., & Mendler, M. (2018, June). On reconciling concurrency, sequentiality and determinacy for reactive systems — A sequentially constructive circuit semantics for Esterel. In 2018 18th International Conference on Application of Concurrency to System Design (ACSD) (pp. 95–104).
Schulz-Rosengarten, A., Smyth, S., von Hanxleden, R., & Mendler, M. (2018, February). A sequentially constructive circuit semantics for Esterel. Technical Report 1801, Christian-Albrechts-Universität zu Kiel, Department of Computer Science. ISSN 2192-6247.
Suryadevara, J., Seceleanu, C. C., Mallet, F., & Pettersson, P. (2013, September). Verifying MARTE/CCSL mode behaviors using UPPAAL. In Software Engineering and Formal Methods. Lecture Notes in Computer Science (Vol. 8137, pp. 1–15). Berlin: Springer.
von Hanxleden, R., Bourke, T., & Girault, A. (2017, September). Real-time ticks for synchronous programming. In Proceedings of the Forum on Specification and Design Languages (FDL ’17), Verona.
von Hanxleden, R., Duderstadt, B., Motika, C., Smyth, S., Mendler, M., Aguado, J., et al. (2014, June). SCCharts: Sequentially Constructive Statecharts for safety-critical applications. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’14), Edinburgh (pp. 372–383). New York: ACM.
Zeigler, B. P. (1976). Theory of Modeling and Simulation. New York: Wiley.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Schulz-Rosengarten, A., von Hanxleden, R., Mallet, F., de Simone, R., Deantoni, J. (2020). Time in SCCharts. In: Kazmierski, T., Steinhorst, S., Große, D. (eds) Languages, Design Methods, and Tools for Electronic System Design. Lecture Notes in Electrical Engineering, vol 611. Springer, Cham. https://doi.org/10.1007/978-3-030-31585-6_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-31585-6_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-31584-9
Online ISBN: 978-3-030-31585-6
eBook Packages: EngineeringEngineering (R0)