Document Open Access Logo

A Formal Link Between Response Time Analysis and Network Calculus

Authors Pierre Roux , Sophie Quinton , Marc Boyer

PDF
Thumbnail PDF

File

LIPIcs.ECRTS.2022.5.pdf
  • Filesize: 0.84 MB
  • 22 pages

Document Identifiers

Author Details

Pierre Roux
  • ONERA, Toulouse, France
  • DTIS - Université de Toulouse, F-31055 Toulouse, France
Sophie Quinton
  • Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, F-38000 Grenoble, France
Marc Boyer
  • ONERA, Toulouse, France
  • DTIS - Université de Toulouse, F-31055 Toulouse, France

Funding

This work has been partially supported by the French national research organization ANR (grant ANR-17-CE25-0016) through the RT-PROOFS project.

Cite AsGet BibTex

Pierre Roux, Sophie Quinton, and Marc Boyer. A Formal Link Between Response Time Analysis and Network Calculus. In 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 231, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECRTS.2022.5

Abstract

Classical Response Time Analysis (RTA) and Network Calculus (NC) are two major formalisms used for the verification of real-time properties. We offer mathematical links between these two different theories. Based on these links, we then prove the equivalence of various key notions in both frameworks. This enables specialists of both formalisms to get increase confidence on their models, or even, like the authors, to discover errors in theorems by investigating apparent discrepancies between some notions expected to be equivalent. The presented mathematical results are all mechanically checked with the interactive theorem prover Coq, building on existing formalizations of RTA and NC. Establishing such a link between NC and RTA paves the way for improved real-time analyses obtained by combining both theories to enjoy their respective strengths (e.g., multicore analyses for RTA or clock drifts for NC).

Subject Classification

ACM Subject Classification
  • Computer systems organization → Real-time system specification
  • Networks → Formal specifications
  • Software and its engineering → Formal methods
  • General and reference → Verification
Keywords
  • Response Time Analysis
  • Network Calculus
  • dense time
  • discrete time
  • response time
  • formal proof
  • Coq

Metrics

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

Supplementary Materials

References

  1. 28th Euromicro Conference on Real-Time Systems, ECRTS 2016, Toulouse, France, July 5-8, 2016. IEEE Computer Society, 2016. URL: https://ieeexplore.ieee.org/xpl/conhome/7557819/proceeding.
  2. Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. Competing inheritance paths in dependent type theory: a case study in functional analysis. In IJCAR 2020 - International Joint Conference on Automated Reasoning, pages 1-19, Paris, France, June 2020. URL: https://hal.inria.fr/hal-02463336.
  3. Anne Bouillard, Marc Boyer, and Euriell Le Corronc. Deterministic Network Calculus: From Theory to Practical Implementation. John Wiley & Sons, Ltd, October 2018. URL: https://doi.org/10.1002/9781119440284.
  4. Anne Bouillard and Éric Thierry. An algorithmic toolbox for network calculus. Discrete Event Dynamic Systems, 18(1):3-49, October 2008. http://www.springerlink.com/content/ 876x51r6647r8g68/. URL: https://doi.org/10.1007/s10626-007-0028-x.
  5. Khaoula Boukir, Jean-Luc Béchennec, and Anne-Marie Déplanche. Requirement specification and model-checking of a real-time scheduler implementation. In Liliana Cucu-Grosjean, Roberto Medina, Sebastian Altmeyer, and Jean-Luc Scharbarg, editors, 28th International Conference on Real Time Networks and Systems, RTNS 2020, Paris, France, June 10, 2020, pages 89-99. ACM, 2020. URL: https://doi.org/10.1145/3394810.3394817.
  6. Marc Boyer and Pierre Roux. Embedding network calculus and event stream theory in a common model. In Proc. of the 21st IEEE Int. Conf. on Emerging Technologies and Factory Automation (ETFA 2016), Berlin, Germany, September 2016. URL: https://doi.org/10.1109/ETFA.2016.7733565.
  7. Sergey Bozhko and Björn B. Brandenburg. Abstract response-time analysis: A formal foundation for the busy-window principle. In Marcus Völp, editor, 32nd Euromicro Conference on Real-Time Systems, ECRTS 2020, July 7-10, 2020, Virtual Conference, volume 165 of LIPIcs, pages 22:1-22:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ECRTS.2020.22.
  8. Felipe Cerqueira, Geoffrey Nelissen, and Björn B. Brandenburg. On Strong and Weak Sustainability, with an Application to Self-Suspending Real-Time Tasks. In Sebastian Altmeyer, editor, 30th Euromicro Conference on Real-Time Systems (ECRTS 2018), volume 106 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:21, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ECRTS.2018.26.
  9. Felipe Cerqueira, Felix Stutz, and Björn B Brandenburg. PROSA: A case for readable mechanized schedulability analysis. In 2016 28th Euromicro Conference on Real-Time Systems (ECRTS), pages 273-284. IEEE, 2016. Google Scholar
  10. The Coq development team. The Coq proof assistant reference manual, 2020. Version 8.13. URL: https://coq.inria.fr.
  11. Pascal Fradet, Xiaojie Guo, Jean-François Monin, and Sophie Quinton. Certican: A tool for the coq certification of CAN analysis results. In 25th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2019, Montreal, QC, Canada, April 16-18, 2019, pages 182-191, 2019. URL: https://doi.org/10.1109/RTAS.2019.00023.
  12. Pascal Fradet, Maxime Lesourd, Jean-François Monin, and Sophie Quinton. A generic coq proof of typical worst-case analysis. In 2018 IEEE Real-Time Systems Symposium, RTSS 2018, Nashville, TN, USA, December 11-14, 2018, pages 218-229. IEEE Computer Society, 2018. URL: https://doi.org/10.1109/RTSS.2018.00039.
  13. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. Certikos: An extensible architecture for building certified concurrent OS kernels. In Kimberly Keeton and Timothy Roscoe, editors, 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016, pages 653-669. USENIX Association, 2016. URL: https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu.
  14. Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, and Zhong Shao. Integrating Formal Schedulability Analysis into a Verified OS Kernel. In Computer Aided Verification, pages 496-514, New York, United States, July 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_28.
  15. Xiaojie Guo, Lionel Rieg, and Paolo Torrini. A generic approach for the certified schedulability analysis of software systems. In RTCSA 2021 - 27th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, pages 1-10, Houston (online), United States, August 2021. URL: https://hal.archives-ouvertes.fr/hal-03540548.
  16. ITU-T. Definitions and terminology for synchronization networks. Technical Report Recommendation G.810, International telecommunication union (ITU), 1996. Google Scholar
  17. Leonie Köhler, Borislav Nikolić, and Marc Boyer. Increasing accuracy of timing models: From cpa to cpa+. In Proc. of the Design, Automation and Test in Europe Conference and Exhibition (DATE), Florence, Italy, March 2019. Google Scholar
  18. Simon Künzli, Arne Hamann, Rolf Ernst, and Lothar Thiele. Combined approach to system level performance analysis of embedded systems. In Soonhoi Ha, Kiyoung Choi, Nikil D. Dutt, and Jürgen Teich, editors, Proceedings of the 5th International Conference on Hardware/Software Codesign and System Synthesis, CODES+ISSS 2007, Salzburg, Austria, September 30 - October 3, 2007, pages 63-68. ACM, 2007. URL: https://doi.org/10.1145/1289816.1289835.
  19. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009. URL: https://doi.org/10.1145/1538788.1538814.
  20. Etienne Mabille, Marc Boyer, Loïc Fejoz, and Stephan Merz. Towards certifying network calculus. In Proc. of the 4th Conference on Interactive Theorem Proving (ITP 2013), Rennes, France, July 2013. Google Scholar
  21. Simon Perathoner, Ernesto Wandeler, Lothar Thiele, Arne Hamann, Simon Schliecker, Rafik Henia, Razvan Racu, Rolf Ernst, and Michael González Harbour. Influence of different system abstractions on the performance analysis of distributed real-time systems. In Proceedings of the 7th ACM & IEEE international conference on Embedded software (EMSOFT'07), pages 193-202, New York, NY, USA, 2007. ACM. URL: https://doi.org/10.1145/1289927.1289959.
  22. Lucien Rakotomalala, Marc Boyer, and Pierre Roux. Formal Verification of Real-time Networks. In JRWRTC 2019, Junior Workshop RTNS 2019, TOULOUSE, France, November 2019. URL: https://hal.archives-ouvertes.fr/hal-02449140.
  23. Lucien Rakotomalala, Pierre Roux, and Marc Boyer. Verifying min-plus computations with coq. In Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, and Ivan Perez, editors, NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings, volume 12673 of Lecture Notes in Computer Science, pages 287-303. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-76384-8_18.
  24. Jonas Rox and Rolf Ernst. Compositional performance analysis with improved analysis techniques for obtaining viable end-to-end latencies in distributed embedded systems. International Journal on Software Tools for Technology Transfer, 15(3):171-187, 2013. Google Scholar
  25. Ludovic Thomas and Jean-Yves Le Boudec. On time synchronization issues in time-sentive networks with regulators and nonideal clocks. Proceedings of the ACM on Measurement and Analysis of Computing SystemsJune 2020 Article No.: 27, 4(2), June 2020. URL: https://doi.org/10.1145/3392145.
  26. Makarius Wenzel. The Isabelle/Isar Reference Manual, 2021. Version 2021-1. URL: https://isabelle.in.tum.de.
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