Top

Formal Methods in System Design

Published in:

25-03-2023

Assumption-based Runtime Verification

Authors: Alessandro Cimatti, Chun Tian, Stefano Tonetta

Published in: Formal Methods in System Design | Issue 2/2022

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Runtime Verification is a lightweight automatic verification technique. We introduce Assumption-Based Runtime Verification framework, which is capable for monitoring partially observable systems. The framework leverages assumptions on the behaviors of the systems under scrutiny for reasoning on their the non-observable or future behaviors. The specification is expressed in Propositional Linear Temporal Logic (LTL) with both future and past temporal operators, while assumptions are described in Fair Kripke Structures. Static or dynamic sets of observables are supported. The monitors are also resettable, i.e. being able to evaluate the specification at arbitrary positions of the input trace. We present the formalism of the framework and a series of monitoring algorithms which can be efficiently implemented by Binary Decision Diagrams. As a by-product, we also present a new automata-based monitor construction for Past-time LTL, an LTL variant with only past temporal operators. We give proofs for the correctness of all involved algorithms. The framework is implemented in NuRV, an extension of the nuXmv model checker. It synthesizes implicit or explicit monitors which can be deployed in online or offline modes. The explicit monitors are embeddable code in programming languages including C, C++, Java and Common Lisp. In particular, monitors can be generated as SMV models, whose correctness and other properties can be verified in nuXmv . Using a benchmark from Dwyer’s LTL patterns, we show the efficiency of the symbolic approach and the generated monitors, and the feasibility and effectiveness of the approach. Some monitors are shown to be predictive under certain assumptions.

previous article Specifiable robustness in reactive synthesis

next article Correction: Parameterized verification of leader/follower systems via first-order temporal logic

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Available only for authorised users

Bauer et al. report that 44% of the formulas they consider in their experiments are not monitorable [57].

We omit compassion requirements as they are not used in our approach.

The ptLTL plugin of RV-Monitor comes from JavaMOP.

Actually in this case the monitor outputs \(\bot ^\textrm{a}\) one step after the fault happens. It did not immediately outputs \(\bot ^\textrm{a}\) at the moment when the fault happens because, according to the model, the bottle may get filled again before the belt moves.

See factory_example/trace3.xml in the artifact for the contents of this trace.

The latest version (55 in total) is available at https://matthewbdwyer.github.io/psp/patterns/ltl.html. We call them Pattern \(0,1, \ldots , 54\) in the same order.

The error message is “violation is not a supported state in this logic, ltl”.

Aceto L, Achilleos A, Francalanza A, Ingólfsdóttir A, Lehtinen K (2019) An operational guide to monitorability. In: Ölveczky PC, Salaün G (eds) LNCS 11724—software engineering and formal methods (SEFM 2019). Springer, Cham, pp 433–453. https://doi.org/10.1007/978-3-030-30446-1_23

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

Azzopardi S, Colombo C, Pace GJ (2016) A model-based approach to combining static and dynamic verification techniques. In: Margaria T, BernhardS (ed) LNCS 9952—leveraging applications of formal methods, verification and validation (ISoLA 2016, Part I). Springer, pp 416–430. https://doi.org/10.1007/978-3-319-47166-2_29

Barringer H, Havelund K (2011) TraceContract—a Scala DSL for trace analysis. In: LNCS 6664—FM 2011: formal methods. Springer, Berlin, pp 57–72. https://doi.org/10.1007/978-3-642-21437-0_7

Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based Runtime Verification. In: Steffen B, Levi G (eds) LNCS 2937—Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, Berlin, pp 44–57. https://doi.org/10.1007/978-3-540-24622-0_5

Barringer H, Rydeheard DE, Havelund K (2007) Rule systems for run-time monitoring: from eagle to RuleR. In: LNCS 4389—Runtime Verification (RV 2007). Springer, Berlin, pp 111–125 . https://doi.org/10.1007/978-3-540-77395-5_10

Bauer A, Falcone Y (2016) Decentralised LTL monitoring. Formal methods in system design 48(1–2):46–93. https://doi.org/10.1007/s10703-016-0253-8CrossRefMATH

Bauer A, Leucker M, Schallhart C (2010) Comparing LTL semantics for Runtime Verification. J Logic Comput 20(3):651–674. https://doi.org/10.1093/logcom/exn075MathSciNetCrossRefMATH

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

10.

Bernasconi A, Menghi C, Spoletini P, Zuck LD, Ghezzi C (2018) From model checking to a temporal proof for partial models. In: Cerone A, Roveri M (eds) LNCS 10469—Software Engineering and Formal Methods (SEFM 2017). Springer, Cham, pp 54–69. https://doi.org/10.1007/978-3-319-66197-1_4

11.

