Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Runtime Verification - 17 Years Later Kapitel lesen Erstes Kapitel lesen

2018 | OriginalPaper | Buchkapitel

Runtime Verification: From Propositional to First-Order Temporal Logic

verfasst von : Klaus Havelund, Doron Peled

Erschienen in: Runtime Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Can We Monitor All Multithreaded Programs?
Nächstes Kapitel Monitoring Smart Contracts: ContractLarva and Open Challenges Beyond
Fußnoten
1
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.
 
2
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.
 
3
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.
 
4
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 }\).).
 
5
Proving that liveness was PSPACE-hard was shown in [3].
 
6
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.
 
7
For dealing with finite domains see [12].
 
8
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 .
 
9
An additional 600+ lines of property independent boilerplate code is generated.
 
10
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.
 
Literatur
1.
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)CrossRef
2.
3.
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
4.
5.
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
6.
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
7.
Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)CrossRef
8.
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)
9.
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.
14.
15.
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.
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)
Metadaten
Titel
Runtime Verification: From Propositional to First-Order Temporal Logic
verfasst von
Klaus Havelund
Doron Peled
Copyright-Jahr
2018
Buch
Runtime Verification

Print ISBN: 978-3-030-03768-0

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

Copyright-Jahr: 2018

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

Premium Partner

    Bildnachweise