Skip to main content
SpringerLink
Log in

Assumption-Based Runtime Verification of Infinite-State Systems

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

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12974))

Included in the following conference series:

Abstract

Runtime Verification (RV) basically means monitoring an execution trace of a system under scrutiny and checking if the trace satisfies or violates a specification. In Assumption-Based Runtime Verification (ABRV), runtime monitors may be synthesized from not only the specification but also a system model (either full or partial), which represents the assumptions on which the input traces are expected to follow. With assumptions the monitor can additionally check if the input traces actually follow the assumptions. Some previous research has shown that monitors under assumptions can be more precise or even predictive, while non-monitorable specifications may become monitorable under assumptions.

The question of synthesizing runtime monitors for finite-state systems and propositional or first-order temporal logics, with or without assumptions, has mostly been answered by prior work. For monitoring infinite-state systems, however, most existing approaches focus on supporting parametric or first-order specifications while they cannot be easily extended to support assumptions.

This paper presents a general solution for ABRV of infinite-state systems by a reduction of RV problems to LTL Model Checking (MC), which is further based on Satisfiability Modulo Theories and other techniques. When First-Order Quantifier Elimination (QE) is also available, the corresponding algorithm can be greatly optimized. This solution is general because in theory any LTL MC (and QE) algorithms can be used, and the supported types of infinite-state variables also depend on these underlying algorithms. In particular, the relatively expensive model checking can be minimized by a modified version of Bounded Model Checking algorithm which performs model checking incrementally on each input of the monitor.

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 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 84.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

Similar content being viewed by others

Notes

  1. 1.

    According to [21], a specification is a concrete description of a property (a partition of traces) using a well-defined formalism (like LTL). However, this difference is not very important here, and thus we use the words “property” and “specification” interchangeably for the rest of this paper.

  2. 2.

    In the ideal case (when BMC stopped by having found a counterexample, and the overall monitoring verdicts is conclusive), the monitor only needs to call SMT solver once to decide the next monitoring output.

  3. 3.

    The official site of NuRV is now at https://es-static.fbk.eu/tools/nurv/.

  4. 4.

    See also https://matthewbdwyer.github.io/psp/patterns/ltl.html.

