Skip to main content
Erschienen in:
Buchtitelbild

2020 | OriginalPaper | Buchkapitel

Time in SCCharts

verfasst von : Alexander Schulz-Rosengarten, Reinhard von Hanxleden, Frédéric Mallet, Robert de Simone, Julien Deantoni

Erschienen in: Languages, Design Methods, and Tools for Electronic System Design

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Fußnoten
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.
 
Literatur
1.
Zurück zum Zitat 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.CrossRef 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.CrossRef
2.
Zurück zum Zitat 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.MathSciNetCrossRef 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.MathSciNetCrossRef
3.
4.
Zurück zum Zitat André, C. (2009). Syntax and semantics of the clock constraint specification language (CCSL). Research Report RR-6925, INRIA. André, C. (2009). Syntax and semantics of the clock constraint specification language (CCSL). Research Report RR-6925, INRIA.
5.
Zurück zum Zitat 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. 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.
6.
Zurück zum Zitat 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. 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.
7.
Zurück zum Zitat 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., & 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).
8.
Zurück zum Zitat 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). 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).
9.
Zurück zum Zitat 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). 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).
10.
Zurück zum Zitat 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. 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.
11.
Zurück zum Zitat 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.CrossRef 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.CrossRef
12.
Zurück zum Zitat 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.CrossRef 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.CrossRef
13.
Zurück zum Zitat Harel, D. (1987, June). Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3), 231–274.MathSciNetCrossRef Harel, D. (1987, June). Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3), 231–274.MathSciNetCrossRef
14.
Zurück zum Zitat Henzinger, T. A., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic model checking for real-time systems. Information and Computation, 111(2), 193–244.MathSciNetCrossRef Henzinger, T. A., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic model checking for real-time systems. Information and Computation, 111(2), 193–244.MathSciNetCrossRef
15.
Zurück zum Zitat 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). 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).
16.
Zurück zum Zitat Lamport, L. (1978, July). Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7), 558–565.CrossRef Lamport, L. (1978, July). Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7), 558–565.CrossRef
17.
Zurück zum Zitat 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.CrossRef 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.CrossRef
18.
Zurück zum Zitat Lee, E. A. (2006). The problem with threads. IEEE Computer, 39(5), 33–42.CrossRef Lee, E. A. (2006). The problem with threads. IEEE Computer, 39(5), 33–42.CrossRef
19.
Zurück zum Zitat Lee, E. A., & Seshia, S. A. (2017). Introduction to Embedded Systems, A Cyber-Physical Systems Approach (2nd ed.). Cambridge: MIT Press.MATH Lee, E. A., & Seshia, S. A. (2017). Introduction to Embedded Systems, A Cyber-Physical Systems Approach (2nd ed.). Cambridge: MIT Press.MATH
20.
Zurück zum Zitat Mallet, F., & de Simone, R. (2015). Correctness issues on MARTE/CCSL constraints. Science of Computer Programming, 106, 78–92.CrossRef Mallet, F., & de Simone, R. (2015). Correctness issues on MARTE/CCSL constraints. Science of Computer Programming, 106, 78–92.CrossRef
21.
Zurück zum Zitat 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. 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.
22.
Zurück zum Zitat 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, 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).
23.
Zurück zum Zitat 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. 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.
24.
Zurück zum Zitat 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. 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.
25.
Zurück zum Zitat 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., 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.
26.
Zurück zum Zitat 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. 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.
27.
Zurück zum Zitat Zeigler, B. P. (1976). Theory of Modeling and Simulation. New York: Wiley.MATH Zeigler, B. P. (1976). Theory of Modeling and Simulation. New York: Wiley.MATH
Metadaten
Titel
Time in SCCharts
verfasst von
Alexander Schulz-Rosengarten
Reinhard von Hanxleden
Frédéric Mallet
Robert de Simone
Julien Deantoni
Copyright-Jahr
2020
DOI
https://doi.org/10.1007/978-3-030-31585-6_1

Neuer Inhalt