Document Open Access Logo

Decentralised Runtime Verification of Timed Regular Expressions

Authors Victor Roussanaly, Yliès Falcone

PDF
Thumbnail PDF

File

LIPIcs.TIME.2022.6.pdf
  • Filesize: 0.84 MB
  • 18 pages

Document Identifiers

Author Details

Victor Roussanaly
  • Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, 38000 Grenoble, France
Yliès Falcone
  • Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, LIG, 38000 Grenoble, France

Funding

  • Roussanaly, Victor: H2020- ECSEL-2018-IA call – Grant Agreement number 826276 (CPS4EU).
  • Falcone, Yliès: H2020- ECSEL-2018-IA call – Grant Agreement number 826276 (CPS4EU), Région Auvergne-Rhône- Alpes - "Pack Ambition Recherche" programme, French ANR project ANR-20-CE39-0009 (SEVERITAS), LabEx PERSYVAL-Lab (ANR- 11-LABX-0025-01).

Cite AsGet BibTex

Victor Roussanaly and Yliès Falcone. Decentralised Runtime Verification of Timed Regular Expressions. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.TIME.2022.6

Abstract

Ensuring the correctness of distributed cyber-physical systems can be done at runtime by monitoring properties over their behaviour. In a decentralised setting, such behaviour consists of multiple local traces, each offering an incomplete view of the system events to the local monitors, as opposed to the standard centralised setting with a unique global trace. We introduce the first monitoring framework for timed properties described by timed regular expressions over a distributed network of monitors. First, we define functions to rewrite expressions according to partial knowledge for both the centralised and decentralised cases. Then, we define decentralised algorithms for monitors to evaluate properties using these functions, as well as proofs of soundness and eventual completeness of said algorithms. Finally, we implement and evaluate our framework on synthetic timed regular expressions, giving insights on the cost of the centralised and decentralised settings and when to best use each of them.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Theory of computation → Regular languages
  • Theory of computation → Rewrite systems
  • Theory of computation → Automata over infinite objects
  • Computer systems organization → Real-time system specification
Keywords
  • Timed expressions
  • Timed properties
  • Monitoring
  • Runtime verification
  • Decentralized systems
  • Asynchronous communication

Metrics

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

