Skip to main content
SpringerLink
Log in

Metric First-Order Temporal Logic with Complex Data Types

  • Conference paper
  • First Online:
Runtime Verification (RV 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14245))

Included in the following conference series:

Abstract

Temporal logics are widely used in runtime verification as they enable the creation of declarative and compositional specifications. However, their ability to model complex data is limited. One must resort to complicated encoding schemes to express properties involving basic structures such as lists or trees. To avoid this drawback, we extend metric first-order temporal logic with a minimalistic, yet expressive, functional programming language. The extension features an expressive collection of types including function, record, variant, and inductive types, as well as support for type inference and monitoring.

Our monitor implementation directly parses traces in the JSON format, based on the user’s type specification, which avoids a separate pre-processing step. We compare our approach to existing shallow embeddings of temporal properties in general-purpose host languages and to encodings into simple temporal logics. Specifically, our language benefits from a precise semantics and a good support for monitoring-specific static analysis.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Alur, R., Henzinger, T.A.: Real-time logics: complexity and expressiveness. Inf. Comput. 104(1), 35–77 (1993). https://doi.org/10.1006/inco.1993.1025

    Article  MathSciNet  MATH  Google Scholar 

  2. Basin, D., et al.: VeriMon: a formally verified monitoring tool. In: Seidl, H., Liu, Z., Pasareanu, C.S. (eds.) ICTAC 2022. LNCS, vol. 13572, pp. 1–6. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-17715-6_1

    Chapter  Google Scholar 

  3. Basin, D., et al.: A formally verified, optimized monitor for metric first-order dynamic logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 432–453. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51074-9_25

    Chapter  Google Scholar 

  4. Basin, D., et al.: Monitoring the internet computer. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 383–402. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-27481-7_22

    Chapter  Google Scholar 

  5. Basin, D., Klaedtke, F., Marinovic, S., Zălinescu, E.: Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Des. 46(3), 262–285 (2015). https://doi.org/10.1007/s10703-015-0222-7

    Article  MATH  Google Scholar 

  6. Basin, D., Klaedtke, F., Müller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1–15:45 (2015). https://doi.org/10.1145/2699444

  7. Basin, D., Klaedtke, F., Zalinescu, E.: The MonPoly monitoring tool. In: Reger, G., Havelund, K. (eds.) Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES). Kalpa, vol. 3, pp. 19–28. EasyChair (2017). https://doi.org/10.29007/89hs

  8. Blein, Y., Ledru, Y., du Bousquet, L., Groz, R.: Extending specification patterns for verification of parametric traces. In: Gnesi, S., Plat, N., Spoletini, P., Pelliccione, P. (eds.) Conference on Formal Methods in Software Engineering (FormaliSE), pp. 10–19. ACM (2018). https://doi.org/10.1145/3193992.3193998

  9. Ben Cheikh, A., Blein, Y., Chehida, S., Vega, G., Ledru, Y., du Bousquet, L.: An environment for the ParTraP trace property language (tool demonstration). In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 437–446. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03769-7_26

    Chapter  Google Scholar 

  10. Chen, K., Hudak, P., Odersky, M.: Parametric type classes. In: White, J.L. (ed.) Conference on Lisp and Functional Programming (LFP), pp. 170–181. ACM (1992). https://doi.org/10.1145/141471.141536

  11. Chomicki, J.: Efficient checking of temporal integrity constraints using bounded history encoding. ACM Trans. Database Syst. 20(2), 149–186 (1995). https://doi.org/10.1145/210197.210200

    Article  Google Scholar 

  12. Cok, D.R.: OpenJML: software verification for Java 7 using JML, OpenJDK, and eclipse. In: Dubois, C., Giannakopoulou, D., Méry, D. (eds.) Workshop on Formal Integrated Development Environment (F-IDE). EPTCS, vol. 149, pp. 79–92 (2014). https://doi.org/10.4204/EPTCS.149.8

  13. Damas, L., Milner, R.: Principal type-schemes for functional programs. In: DeMillo, R.A. (ed.) ACM Symposium on Principles of Programming Languages (POPL), pp. 207–212. ACM Press (1982). https://doi.org/10.1145/582153.582176

  14. D’Angelo, B., et al.: LOLA: runtime monitoring of synchronous systems. In: Symposium on Temporal Representation and Reasoning (TIME), pp. 166–174. IEEE (2005). https://doi.org/10.1109/TIME.2005.26

  15. Dybjer, P.: Representing inductively defined sets by wellorderings in Martin-Löf’s type theory. Theor. Comp. Sci. 176(1–2), 329–335 (1997). https://doi.org/10.1016/S0304-3975(96)00145-4

    Article  MathSciNet  MATH  Google Scholar 

  16. Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. Springer, Heidelberg (1979). https://doi.org/10.1007/3-540-09724-4

    Book  MATH  Google Scholar 

  17. Gorostiaga, F., Sánchez, C.: HLola: a very functional tool for extensible stream runtime verification. In: TACAS 2021. LNCS, vol. 12652, pp. 349–356. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72013-1_18

    Chapter  Google Scholar 

  18. Hallé, S., Khoury, R.: Event stream processing with BeepBeep 3. In: Reger, G., Havelund, K. (eds.) Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES). Kalpa, vol. 3, pp. 81–88. EasyChair (2017). https://doi.org/10.29007/4cth

  19. Harper, R.: Practical Foundations for Programming Languages, 2nd edn. Cambridge University Press, Cambridge (2016)

    Book  MATH  Google Scholar 

  20. Havelund, K.: Rule-based runtime verification revisited. Int. J. Softw. Tools Technol. Transf. 17(2), 143–170 (2015). https://doi.org/10.1007/s10009-014-0309-2

    Article  Google Scholar 

  21. Havelund, K., Peled, D., Ulus, D.: DejaVu: a monitoring tool for first-order temporal logic. In: Workshop on Monitoring and Testing of Cyber-Physical Systems (MT@CPSWeek), pp. 12–13. IEEE (2018). https://doi.org/10.1109/MT-CPS.2018.00013

  22. Kaletsch, N.: Formalizing typing rules for VeriMon. Bachelor thesis, ETH Zürich (2021)

    Google Scholar 

  23. Leucker, M., Sánchez, C., Scheffel, T., Schmitz, M., Schramm, A.: TeSSLa: runtime verification of non-synchronized real-time streams. In: Haddad, H.M., Wainwright, R.L., Chbeir, R. (eds.) ACM Symposium on Applied Computing (SAC), pp. 1925–1933. ACM (2018). https://doi.org/10.1145/3167132.3167338

  24. Lima Graf, J., Krstić, S., Schneider, J.: Metric first-order temporal logic with complex data types. Technical report, ETH Zürich (2023), https://bitbucket.org/jshs/monpoly/src/cmfodl2/paper.pdf

  25. Lima Graf, J., Krstić, S., Schneider, J.: MonPoly extended with complex data types (2023). https://bitbucket.org/jshs/monpoly/src/cmfodl2/

  26. Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348–375 (1978). https://doi.org/10.1016/0022-0000(78)90014-4

    Article  MathSciNet  MATH  Google Scholar 

  27. Morris Jr, J.H.: Lambda-calculus models of programming languages. Ph.D. thesis, MIT (1969)

    Google Scholar 

  28. Ohori, A.: A polymorphic record calculus and its compilation. ACM Trans. Program. Lang. Syst. 17(6), 844–895 (1995). https://doi.org/10.1145/218570.218572

    Article  Google Scholar 

  29. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  30. Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 345–359. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16612-9_26

    Chapter  Google Scholar 

  31. Signoles, J., Kosmatov, N., Vorobyov, K.: E-ACSL, a runtime verification tool for safety and security of C programs (tool paper). In: Reger, G., Havelund, K. (eds.) Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES). Kalpa, vol. 3, pp. 164–173. EasyChair (2017). https://doi.org/10.29007/fpdh

  32. Statman, R.: Logical relations and the typed \(\lambda \)-calculus. Inf. Control 65(2/3), 85–97 (1985). https://doi.org/10.1016/S0019-9958(85)80001-2

    Article  MathSciNet  MATH  Google Scholar 

  33. Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad-hoc. In: Symposium on Principles of Programming Languages (POPL), pp. 60–76. ACM Press (1989). https://doi.org/10.1145/75277.75283

  34. Zingg, S., Krstić, S., Raszyk, M., Schneider, J., Traytel, D.: Verified first-order monitoring with recursive rules. In: TACAS 2022. LNCS, vol. 13244, pp. 236–253. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99527-0_13

    Chapter  Google Scholar 

  35. Zumsteg, R.: Monitoring complex data types. Bachelor thesis, ETH Zürich (2022)

    Google Scholar 