Bertot Y, Castéran P (2013) Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Springer, Berlin. https://doi.org/10.1007/978-3-662-07964-5

12.

Bittner B, Bozzano M, Cimatti A, Olive X (2012) Symbolic synthesis of observability requirements for diagnosability. In: Proceedings of the twenty-sixth AAAI conference on artificial intelligence, July 22–26, 2012, Toronto, Ontario, Canada. http://www.aaai.org/ocs/index.php/AAAI/AAAI12/paper/view/5056

13.

Bozzano M, Cimatti A, Gario M, Tonetta S (2014) Formal design of fault detection and identification components using temporal epistemic logic. In: LNCS 8413—tools and algorithms for the construction and analysis of systems (TACAS 2014). Springer, Berlin, pp 326–340. https://doi.org/10.1007/978-3-642-54862-8_22

14.

Bozzano M, Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2019) nuXmv 2.0.0 user manual. https://es.fbk.eu/tools/nuxmv/downloads/nuxmv-user-manual.pdf

15.

Broy M, Jonsson B, Katoen J-P, Leucker M, Pretschner A (2005). LNCS 3472–model-based testing of reactive systems. https://doi.org/10.1007/b137241

16.

Bruns G, Godefroid P (1999) Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs N, Peled DA (eds) LNCS 1633-Computer Aided Verification (CAV 1999). Springer, Berlin, pp 274–287. https://doi.org/10.1007/3-540-48683-6_25

17.

Bryant RE (2018) Binary Decision Diagrams. In: Clarke EM Jr, Henzinger TA, Veith H, Bloem R (eds) Handbook of model checking. Springer, Cham, pp 191–217. https://doi.org/10.1007/978-3-319-10575-8_7

18.

Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang L-J (1992) Symbolic model checking: \(10^{20}\) states and beyond. Inf Comput 98(2):142–170. https://doi.org/10.1016/0890-5401(92)90017-ACrossRefMATH

19.

Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuXmv symbolic model checker. In: Biere A, Bloem R (eds) LNCS 8559—Computer Aided Verification (CAV 2014). Springer, Cham, pp 334–342. https://doi.org/10.1007/978-3-319-08867-9_22

20.

Chen F, Roşu G (2007) MOP: an efficient and generic runtime verification framework. In: 22nd Annual ACM SIGPLAN conference. ACM Press, New York, USA, pp 569–588. https://doi.org/10.1145/1297027.1297069

21.

Chen F, Roşu G (2009) Parametric trace slicing and monitoring. In: LNCS 5505—tools and algorithms for the construction and analysis of systems (TACAS 2009). Springer, Berlin, pp 246–261. https://doi.org/10.1007/978-3-642-00768-2_23

22.

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

23.

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

24.

Clarke EM, Grumberg O, Hamaguchi K (1997) Another look at LTL model checking. Formal Methods Syst Des 10(1):47–71. https://doi.org/10.1023/A:1008615614281CrossRef

25.

Clarke EM, Henzinger TA, Veith H, Bloem R (2018). Handbook of model checking. https://doi.org/10.1007/978-3-319-10575-8

26.

Coble AR (2010) Anonymity, information, and machine-assisted proof. Technical Report UCAM-CL-TR-785, University of Cambridge, Computer Laboratory. https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-785.pdf

27.

Colombo C, Falcone Y (2016) Organising LTL monitors over distributed systems with a global clock. Formal Methods Syst Des 49(1):109–158. https://doi.org/10.1007/s10703-016-0251-xCrossRefMATH

28.

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

29.

Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: Proceedings of the 21st international conference on software engineering. ACM Press, New York, pp 411–420. https://doi.org/10.1145/302405.302672

30.

Emerson El, Lei C-L (1986) Temporal reasoning under generalized fairness constraints. In: Monien B, Vidal-Naquet G (eds) LNCS 210—theoretical aspects of computer science (STACS 1986). Springer, Berlin, pp 21–36. https://doi.org/10.1007/3-540-16078-7_62

31.

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

32.

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

33.

Fauri D, dos Santos DR, Costante E, den Hartog J, Etalle S, Tonetta S (2017) From system specification to anomaly detection (and back). In: Proceedings of the 2017 workshop on cyber-physical systems security and PrivaCy. ACM Press, New York, pp 13–24. https://doi.org/10.1145/3140241.3140250

34.

Fuxman AD (2001) Formal analysis of early requirements specifications. PhD thesis, University of Toronto. https://tspace.library.utoronto.ca/handle/1807/15905

35.

Genc S, Lafortune S (2009) Predictability of event occurrences in partially-observed discrete-event systems. Automatica 45(2):301–311. https://doi.org/10.1016/j.automatica.2008.06.022MathSciNetCrossRefMATH

36.

Genc S, Lafortune S (2006) Predictability in discrete-event systems under partial observation. IFAC Proc 39(13):1461–1466. https://doi.org/10.3182/20060829-4-CN-2909.00243CrossRef

37.

Gordon MJC, Melham TF (1993) Introduction to HOL. Cambridge University Press, New York, A theorem proving environment for higher order logicMATH

38.

Graf S, Peled DA, Quinton S (2011) Monitoring distributed systems using knowledge. In: Bruni R, Dingel J (eds) LNCS 6722—formal techniques for distributed systems (FMOODS/FORTE 2011). Springer, Berlin, pp 183–197. https://doi.org/10.1007/978-3-642-21461-5_12

39.

Halpern Joseph Y, Vardi Moshe Y (1989) The complexity of reasoning about knowledge and time. I. Lower bounds. J Comput Syst Sci 38(1):195–237. https://doi.org/10.1016/0022-0000(89)90039-1

40.

Havelund K, Peled DA (2018) Runtime Verification—from propositional to first-order temporal logic. In: LNCS 11237—Runtime Verification (RV 2018). Springer, Cham, pp 90–112. https://doi.org/10.1007/978-3-030-03769-7_7

41.

Havelund K, Roşu G (2002) Synthesizing monitors for safety properties. In: Katoen J-P, Stevens P (eds) LNCS 2280—tools and algorithms for the construction and analysis of systems (TACAS 2002). Springer, Berlin, pp 342–356. https://doi.org/10.1007/3-540-46002-0_24

42.

Havelund K, Roşu G (2004) An overview of the runtime verification tool Java PathExplorer. Formal Methods Syst Des 24(2):189–215. https://doi.org/10.1023/B:FORM.0000017721.39909.4bCrossRefMATH

43.

Havelund K, Peled DA, Ulus D (2017) First order temporal logic monitoring with BDDs. In: Formal methods in computer-aided design (FMCAD 2017). IEEE, pp 116–123. https://doi.org/10.23919/FMCAD.2017.8102249

44.

Havelund K, Peled DA, Ulus D (2019) First-order temporal logic monitoring with BDDs. Formal Methods Syst Des 2(3):117–23. https://doi.org/10.1007/s10703-018-00327-4CrossRefMATH

45.

Henzinger TA, Ege SN (2020) Monitorability under assumptions. In: Deshmukh J, Nickovic D (eds) LNCS 12399—Runtime Verification (RV 2020). Springer, Cham, pp 3–18. https://doi.org/10.1007/978-3-030-60508-7_1

46.

Hurd J (2003) Formal verification of probabilistic algorithms. Technical Report UCAM-CL-TR-566, University of Cambridge, Computer Laboratory. https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-566.pdf

47.

Jhala R, Majumdar R (2009) Software model checking. ACM Comput Surv CSUR 41(4):1–54CrossRefMATH

48.

Kaufmann M, Manolios P, Strother MJ (2000) Computer-aided reasoning: an approach, volume 3 of advances in formal methods. Springer, Boston

49.

Kesten Y, Pnueli A, Raviv L (1998) Algorithmic verification of linear temporal logic specifications. In: Larsen KG, Skyum S, Winskel G (eds) LNCS 1443—automata, languages and programming (ICALP 1998). Springer, Berlin, pp 1–16. https://doi.org/10.1007/BFb0055036

50.

Kleene SC (1971) Introduction to metamathematics. Wolthers-Noordhoff, New YorkMATH

51.

Laroussinie F, Markey N, Schnoebelen P (2002) Temporal logic with forgettable past. In: Proceedings of the 17th annual IEEE symposium on logic in computer science (LICS 2002). IEEE Computer Society, pp 383–392. https://doi.org/10.1109/LICS.2002.1029846

52.

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

53.

Leucker M, Schallhart C (2009) A brief account of Runtime Verification. J Logic Algebr Program 78(5):293–303. https://doi.org/10.1016/j.jlap.2008.08.004CrossRefMATH

54.

Luo Q, Zhang Y, Lee C, Jin D, O’Neil MP, Serbanuta T-F, Roşu G (2014) RV-Monitor: efficient parametric Runtime Verification with simultaneous properties. In: Bonakdarpour B, Smolka SA (eds) LNCS 8734—Runtime Verification (RV 2014). Springer, Cham, pp 285–300. https://doi.org/10.1007/978-3-319-11164-3_24

55.

Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems: specification. Springer, New York. https://doi.org/10.1007/978-1-4612-0931-7CrossRefMATH

56.

Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, New York. https://doi.org/10.1007/978-1-4612-4222-2CrossRefMATH

57.

Mascle C, Neider D, Schwenger M, Tabuada P (2020) From LTL to rLTL monitoring: improved monitorability through robust semantics. In: 23rd International conference on hybrid systems computation and control. ACM, New York, pp 1–12. https://doi.org/10.1145/3365365.3382197

