Top

Published in:

2018 | OriginalPaper | Chapter

Runtime Verification: From Propositional to First-Order Temporal Logic

Authors : Klaus Havelund, Doron Peled

Published in: Runtime Verification

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

Runtime Verification is a branch of formal methods concerned with analysis of execution traces for the purpose of determining the state or general quality of the executing system. The field covers numerous approaches, one of which is specification-based runtime verification, where execution traces are checked against formal specifications. The paper presents syntax, semantics, and monitoring algorithms for respectively propositional and first-order temporal logics. In propositional logics the observed events in the execution trace are represented using atomic propositions, while first-order logic allows universal and existential quantification over data occurring as arguments in events. Monitoring of the first-order case is drastically more challenging than the propositional case, and we present a solution for this problem based on BDDs. We furthermore discuss monitorability of temporal properties by dividing them into different classes representing different degrees of monitorability.

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 "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

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

previous chapter Can We Monitor All Multithreaded Programs?

next chapter Monitoring Smart Contracts: ContractLarva and Open Challenges Beyond

RV can be understood more broadly to mean: any processing of execution traces for the purpose of evaluating a system state or quality. Some approaches do not involve specifications but rather use pre-programmed algorithms as monitors.

This definition is equivalent to the traditional definition \(\xi , {i} \models ( \varphi \ \mathcal {S}\ \psi )\) iff for some \(0 < j \le i\), \(\xi , {j} \models \psi \), and for all \(j < k \le i\) it holds that \(\xi , {k} \models \varphi \), but is more intuitive for the forthcoming presentation of the RV algorithm.

There are examples of safety properties that are much more compact when expressed with the past temporal operators [21], and for symmetrical considerations also vice versa.

To show that a property is not monitorable, one needs to guess a state of \(\mathcal{B}_\varphi \times \mathcal{B}_{\lnot \varphi }\) and check that (1) it is reachable, and (2) one cannot reach from it an empty component, both for \(\mathcal{B}_\varphi \) and for \(\mathcal{B}_{\lnot \varphi }\). (There is no need to construct \(\mathcal{C}_\varphi \) or \(\mathcal{C}_{\lnot \varphi }\).).

Proving that liveness was PSPACE-hard was shown in [3].

All examples of safety properties henceforth will omit the implied

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-03769-7_7/476168_1_En_7_IEq200_HTML.gif

operator.

For dealing with finite domains see [12].

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-03769-7_7/476168_1_En_7_IEq292_HTML.gif

is the overriding of \(\gamma \) with the binding

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-03769-7_7/476168_1_En_7_IEq294_HTML.gif

An additional 600+ lines of property independent boilerplate code is generated.

Traces accepted by the tool are concretely in CSV format. For example the first event is a single line of the form: open,input,read.

Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)CrossRef

Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1–33. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_1CrossRef

Basin, D.A., Jiménez, C.C., Klaedtke, F., Zalinescu, E.: Deciding safety and liveness in TPTL. Inf. Process. Lett. 114(12), 680–688 (2014)MathSciNetCrossRef

Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126–138. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77395-5_11CrossRefMATH

Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Method. 20(4), 14:1–14:64 (2011)CrossRef

Bryant, R.E.: On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans. Comput. 40(2), 205–213 (1991)MathSciNetCrossRef

Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)CrossRef

Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. In: LICS 1990, pp. 428–439 (1990)

Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? STTT 14(3), 349–382 (2012)CrossRef

10.

Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL 1980, pp. 163–173. ACM (1980)

11.

Gerth, R., Peled, D.A., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995, pp. 3–18 (1995)CrossRef

12.

Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with BDDs. In: FMCAD 2017, pp. 116–123. IEEE (2017)

13.

Havelund, K., Reger, G., Thoma, D., Zălinescu, E.: Monitoring events that carry data. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 61–102. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_3CrossRef

14.

Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-46002-0_24CrossRefMATH

15.

JavaBDD. http://javabdd.sourceforge.net

16.

Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance tool for Java. In: RV 2001. Elsevier (2001). ENTCS 55(2), 218–235CrossRef

17.

Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291–314 (2001)CrossRef

18.

Kupferman, O., Vardi, G.: On relative and probabilistic finite counterability. Formal Methods Syst. Des. 52(2), 117–146 (2018)CrossRef

19.

Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125–143 (1977)MathSciNetCrossRef

20.

Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83, 91–130 (1991)CrossRef

21.

Markey, N.: Temporal logic with past is exponentially more succinct, concurrency column. Bull. EATCS 79, 122–128 (2003)MathSciNetMATH

22.

Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. STTT 14(3), 249–289 (2012). SpringerCrossRef

23.

Peled, D., Havelund, K.: Refining the safety-liveness classification of temporal properties according to monitorability. LNCS (2018, submitted )

24.

Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, Jayadev, Nipkow, Tobias, Sekerinski, Emil (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006). https://doi.org/10.1007/11813040_38CrossRef

25.

Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6(5), 495–512 (1994)CrossRef

26.

Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. In: STOC 1982, pp. 159–168 (1982). J. ACM (JACM), 32(3), 733–749, July 1985. JACM Homepage archiveMathSciNetCrossRef

27.

Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133–192 (1990)

Title: Runtime Verification: From Propositional to First-Order Temporal Logic
Authors: Klaus Havelund
Doron Peled
Publisher: Springer International Publishing
Book: Runtime Verification
Print ISBN: 978-3-030-03768-0

Electronic ISBN: 978-3-030-03769-7

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-030-03769-7_7

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 "Technik"

Springer Professional "Wirtschaft"

Premium Partner