References

  1. Arafat, O., Bauer, A., Leucker, M., Schallhart, C.: Runtime verification revisited. Technical report TUM-I0518, Technische Universität München, München (2005)

    Google Scholar 

  2. Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825–885. IOS Press, January 2009. https://doi.org/10.3233/978-1-58603-929-5-825

  3. Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651–674 (2010). https://doi.org/10.1093/logcom/exn075

    Article  MathSciNet  MATH  Google Scholar 

  4. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14–64 (2011). https://doi.org/10.1145/2000799.2000800

    Article  Google Scholar 

  5. Biere, A., Cimatti, A., Clarke Jr, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Advances in Computers: Highly Dependable Software, pp. 117–148. Academic Press (2003)

    Google Scholar 

  6. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (2008). https://doi.org/10.1007/3-540-49059-0_14

    Chapter  Google Scholar 

  7. Bryant, R.E.: Binary decision diagrams. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 191–217. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_7

    Chapter  Google Scholar 

  8. Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_22

    Chapter  Google Scholar 

  9. Cimatti, A., Griggio, A., Magnago, E., Roveri, M., Tonetta, S.: SMT-based satisfiability of first-order LTL with event freezing functions and metric operators. Inf. Comput. 272, 104502 (2020). https://doi.org/10.1016/j.ic.2019.104502

    Article  MathSciNet  MATH  Google Scholar 

  10. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 46–61. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_4

    Chapter  MATH  Google Scholar 

  11. Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_7

    Chapter  MATH  Google Scholar 

  12. Cimatti, A., Pistore, M., Roveri, M., Sebastiani, R.: Improving the encoding of LTL model checking into SAT. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 196–207. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-47813-2_14

    Chapter  MATH  Google Scholar 

  13. Cimatti, A., Tian, C., Tonetta, S.: Assumption-based runtime verification with partial observability and resets. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 165–184. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32079-9_10

    Chapter  Google Scholar 

  14. Cimatti, A., Tian, C., Tonetta, S.: NuRV: a nuXmv extension for runtime verification. In: Finkbeiner, B., Mariani, L. (eds.) RV 2019. LNCS, vol. 11757, pp. 382–392. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32079-9_23

    Chapter  Google Scholar 

  15. Colin, S., Mariani, L.: 18 run-time verification. In: Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.) Model-Based Testing of Reactive Systems. LNCS, vol. 3472, pp. 525–555. Springer, Heidelberg (2005). https://doi.org/10.1007/11498490_24

    Chapter  Google Scholar 

  16. Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. Int. J. Softw. Tools Technol. Transf. 18(2), 205–225 (2015). https://doi.org/10.1007/s10009-015-0380-3

    Article  Google Scholar 

  17. Du, X., Liu, Y., Tiu, A.: Trace-length independent runtime monitoring of quantitative policies in LTL. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 231–247. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_15

    Chapter  Google Scholar 

  18. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, pp. 411–420. ACM Press, New York (1999). https://doi.org/10.1145/302405.302672

  19. Allen Emerson, E., Lei, C.-L.: Temporal reasoning under generalized fairness constraints. In: Monien, B., Vidal-Naquet, G. (eds.) STACS 1986. LNCS, vol. 210, pp. 21–36. Springer, Heidelberg (1986). https://doi.org/10.1007/3-540-16078-7_62

    Chapter  Google Scholar 

  20. Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. Eng. Dependable Softw. Syst. 34, 141–175 (2013). https://doi.org/10.3233/978-1-61499-207-3-141

    Article  Google Scholar 

  21. Falcone, Y., Krstić, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 241–262. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03769-7_14

    Chapter  Google Scholar 

  22. Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput. 4(1), 69–76 (1975). https://doi.org/10.1137/0204006

    Article  MathSciNet  MATH  Google Scholar 

  23. Havelund, K., Peled, D.: Runtime verification: from propositional to first-order temporal logic. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 90–112. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03769-7_7

    Chapter  Google Scholar 

  24. Henzinger, T.A., Saraç, N.E.: Monitorability under assumptions. In: Deshmukh, J., Ničković, D. (eds.) RV 2020. LNCS, vol. 12399, pp. 3–18. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-60508-7_1

    Chapter  Google Scholar 

  25. Hoffmann, J., Brafman, R.I.: Contingent planning via heuristic forward search with implicit belief states. In: Biundo, S., Myers, K.L., Rajan, K. (eds.) Proceedings of the Fifteenth International Conference on Automated Planning and Scheduling (ICAPS 2005), 5–10 June 2005, Monterey, California, USA, pp. 71–80. AAAI (2005). http://www.aaai.org/Library/ICAPS/2005/icaps05-008.php

  26. Kejstová, K., Ročkai, P., Barnat, J.: From model checking to runtime verification and back. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 225–240. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_14

    Chapter  Google Scholar 

  27. Khachiyan, L.: Fourier-Motzkin elimination method. In: Floudas, C., Pardalos, P. (eds.) Encyclopedia of Optimization, pp. 1074–1077. Springer, Boston (2009). https://doi.org/10.1007/978-0-387-74759-0_187

    Chapter  Google Scholar 

  28. Leucker, M.: Sliding between model checking and runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 82–87. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_10

    Chapter  Google Scholar 

  29. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Program. 78(5), 293–303 (2009). https://doi.org/10.1016/j.jlap.2008.08.004

    Article  MATH  Google Scholar 

  30. Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450–462 (1993). https://dblp.org/rec/journals/cj/LoosW93

  31. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992). https://doi.org/10.1007/978-1-4612-0931-7

    Book  MATH  Google Scholar 

  32. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995). https://doi.org/10.1007/978-1-4612-4222-2

    Book  MATH  Google Scholar 

  33. Marcja, A., Toffalori, C.: Quantifier elimination. In: Marcja, A., Toffalori, C. (eds.) A Guide to Classical and Modern Model Theory, pp. 43–83. Springer, Dordrecht (2003). https://doi.org/10.1007/978-94-007-0812-9_2

    Chapter  MATH  Google Scholar 

  34. Reger, G., Rydeheard, D.: From first-order temporal logic to parametric trace slicing. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 216–232. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_14

    Chapter  Google Scholar 

  35. Tekken Valapil, V., Yingchareonthawornchai, S., Kulkarni, S., Torng, E., Demirbas, M.: Monitoring partially synchronous distributed systems using SMT solvers. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 277–293. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_17

    Chapter  Google Scholar 

  36. Zhang, X., Leucker, M., Dong, W.: Runtime verification with predictive semantics. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 418–432. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28891-3_37

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fondazione Bruno Kessler, Trento, Italy

    Alessandro Cimatti, Chun Tian & Stefano Tonetta

Authors
  1. Alessandro Cimatti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Chun Tian
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Stefano Tonetta
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Chun Tian .

Editor information

Editors and Affiliations

  1. University of Virginia, Charlottesville, VA, USA

    Lu Feng

  2. Ben-Gurion University of the Negev, Be'er Sheva, Israel

    Dana Fisman

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Cimatti, A., Tian, C., Tonetta, S. (2021). Assumption-Based Runtime Verification of Infinite-State Systems. In: Feng, L., Fisman, D. (eds) Runtime Verification. RV 2021. Lecture Notes in Computer Science(), vol 12974. Springer, Cham. https://doi.org/10.1007/978-3-030-88494-9_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-88494-9_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-88493-2

  • Online ISBN: 978-3-030-88494-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation