Document Open Access Logo

TESL: A Model with Metric Time for Modeling and Simulation

Authors Hai Nguyen Van , Frédéric Boulanger , Burkhart Wolff

PDF
Thumbnail PDF

File

LIPIcs.TIME.2020.15.pdf
  • Filesize: 1.54 MB
  • 15 pages

Document Identifiers

Author Details

Hai Nguyen Van
  • Université Paris-Saclay, CNRS, LRI, Orsay, France
Frédéric Boulanger
  • Université Paris-Saclay, CNRS, LRI, CentraleSupélec, Orsay, France
Burkhart Wolff
  • Université Paris-Saclay, CNRS, LRI, Orsay, France

Cite AsGet BibTex

Hai Nguyen Van, Frédéric Boulanger, and Burkhart Wolff. TESL: A Model with Metric Time for Modeling and Simulation. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.TIME.2020.15

Abstract

Real-time and distributed systems are increasingly finding their way into critical embedded systems. On one side, computations need to be achieved within specific time constraints. On the other side, computations may be spread among various units which are not necessarily sharing a global clock. Our study is focused on a specification language - named TESL - used for coordinating concurrent models with timed constraints. We explore various questions related to time when modeling systems, and aim at showing that TESL can be introduced as a reasonable balance of expressiveness and decidability to tackle issues in complex systems. This paper introduces (1) an overview of the TESL language and its main properties (polychrony, stutter-invariance, coinduction for simulation), (2) extensions to the language and their applications.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
Keywords
  • Timed Systems
  • Semantics
  • Models
  • Simulation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Rajeev Alur. Timed automata. In Nicolas Halbwachs and Doron Peled, editors, Computer Aided Verification, pages 8-22, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. Google Scholar
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  3. A. Benveniste, P. Caspi, S. A. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone. The synchronous languages 12 years later. Proceedings of the IEEE, 91(1):64-83, 2003. Google Scholar
  4. Béatrice Bérard, Michel Bidoit, Alain Finkel, François Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, and Pierre McKenzie. Systems and Software Verification. Springer Berlin Heidelberg, 2001. URL: https://doi.org/10.1007/978-3-662-04558-9.
  5. G. Berry. The constructive semantics of pure Esterel, 1996. Google Scholar
  6. Gérard Berry. The foundations of Esterel. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, pages 425-454. MIT Press, Cambridge, MA, USA, 2000. Google Scholar
  7. Gérard Berry. SCADE: Synchronous design and validation of embedded control software. In S. Ramesh and Prahladavaradan Sampath, editors, Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems, pages 19-33, Dordrecht, 2007. Springer Netherlands. Google Scholar
  8. Frédéric Boulanger, Christophe Jacquet, Cécile Hardebolle, and Iuliana Prodan. TESL: a language for reconciling heterogeneous execution traces. In Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2014), pages 114-123, Lausanne, Switzerland, October 2014. URL: https://doi.org/10.1109/MEMCOD.2014.6961849.
  9. Timothy Bourke and Marc Pouzet. Zélus: A synchronous language with odes. In Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC ’13, page 113–118, New York, NY, USA, 2013. Association for Computing Machinery. URL: https://doi.org/10.1145/2461328.2461348.
  10. Benoit Combemale, Betty H.C. Cheng, Robert B. France, Jean-Marc Jezequel, and Bernhard Rumpe. Globalizing Domain-Specific Languages, volume 9400 of LNCS, Programming and Software Engineering. Springer International Publishing, 2015. Google Scholar
  11. Julien Deantoni, Charles André, and Régis Gascon. CCSL denotational semantics. Research Report RR-8628, Inria, November 2014. URL: https://hal.inria.fr/hal-01082274.
  12. Julien DeAntoni and Frédéric Mallet. Timesquare: Treat your models with logical time. In Carlo A. Furia and Sebastian Nanz, editors, Objects, Models, Components, Patterns - 50th International Conference, TOOLS 2012, Prague, Czech Republic, May 29-31, 2012. Proceedings, volume 7304 of Lecture Notes in Computer Science, pages 34-41. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-30561-0_4.
  13. J. Eker, J. W. Janneck, E. A. Lee, Jie Liu, Xiaojun Liu, J. Ludvig, S. Neuendorffer, S. Sachs, and Yuhong Xiong. Taming heterogeneity - the ptolemy approach. Proceedings of the IEEE, 91(1):127-144, 2003. Google Scholar
  14. K. Erciyes. Distributed Real-Time Systems. Springer International Publishing, 2019. URL: https://doi.org/10.1007/978-3-030-22570-4.
  15. Sulaymon Eshkabilov. MATLAB®/Simulink® Essentials: MATLAB®/Simulink® for Engineering Problem Solving and Numerical Analysis. Lulu Publishing Services, November 2016. Google Scholar
  16. Kelly Garcés, Julien Deantoni, and Frédéric Mallet. A Model-Based Approach for Reconciliation of Polychronous Execution Traces. In SEAA 2011 - 37th EUROMICRO Conference on Software Engineering and Advanced Applications, Oulu, Finland, August 2011. IEEE. URL: https://hal.inria.fr/inria-00597981.
  17. P. Le Guernic, A. Benveniste, P. Bournai, and T. Gautier. Synchronous data flow programming with the language SIGNAL. IFAC Proceedings Volumes, 20(2):359-364, 1987. 2nd IFAC Workshop on Adaptive Systems in Control and Signal Processing 1986, Lund, Sweden, 30 June-2 July 1986. Google Scholar
  18. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 79(9):1305-1320, September 1991. Google Scholar
  19. Michael J W Hall. Concepts in special relativity. In General Relativity: An Introduction to Black Holes, Gravitational Waves, and Cosmology, 2053-2571, pages 1-1 to 1-11. Morgan & Claypool Publishers, 2018. URL: https://doi.org/10.1088/978-1-6817-4885-6ch1.
  20. Cécile Hardebolle and Frédéric Boulanger. Exploring multi-paradigm modeling techniques. SIMULATION: Transactions of The Society for Modeling and Simulation International, 85(11/12):688-708, November/December 2009. URL: https://doi.org/10.1177/0037549709105240.
  21. Yannick Hildenbrand. Ed-247 (vistas) gateway for hybrid test systems. In Aerospace Systems and Technology Conference. SAE International, October 2018. URL: https://doi.org/10.4271/2018-01-1949.
  22. Leslie Lamport. What good is temporal logic? Information Processing 83, R. E. A. Mason, ed., Elsevier Publishers, 83:657-668, May 1983. URL: https://www.microsoft.com/en-us/research/publication/good-temporal-logic/.
  23. Paul Le Guernic, Thierry Gautier, Jean-Pierre Talpin, and Loïc Besnard. Polychronous automata. In TASE 2015, 9th International Symposium on Theoretical Aspects of Software Engineering, pages 95-102, Nanjing, China, September 2015. IEEE Computer Society. Google Scholar
  24. E. A. Lee and D. G. Messerschmitt. Synchronous data flow. Proceedings of the IEEE, 75(9):1235-1245, 1987. Google Scholar
  25. Edward A. Lee and Alberto Sangiovanni-Vincentelli. A framework for comparing models of computation. IEEE Trans. CAD, 17(12), 1998. Google Scholar
  26. Frédéric Mallet, Julien Deantoni, Charles André, and Robert De Simone. The Clock Constraint Specification Language for building timed causality models. Innovations in Systems and Software Engineering, 6(1-2):99-106, March 2010. Google Scholar
  27. Frédéric Mallet and Robert de Simone. Correctness issues on MARTE/CCSL constraints. Science of Computer Programming, 106:78-92, 2015. Special Issue: Architecture-Driven Semantic Analysis of Embedded Systems. URL: https://doi.org/10.1016/j.scico.2015.03.001.
  28. Mathieu Montin and Marc Pantel. Mechanizing the denotational semantics of the clock constraint specification language. In El Hassan Abdelwahed, Ladjel Bellatreche, Mattéo Golfarelli, Dominique Méry, and Carlos Ordonez, editors, Model and Data Engineering, pages 385-400, Cham, 2018. Springer International Publishing. Google Scholar
  29. Hai Nguyen Van, Thibaut Balabonski, Frédéric Boulanger, Chantal Keller, Benoît Valiron, and Burkhart Wolff. A symbolic operational semantics for TESL. In Alessandro Abate and Gilles Geeraerts, editors, Formal Modeling and Analysis of Timed Systems, pages 318-334, Cham, 2017. Springer International Publishing. Google Scholar
  30. Tobias Nipkow and Gerwin Klein. Concrete Semantics: With Isabelle/HOL. Springer Publishing Company, Incorporated, 2014. Google Scholar
  31. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  32. Claire Pagetti, Julien Forget, Frédéric Boniol, Mikel Cordovilla, and David Lesens. Multi-task implementation of multi-periodic synchronous programs. Discrete Event Dynamic Systems, 21(3):307-338, 2011. URL: https://hal.inria.fr/inria-00638936.
  33. Kirill Rozhdestvensky, Vladimir Ryzhov, Tatiana Fedorova, Kirill Safronov, Nikita Tryaskin, Shaharin Anwar Sulaiman, Mark Ovinis, and Suhaimi Hassan. Description of the Wolfram SystemModeler, pages 23-87. Springer Singapore, Singapore, 2020. URL: https://doi.org/10.1007/978-981-15-2803-3_2.
  34. Werner Schutz. The Testability of Distributed Real-Time Systems. Kluwer Academic Publishers, USA, 1993. Google Scholar
  35. J. A. Stankovic. Misconceptions about real-time computing: a serious problem for next-generation systems. Computer, 21(10):10-19, 1988. Google Scholar
  36. Stephen Weeks. Whole-program compilation in mlton. In Proceedings of the 2006 Workshop on ML, ML ’06, page 1, New York, NY, USA, 2006. Association for Computing Machinery. URL: https://doi.org/10.1145/1159876.1159877.
  37. Sam Westrick, Rohan Yadav, Matthew Fluet, and Umut A. Acar. Disentanglement in nested-parallel programs. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371115.
  38. M. Zhang and F. Mallet. An executable semantics of Clock Constraint Specification Language and its applications. In Formal Techniques for Safety-Critical Systems: 4th International Workshop, FTSCS 2015, pages 37-51, Cham, 2016. Springer. Google Scholar
  39. Karl Johan Åström and Richard M. Murray. Feedback Systems. Princeton University Press, Princeton, 2010. URL: https://www.degruyter.com/view/title/563028.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact