Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
International Journal on Software Tools for Technology Transfer
Published in: International Journal on Software Tools for Technology Transfer 4/2021

12-07-2021 | General

An extension of first-order LTL with rules with application to runtime verification

Authors: Klaus Havelund, Doron Peled

Published in: International Journal on Software Tools for Technology Transfer | Issue 4/2021

Log in

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

search-config
loading …

Abstract

Linear temporal logic (LTL) is extensively used in formal methods, in particular in runtime verification (RV) and in model checking. Its propositional version was shown by Wolper (1983, Inform Control 56(1/2): 72–99) to be limited in expressiveness. Several extensions of propositional LTL, which promote the expressive power to that of Büchi automata, have therefore been proposed; however, none of those, by and large, have been adopted for formal methods. We present an extension of propositional LTL with rules, that is as expressive as these aforementioned extensions. We then show a similar deficiency in the expressiveness of first-order LTL and present an extension of it with rules, which parallels the propositional version. In our work on runtime verification, we focus on execution traces which consist of events that carry data, where a first-order version of LTL is needed, and in particular on past time versions of first-order LTL. In the previous work, we provided an algorithm for past time first-order LTL that uses BDDs to represent relations over data elements, and implemented it as a tool called DejaVu. In this paper, we propose a monitoring algorithm for the extension of past time first-order LTL with rules. This is implemented as an extension of DejaVu, and experimental results are provided.
previous article Introduction to the special issue of the 19th International Conference on Runtime Verification
next article Specifying and detecting temporal patterns with shape expressions

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
Footnotes
1
The logics are called monadic since they allow relations with one parameter that explicitly represents the time; hence, instead of occurrences of a proposition p in the temporal logic formulas, the monadic logics have a relation p where p(i) stands for p holds at time i. First-order monadic logic allows quantifying over the time variables, while second-order logic allows quantifying over the relations.
 
2
For a counter-free language, there is an integer n such that for all words x, y, z and integers \(m \ge n\) we have that \(xy^m z \in L\) if and only if \(xy^n z \in L\).
 
3
Finite domains are handled with some minor changes, see [24].
 
4
This theory is based on the compactness theory of first-order logic, see [17] Chap. 4.
 
5
Again, the definition can be extended to any number of variables.
 
6
Other enumeration generation schemes are possible. Our implementation allows a garbage collection mechanism that can reuse enumerations that are no longer needed.
 
7
With k bits, we can store \(2^k\) enumerations. It is possible to extend the number of bits used on the fly.
 
8
An additional 900+ lines of mostly property-independent boilerplate code is generated.
 
Literature
1.
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)CrossRef
2.
Attard, D.P., Cassar, I., Francalanza, A., Aceto, L., Ingólfsdóttir, A.: A runtime monitoring tool for actor-based systems. In: Gay, S., Ravara, A. (eds) Behavioural Types: from Theory to Tools, Chapter 3, pp. 49–76, River Publishers, Denmark (2017)
3.
Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification, Verification, Model Checking, and Abstract Interpretation (VMCAI’04), LNCS, vol. 44–57. Springer, Berlin (2004)
4.
Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Log. Comput. (JLC), Vol. 20, No. 3. Oxford University Press, Oxford, pp. 675–706 (2008)
5.
Bartocci, E., Falcone, Y., Francalanza, A., Leucker, M., Reger, G.: An introduction to runtime verification, lectures on runtime verification - introductory and advanced topics, LNCS, vol. 1–23. Springer, Berlin (2018)
6.
Basin, D.A., Klaedtke, F., Marinovic, S., Zalinescu, En: Monitoring of temporal first-order properties with aggregations. Form. Meth. Syst. Des. 46(3), 262–285 (2015)CrossRef
7.
Basin, D.A., Klaedtke, F., Müller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 1–45 (2015)MathSciNetCrossRef
8.
Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly?, Workshop on Runtime Verification (RV’07), LNCS, vol. 126–138. Springer, Berlin (2007)
9.
Bohn, J., Damm, W., Grumberg, O., Hungar, H., Laster, K.: First-order CTL model checking, International Conference on Foundations of Software Technology and Theoretical Computer Science, (FSTTCS’98), LNCS, vol. 283–294. Springer, Berlin (1998)
10.
Bryant, R.E.: Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)CrossRef
11.
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. Inform. Comput. 98(2), 142–170 (1992)MathSciNetCrossRef
12.
Chomicki, J.: Efficient checking of temporal integrity constraints using bounded history encoding. ACM Trans. Database Syst. 20(2), 149–186 (1995)CrossRef
13.
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Chambridge (2000)MATH
14.
D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z. LOLA: Runtime monitoring of synchronous systems, International Symposium on Temporal Representation and Reasoning (TIME’05), IEEE, 166-174. (2005)
15.
Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. J. Softw. Tools Technol. Transf. 18(2), 205–225 (2016)CrossRef
16.
17.
Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical Logic. Undergraduate texts in mathematics. Springer, Berlin (1984)MATH
18.
Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? STTT 14(3), 349–382 (2012)CrossRef
19.
Forgy, C.: Rete: A Fast algorithm for the many pattern/many object pattern match problem. Artif. Intell. 19, 17–37 (1982)CrossRef
20.
Frenkel, H., Grumberg, O., Sheinvald, S.: An automata-theoretic approach to modeling systems and specifications over infinite data, NASA Formal Methods (NFM 17), LNCS, vol. 1–18. Springer, Berlin (2017)
21.
Geist, J., Rozier, K.Y., Schumann, J.: Runtime observer pairs and Bayesian network reasoners on-board FPGAs: Flight-certifiable system health management for embedded systems, International Conference on Runtime Verification (RV’14), LNCS, vol. 215–230. Springer, Berlin (2014)
22.
Gerth, R., Peled, D.A., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. PSTV 3–18 (1995)
23.
Hallé, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Trans. Serv. Comput. 5(2), 192 (2012)CrossRef
24.
Havelund, K., Peled, D.A., Ulus, D.: First-order temporal logic monitoring with BDDs, Formal Methods in Computer Aided Design (FMCAD’17), IEEE, pp. 116–123 (2017)
25.
Havelund, K., Peled, D.: Efficient runtime verification of first-order temporal properties. International Symposium on Model Checking Software (SPIN’18), LNCS Volume 10869, Springer, Berlin, pp. 26–47 (2018)
26.
Havelund, K., Reger, G., Thoma, D., Zălinescu, E.: Monitoring events that carry data, Lectures on Runtime Verification—Introductory and Advanced Topics, LNCS, vol. 61–102. Springer, Berlin (2018)
27.
Havelund, K., Rosu, G.: Synthesizing monitors for safety properties, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 02), LNCS, vol. 342–356. Springer, Berlin (2002)
28.
Havelund, K.: Data automata in Scala, Theoretical Aspects of Software Engineering (TASE’14), IEEE Computer Society, pp. 1–9 (2014)
29.
Havelund, K.: Rule-based runtime verification revisited. Softw. Tools Technol. Transf. 17(2), 143–170 (2015)CrossRef
30.
Havelund, K., Peled, D.A., Ulus, D.: First-order temporal logic monitoring with BDDs. Form. Meth. Syst. Des. 56, 1–21 (2019)CrossRef
31.
32.
IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850TM-2010, (2010)
33.
34.
Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Form. Methods Syst. Des. 19(3), 291–314 (2001)CrossRef
35.
Maler, O., Nic̆ković, D.: Monitoring properties of analog and mixed-signal circuits. Int. J. Softw. Tools Technol. Transf., Springer, Berlin, vol. 15, pp. 247–268, (2013)
36.
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems—Specification. Springer, Berlin (1992)CrossRef
37.
38.
Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. vol. 14, pp. 249–289. Springer, Berlin (2012)
39.
Pike, L., Wegmann, N., Niller, S., Goodloe, A.: Copilot: Monitoring embedded systems. Innov. Syst. Softw. Eng. 9(4), 235–255 (2013)CrossRef
40.
Reger, G., Cruz, H., Rydeheard, D.: MarQ: Monitoring at runtime with QEA, Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15), LNCS, vol. 596–610. Springer, Berlin (2015)
41.
Schneider, J., Basin, D., Krstić, S., Traytel, D.: A formally verified monitor for metric first-order temporal logic, International Conference on Runtime Verification (RV’19), LNCS, vol. 310–328. Springer, Berlin (2019)
42.
Shafiei, N., Havelund, K., Mehlitz, P.C.: Actor-based runtime verification with MESA, International Conference on Runtime Verification (RV’20), LNCS, vol. 221–240. Springer, Berlin (2020)
43.
Sistla, A.P.: Theoretical Issues in the Design and Analysis of Distributed Systems, Ph.D Thesis, Harvard University, (1983)
44.
Thomas, W.: Automata on infinite objects, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 133–192 (1990)
45.
Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths, Annual Symposium on Foundations of Computer Science (SFCS’83), ACM, pp. 185–194
46.
Metadata
Title
An extension of first-order LTL with rules with application to runtime verification
Authors
Klaus Havelund
Doron Peled
Publication date
12-07-2021
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 4/2021
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-021-00626-y

Other articles of this Issue 4/2021

International Journal on Software Tools for Technology Transfer 4/2021 Go to the issue

General

What can we monitor over unreliable channels?

General

Specifying and detecting temporal patterns with shape expressions

General

Quantitative estimation of side-channel leaks with neural networks

General

Neural predictive monitoring and a comparison of frequentist and Bayesian approaches

General

Compositional learning of mutually recursive procedural systems

General

Introduction to the special issue of the 19th International Conference on Runtime Verification

Premium Partner

    Image Credits