References

  1. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pages 414-425, 1990. URL: https://doi.org/10.1109/LICS.1990.113766.
  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. Eugene Asarin, Paul Caspi, and Oded Maler. Timed regular expressions. J. ACM, 49(2):172-206, 2002. URL: https://doi.org/10.1145/506147.506151.
  4. Ezio Bartocci, Yliès Falcone, Adrian Francalanza, and Giles Reger. Introduction to runtime verification. In Ezio Bartocci and Yliès Falcone, editors, Lectures on Runtime Verification - Introductory and Advanced Topics, volume 10457 of Lecture Notes in Computer Science, pages 1-33. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-75632-5_1.
  5. Andreas Bauer, Martin Leucker, and Christian Schallhart. Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol., 20(4):14:1-14:64, September 2011. URL: https://doi.org/10.1145/2000799.2000800.
  6. Andreas Klaus Bauer and Yliès Falcone. Decentralised LTL monitoring. In Dimitra Giannakopoulou and Dominique Méry, editors, FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, volume 7436 of Lecture Notes in Computer Science, pages 85-100. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32759-9_10.
  7. Christian Colombo and Yliès Falcone. Organising LTL monitors over distributed systems with a global clock. Formal Methods Syst. Des., 49(1-2):109-158, 2016. URL: https://doi.org/10.1007/s10703-016-0251-x.
  8. Daniel de Leng and Fredrik Heintz. Approximate stream reasoning with metric temporal logic under uncertainty. In Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence and Thirty-First Innovative Applications of Artificial Intelligence Conference and Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, AAAI'19/IAAI'19/EAAI'19. AAAI Press, 2019. URL: https://doi.org/10.1609/aaai.v33i01.33012760.
  9. Antoine El-Hokayem and Yliès Falcone. On the monitoring of decentralized specifications: Semantics, properties, analysis, and simulation. ACM Trans. Softw. Eng. Methodol., 29(1):1:1-1:57, 2020. URL: https://doi.org/10.1145/3355181.
  10. Yliès Falcone. On decentralized monitoring. In Ayoub Nouri, Weimin Wu, Kamel Barkaoui, and ZhiWu Li, editors, Verification and Evaluation of Computer and Communication Systems - 15th International Conference, VECoS 2021, Virtual Event, November 22-23, 2021, Revised Selected Papers, volume 13187 of Lecture Notes in Computer Science, pages 1-16. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-98850-0_1.
  11. Yliès Falcone, Tom Cornebize, and Jean-Claude Fernandez. Efficient and generalized decentralized monitoring of regular languages. In Erika Ábrahám and Catuscia Palamidessi, editors, Formal Techniques for Distributed Objects, Components, and Systems - 34th IFIP WG 6.1 International Conference, FORTE 2014, Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014. Proceedings, volume 8461 of Lecture Notes in Computer Science, pages 66-83. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43613-4_5.
  12. Yliès Falcone, Klaus Havelund, and Giles Reger. A tutorial on runtime verification. In Manfred Broy, Doron A. Peled, and Georg Kalus, editors, Engineering Dependable Software Systems, volume 34 of NATO Science for Peace and Security Series, D: Information and Communication Security, pages 141-175. IOS Press, 2013. URL: https://doi.org/10.3233/978-1-61499-207-3-141.
  13. Yliès Falcone, Srdan Krstic, Giles Reger, and Dmitriy Traytel. A taxonomy for classifying runtime verification tools. Int. J. Softw. Tools Technol. Transf., 23(2):255-284, 2021. URL: https://doi.org/10.1007/s10009-021-00609-z.
  14. Florian Gallay and Yliès Falcone. Decentralized LTL enforcement. In Pierre Ganty and Davide Bresolin, editors, Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2021, Padua, Italy, 20-22 September 2021, volume 346 of EPTCS, pages 135-151, 2021. URL: https://doi.org/10.4204/EPTCS.346.9.
  15. Alejandro Grez, Filip Mazowiecki, Michal Pilipczuk, Gabriele Puppis, and Cristian Riveros. The monitoring problem for timed automata. CoRR, abs/2002.07049, 2020. URL: http://arxiv.org/abs/2002.07049.
  16. Dejan Nickovic and Oded Maler. AMT: a property-based monitoring tool for analog systems. In Jean-François Raskin and P. S. Thiagarajan, editors, Proceedings of the 5th International Conference on Formal modeling and analysis of timed systems (FORMATS 2007), volume 4763 of Lecture Notes in Computer Science, pages 304-319. Springer-Verlag, 2007. Google Scholar
  17. Srinivas Pinisetty, Thierry Jéron, Stavros Tripakis, Yliès Falcone, Hervé Marchand, and Viorel Preoteasa. Predictive runtime verification of timed properties. J. Syst. Softw., 132:353-365, 2017. URL: https://doi.org/10.1016/j.jss.2017.06.060.
  18. Prasanna Thati and Grigore Rosu. Monitoring algorithms for metric temporal logic specifications. Electronic Notes in Theoretical Computer Science, 113:145-162, 2005. URL: https://doi.org/10.1016/j.entcs.2004.01.029.
  19. Stavros Tripakis. Decentralized observation problems. In 44th IEEE IEEE Conference on Decision and Control and 8th European Control Conference Control, CDC/ECC 2005, Seville, Spain, 12-15 December, 2005, pages 6-11. IEEE, 2005. URL: https://doi.org/10.1109/CDC.2005.1582122.
  20. Stavros Tripakis and Karen Rudie. Decentralized observation of discrete-event systems: At least one can tell. IEEE Control. Syst. Lett., 6:1652-1657, 2022. URL: https://doi.org/10.1109/LCSYS.2021.3130887.
  21. Dogan Ulus. Montre: A tool for monitoring timed regular expressions. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 of Lecture Notes in Computer Science, pages 329-335. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63387-9_16.
  22. Yin Wang, Tae-Sic Yoo, and Stéphane Lafortune. Diagnosis of discrete event systems using decentralized architectures. Discret. Event Dyn. Syst., 17(2):233-263, 2007. URL: https://doi.org/10.1007/s10626-006-0006-8.
  23. Xiang Yin and Stéphane Lafortune. Codiagnosability and coobservability under dynamic observations: Transformation and verification. Autom., 61:241-252, 2015. URL: https://doi.org/10.1016/j.automatica.2015.08.023.
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