Document Open Access Logo

Foundational Response-Time Analysis as Explainable Evidence of Timeliness

Authors Marco Maida, Sergey Bozhko, Björn B. Brandenburg

PDF
Thumbnail PDF

File

LIPIcs.ECRTS.2022.19.pdf
  • Filesize: 1.61 MB
  • 25 pages

Document Identifiers

Author Details

Marco Maida
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Sergey Bozhko
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
  • Saarbrücken Graduate School of Computer Science, Universität des Saarlandes, Germany
Björn B. Brandenburg
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Funding

This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 803111), and from the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - 391919384.

Acknowledgements

We thank Pierre Roux for introducing us to CoqEAL and the members of the joint ANR-DFG project RT-PROOFS for fruitful discussions.

Cite AsGet BibTex

Marco Maida, Sergey Bozhko, and Björn B. Brandenburg. Foundational Response-Time Analysis as Explainable Evidence of Timeliness. In 34th Euromicro Conference on Real-Time Systems (ECRTS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 231, pp. 19:1-19:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECRTS.2022.19

Abstract

The paper introduces foundational response-time analysis (RTA) as a means to produce strong and independently checkable evidence of temporal correctness. In a foundational RTA, each response-time bound calculated comes with an auto-generated certificate of correctness - a short and human-inspectable sequence of machine-checked proofs that formally show the claimed bound to hold. In other words, a foundational RTA yields explainable results that can be independently verified (e.g., by a certification authority) in a rigorous manner (with an automated proof checker). Consequently, the analysis tool itself does not need to be verified nor trusted. As a proof of concept, the paper presents POET, the first foundational RTA tool. POET generates certificates based on Prosa, the to-date largest verified framework for schedulability analysis, which is based on Coq. The trusted computing base is hence reduced to the Coq proof checker and its dependencies. POET currently supports two scheduling policies (earliest-deadline-first, fixed-priority), two preemption models (fully preemptive, fully non-preemptive), arbitrary deadlines, periodic and sporadic tasks, and tasks characterized by arbitrary arrival curves. The paper describes the challenges inherent in the development of a foundational RTA tool, discusses key design choices, and reports on its scalability.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Real-time systems
  • Software and its engineering → Formal software verification
Keywords
  • hard real-time systems
  • response-time analysis
  • uniprocessor
  • Coq
  • Prosa
  • fixed priority
  • EDF
  • preemptive
  • non-preemptive
  • verification

Metrics

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

Supplementary Materials

References

  1. Rajeev Alur and David L Dill. A theory of timed automata. Theoretical computer science, 126(2):183-235, 1994. Google Scholar
  2. Rajeev Alur, Thomas A Henzinger, and Pei-Hsin Ho. Automatic symbolic verification of embedded systems. IEEE Transactions on Software Engineering, 22(3):181-201, 1996. Google Scholar
  3. Andrew W Appel. Foundational proof-carrying code. In Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pages 247-256. IEEE, 2001. Google Scholar
  4. Jiri Barnat, Luboš Brim, Milan Ceška, and Tomáš Lamr. CUDA accelerated LTL model checking. In 2009 15th International Conference on Parallel and Distributed Systems, pages 34-41. IEEE, 2009. Google Scholar
  5. Gerd Behrmann, Alexandre David, Kim G Larsen, John Hakansson, Paul Petterson, Wang Yi, and Martijn Hendriks. UPPAAL 4.0. In Proceedings of the 3rd international conference on the Quantitative Evaluation of Systems, pages 125-126, 2006. Google Scholar
  6. Marc Boyer, Jorn Migge, and Marc Fumey. PEGASE-a robust and efficient tool for worst-case network traversal time evaluation on AFDX. Technical report, SAE Technical Paper, 2011. Google Scholar
  7. Marc Boyer, Pierre Roux, Hugo Daigmorte, and David Puechmaille. A residual service curve of rate-latency server used by sporadic flows computable in quadratic time for network calculus. In 33rd Euromicro Conference on Real-Time Systems (ECRTS 2021). Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. Google Scholar
  8. Sergey Bozhko and Björn B. Brandenburg. Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle. In 32nd Euromicro Conference on Real-Time Systems (ECRTS'20), July 7-10, 2020, Virtual Conference, 2020. Google Scholar
  9. Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W Appel. VST-Floyd: A separation logic tool to verify correctness of C programs. Journal of Automated Reasoning, 61(1):367-422, 2018. Google Scholar
  10. Felipe Cerqueira, Geoffrey Nelissen, and Björn B Brandenburg. On strong and weak sustainability, with an application to self-suspending real-time tasks. In 30th Euromicro Conference on Real-Time Systems (ECRTS), pages 26-1, 2018. Google Scholar
  11. 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
  12. Jian-Jia Chen and Björn B Brandenburg. A note on the period enforcer algorithm for self-suspending tasks. Leibniz Transactions on Embedded Systems, 4(1):01-1, 2017. Google Scholar
  13. Jian-Jia Chen, Geoffrey Nelissen, Wen-Hung Huang, Maolin Yang, Björn Brandenburg, Konstantinos Bletsas, Cong Liu, Pascal Richard, Frédéric Ridouard, Neil Audsley, et al. Many suspensions, many problems: a review of self-suspending tasks in real-time systems. Real-Time Systems, 55(1), 2019. Google Scholar
  14. Cyril Cohen, Maxime Dénès, and Anders Mörtberg. Refinements for free! In International Conference on Certified Programs and Proofs, pages 147-162. Springer, 2013. Google Scholar
  15. Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76(2):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  16. Thierry Coquand and Christine Paulin. Inductively defined types. In International Conference on Computer Logic, pages 50-66. Springer, 1988. Google Scholar
  17. Alexandre David, Kim G Larsen, Axel Legay, Marius Mikučionis, and Zheng Wang. Time for statistical model checking of real-time systems. In International Conference on Computer Aided Verification, pages 349-355. Springer, 2011. Google Scholar
  18. Robert I Davis, Alan Burns, Reinder J Bril, and Johan J Lukkien. Controller Area Network (CAN) schedulability analysis: Refuted, revisited and revised. Real-Time Systems, 35(3), 2007. Google Scholar
  19. Leonardo De Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pages 625-635. Springer, 2021. Google Scholar
  20. Daniel de Rauglaudre. Vérification formelle de conditions d'ordonnancabilité de tâches temps réel périodiques strictes. In JFLA-Journées Francophones des Langages Applicatifs-2012, 2012. Google Scholar
  21. Bruno Dutertre. The priority ceiling protocol: formalization and analysis using PVS. In Proceedings of the 21st IEEE Conference on Real-Time Systems Symposium (RTSS), pages 151-160, 1999. Google Scholar
  22. Pascal Fradet, Xiaojie Guo, Jean-François Monin, and Sophie Quinton. A generalized digraph model for expressing dependencies. In Proceedings of the 26th International Conference on Real-Time Networks and Systems, pages 72-82, 2018. Google Scholar
  23. Pascal Fradet, Xiaojie Guo, Jean-François Monin, and Sophie Quinton. CertiCAN: A tool for the Coq certification of CAN analysis results. In RTAS, 2019. Google Scholar
  24. 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), pages 218-229. IEEE, 2018. Google Scholar
  25. Georges Gonthier. Formal proof-the four-color theorem. Notices of the AMS, 55(11):1382-1393, 2008. Google Scholar
  26. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, Lecture Notes in Computer Science, pages 163-179, 2013. Google Scholar
  27. David Griffin, Iain Bate, and Robert I. Davis. Generating utilization vectors for the systematic evaluation of schedulability tests. In 41st IEEE Real-Time Systems Symposium (RTSS'20), December 1-4, Houston, TX, USA, pages 76-88. IEEE Computer Society, 2020. Google Scholar
  28. Arpan Gujarati, Felipe Cerqueira, Björn B Brandenburg, and Geoffrey Nelissen. Correspondence article: a correction of the reduction-based schedulability analysis for apa scheduling. Real-Time Systems, 55(1):136-143, 2019. Google Scholar
  29. Mario Günzel and Jian-Jia Chen. A note on slack enforcement mechanisms for self-suspending tasks. Real-Time Systems, pages 1-10, 2021. Google Scholar
  30. Thomas A Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. HyTech: A model checker for hybrid systems. International Journal on Software Tools for Technology Transfer, 1(1-2):110-122, 1997. Google Scholar
  31. Leandro Soares Indrusiak, Alan Burns, and Borislav Nikolic. Analysis of buffering effects on hard real-time priority-preemptive wormhole networks. arXiv preprint arXiv:1606.02942, 2016. Google Scholar
  32. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. seL4: Formal verification of an OS kernel. In SOSP, 2009. Google Scholar
  33. Simon Kramer, Dirk Ziegenbein, and Arne Hamann. Real world automotive benchmarks for free. In 6th International Workshop on Analysis Tools and Methodologies for Embedded and Real-time Systems (WATERS), 2015. Google Scholar
  34. Karthik Lakshmanan, Dionisio de Niz, and Ragunathan Rajkumar. Coordinated task scheduling, allocation and synchronization on multiprocessors. In RTSS, 2009. Google Scholar
  35. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009. Google Scholar
  36. Etienne Mabille, Marc Boyer, Loïc Fejoz, and Stephan Merz. Towards certifying network calculus. In ITP, 2013. Google Scholar
  37. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, 2021. URL: https://doi.org/10.5281/zenodo.4457887.
  38. George C Necula. Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 106-119, 1997. Google Scholar
  39. Christine Paulin-Mohring. Introduction to the calculus of inductive constructions, 2015. Google Scholar
  40. Prosa. URL: http://prosa.mpi-sws.org/.
  41. Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. RefinedC: automating the foundational verification of C code with refined ownership types. In PLDI, 2021. Google Scholar
  42. The Coq Proof Assistant. URL: https://coq.inria.fr.
  43. The Isabelle Proof Assistant. URL: https://isabelle.in.tum.de/.
  44. The Nqthm Theorem Prover. URL: https://www.cs.utexas.edu/users/moore/best-ideas/nqthm/index.html.
  45. The PVS Proof Assistant. URL: https://pvs.csl.sri.com/.
  46. Matthew Wilding. A machine-checked proof of the optimality of a real-time scheduling policy. In International Conference on Computer Aided Verification, pages 369-378. Springer, 1998. Google Scholar
  47. Simon Wimmer and Peter Lammich. Verified model checking of timed automata. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 61-78. Springer, 2018. Google Scholar
  48. Beyazit Yalcinkaya, Mitra Nasri, and Björn B Brandenburg. An exact schedulability test for non-preemptive self-suspending real-time tasks. In 2019 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 1228-1233. IEEE, 2019. Google Scholar
  49. Maolin Yang, Jian-Jia Chen, and Wen-Hung Huang. A misconception in blocking time analyses under multiprocessor synchronization protocols. Real-Time Systems, 53(2):187-195, 2017. Google Scholar
  50. Sergio Yovine. Kronos: A verification tool for real-time systems. International Journal on Software Tools for Technology Transfer, 1(1-2):123-133, 1997. Google Scholar
  51. Xingyuan Zhang, Christian Urban, and Chunhan Wu. Priority inheritance protocol proved correct. In International Conference on Interactive Theorem Proving, pages 217-232. Springer, 2012. Google Scholar
  52. Quan Zhou, Jihua Huang, Jianjun Li, and Zhi Li. Response time analysis for hybrid task sets under fixed priority scheduling. In Proceedings of the IEEE 28th Real-Time and Embedded Technology and Applications Symposium (RTAS), pages 108-120. IEEE Computer Society, 2022. Google Scholar
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