58.

Menghi C, Spoletini P, Ghezzi C (2016) Dealing with incompleteness in automata-based model checking. In: LNCS 9995—FM 2016: formal methods. Springer. https://doi.org/10.1007/978-3-319-48989-6

59.

Peled DA, Havelund K (2019) Refining the safety-liveness classification of temporal properties according to monitorability. In: Models, mindsets, meta: the what, the how, and the why not? Springer, pp 218–234. https://doi.org/10.1007/978-3-030-22348-9_14

60.

Pinisetty S, Jéron T, Tripakis S, Falcone Y, Marchand H, Preoteasa V (2017) Predictive runtime verification of timed properties. J Syst Softw 132:353–365. https://doi.org/10.1016/j.jss.2017.06.060CrossRefMATH

61.

Roşu G, Havelund K (2005) Rewriting-based techniques for Runtime Verification. Autom Softw Eng 12(2):151–197. https://doi.org/10.1007/s10515-005-6205-yCrossRef

62.

Rozier KY, Schumann J (2017) R2U2: tool overview. Kalpa Publ Comput 3:138–156. https://doi.org/10.29007/5pch

63.

Sampath M, Sengupta R, Lafortune S, Sinnamohideen K, Teneketzis D (1995) Diagnosability of discrete-event systems. IEEE Trans Autom Control 40(9):1555–1575. https://doi.org/10.1109/9.412626MathSciNetCrossRefMATH

64.

Schneider K (2001) Improving automata generation for Linear Temporal Logic by considering the automaton hierarchy. In: Nieuwenhuis R, Voronkov A (eds) LNAI 2250—logic for programming, artificial intelligence, and reasoning (LPAR 2001). Springer, Berlin, pp 39–54. https://doi.org/10.1007/3-540-45653-8_3

65.

Schneider K (2004) Temporal logics. In: Verification of reactive systems—formal methods and algorithms. Springer, Berlin, pp 279–404. https://doi.org/10.1007/978-3-662-10778-2_5

66.

Selyunin K, Jaksic S, Nguyen T, Reidl C, Hafner U, Bartocci E, Nickovic D, Grosu R (2017) Runtime monitoring with recovery of the SENT communication protocol. In: Majumdar R, Kunčak V (eds) LNCS 10426—computer aided verification (CAV 2017, Part I). Springer. https://doi.org/10.1007/978-3-319-63387-9_17

67.

Sistla AP, Zhou M, Zuck LD (2006) Monitoring off-the-shelf components. In: Emerson EA, Namjoshi KS (eds) LNCS 3855—verification, model checking, and abstract interpretation (VMCAI 2006). Springer, Berlin, pp 222–236. https://doi.org/10.1007/11609773_15

68.

Sistla AP, Zefran M, Feng Y (2011) Monitorability of stochastic dynamical systems. In: CAV, pp 720–736

69.

Tan L, Kim J, Sokolsky O, Lee I (2004) Model-based testing and monitoring for hybrid embedded systems. In: IEEE international conference on information reuse and integration. IEEE, pp 487–492. https://doi.org/10.1109/IRI.2004.1431508

70.

Tuerk T, Schneider K, Gordon M (2007) Model checking PSL using HOL and SMV. In: Bin E, Ziv A, Ur S (eds) LNCS 4383—hardware and software: verification and testing (HVC 2006). Springer, Berlin, pp 1–15. https://doi.org/10.1007/978-3-540-70889-6_1

71.

Zhang X, Leucker M, Dong W (2012) Runtime Verification with predictive semantics. In: Goodloe AE, Person S (eds) LNCS 7226—NASA formal methods (NFM 2012). Springer, Berlin, pp 418–432. https://doi.org/10.1007/978-3-642-28891-3_37

72.

Zhao Y, Oberthür S, Kardos M, Rammig FJ (2006) Model-based Runtime Verification framework for self-optimizing systems. Electron Notes Theor Comput Sci 144(4):125–145. https://doi.org/10.1016/j.entcs.2006.02.008CrossRefMATH

73.

Zhao Y, Rammig F (2009) Model-based Runtime Verification framework. Electron Notes Theor Comput Sci 253(1):179–193. https://doi.org/10.1016/j.entcs.2009.09.035CrossRef

Title: Assumption-based Runtime Verification
Authors: Alessandro Cimatti
Chun Tian
Stefano Tonetta
Publication date: 25-03-2023
Publisher: Springer US
Published in: Formal Methods in System Design / Issue 2/2022
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-023-00416-z

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 2/2022

LTL model checking of self modifying code

Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking

Specifiable robustness in reactive synthesis

Correction: Parameterized verification of leader/follower systems via first-order temporal logic

Control strategies for off-line testing of timed systems

Functional synthesis via input–output separation

Premium Partner