Download references

Acknowledgments

Remo Zumsteg contributed to adding product types to CMFOTL via an encoding approach. François Hublet and Dmitriy Traytel contributed to CMFOTL’s type system and semantics. We thank the anonymous reviewers for helping us improve the presentation of this paper.

Author information

Authors and Affiliations

  1. Institute of Information Security, Department of Computer Science, ETH Zürich, Zürich, Switzerland

    Jeniffer Lima Graf, Srđan Krstić & Joshua Schneider

Authors
  1. Jeniffer Lima Graf
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Srđan Krstić
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Joshua Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Srđan Krstić or Joshua Schneider .

Editor information

Editors and Affiliations

  1. Dept. of Informatics, Aristotle Univ. of Thessaloniki, Thessaloniki, Greece

    Panagiotis Katsaros

  2. University of Trieste, Trieste, Italy

    Laura Nenzi

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lima Graf, J., Krstić, S., Schneider, J. (2023). Metric First-Order Temporal Logic with Complex Data Types. In: Katsaros, P., Nenzi, L. (eds) Runtime Verification. RV 2023. Lecture Notes in Computer Science, vol 14245. Springer, Cham. https://doi.org/10.1007/978-3-031-44267-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-44267-4_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-44266-7

  • Online ISBN: 978-3-031-44267-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation