More Web Proxy on the site http://driver.im/

research-article

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

Authors:

Klaus Havelund,

Doron PeledAuthors Info & Claims

International Journal on Software Tools for Technology Transfer, Volume 23, Issue 4

Pages 547 - 563

https://doi.org/10.1007/s10009-021-00626-y

Published: 01 August 2021 Publication History

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.

References

[1]

Alpern B and Schneider FB Recognizing safety and liveness Distrib. Comput. 1987 2 3 117-126

[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 DA, Klaedtke F, Marinovic S, and Zalinescu En Monitoring of temporal first-order properties with aggregations Form. Meth. Syst. Des. 2015 46 3 262-285

[7]

Basin DA, Klaedtke F, Müller S, and Zalinescu E Monitoring metric first-order temporal properties J. ACM 2015 62 2 1-45

[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 RE Symbolic Boolean manipulation with ordered binary-decision diagrams ACM Comput. Surv. 1992 24 3 293-318

[11]

Burch JR, Clarke EM, McMillan KL, Dill DL, and Hwang LJ Symbolic model checking:

10^{20}

states and beyond Inform. Comput. 1992 98 2 142-170

[12]

Chomicki J Efficient checking of temporal integrity constraints using bounded history encoding ACM Trans. Database Syst. 1995 20 2 149-186

[13]

Clarke EM, Grumberg O, and Peled D Model checking 2000 Chambridge MIT Press

[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, and Thoma D Monitoring modulo theories J. Softw. Tools Technol. Transf. 2016 18 2 205-225

[16]

DejaVu, https://github.com/havelund/dejavu

[17]

Ebbinghaus H-D, Flum J, and Thomas W Mathematical Logic. Undergraduate texts in mathematics 1984 Berlin Springer

[18]

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

[19]

Forgy C Rete: A Fast algorithm for the many pattern/many object pattern match problem Artif. Intell. 1982 19 17-37

[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 and Villemaire R Runtime enforcement of web service message contracts with data IEEE Trans. Serv. Comput. 2012 5 2 192

[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. 2015 17 2 143-170

[30]

Havelund K, Peled DA, and Ulus D First-order temporal logic monitoring with BDDs Form. Meth. Syst. Des. 2019 56 1-21

[31]

Hella L, Libkin L, Nurmonen J, and Wong L Logics with aggregate operators J. ACM 2001 48 4 880-907

[32]

IEEE Standard for Property Specification Language (PSL), Annex B. IEEE Std 1850TM-2010, (2010)

[33]

JavaBDD, http://javabdd.sourceforge.net

[34]

Kupferman O and Vardi MY Model checking of safety properties Form. Methods Syst. Des. 2001 19 3 291-314

[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 and Pnueli A The Temporal Logic of Reactive and Concurrent Systems—Specification 1992 Berlin Springer

[37]

Mars Science Laboratory (MSL) mission website. http://mars.jpl.nasa.gov/msl

[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, and Goodloe A Copilot: Monitoring embedded systems Innov. Syst. Softw. Eng. 2013 9 4 235-255

[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]

Wolper P Temporal logic can be more expressive Inform. Contl. 1983 56 1/2 72-99

Cited By

Havelund KOmer MPeled DAncona DAudrito G(2024)Operational and Declarative Runtime Verification (Keynote)Proceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution10.1145/3679008.3685541(3-12)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3679008.3685541
Havelund KKatsaros POmer MPeled DTemperekidis A(2024)TP-DejaVu: Combining Operational and Declarative Runtime VerificationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_12(249-263)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_12
Kallwies HLeucker MSánchez C(2022)Symbolic Runtime Verification for Monitoring Under Uncertainties and AssumptionsAutomated Technology for Verification and Analysis10.1007/978-3-031-19992-9_8(117-134)Online publication date: 25-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19992-9_8

Index Terms

An extension of first-order LTL with rules with application to runtime verification
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Index terms have been assigned to the content through auto-classification.

Recommendations

LTL satisfiability checking

We report here on an experimental investigation of LTL satisfiability checking via a reduction to model checking. By using large LTL formulas, we offer challenging model-checking benchmarks to both explicit and symbolic model checkers. For symbolic ...
Anchored LTL separation
CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Gabbay's separation theorem is a fundamental result for linear temporal logic (LTL). We show that separating a restricted class of LTL formulas, called anchored LTL, is elementary if and only if the translation from LTL to the linear temporal logic with ...
An Extension of LTL with Rules and Its Application to Runtime Verification
Runtime Verification
Abstract
Runtime Verification (RV) consists of analyzing execution traces using formal techniques, e.g., monitoring executions against Linear Temporal Logic (LTL) properties. Propositional LTL is, however, limited in expressiveness, as first shown by ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image International Journal on Software Tools for Technology Transfer (STTT)

International Journal on Software Tools for Technology Transfer (STTT) Volume 23, Issue 4

Aug 2021

131 pages

ISSN:1433-2779

EISSN:1433-2787

Issue’s Table of Contents

© The Author(s), under exclusive licence to Springer-Verlag GmbH Germany, part of Springer Nature 2021.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 August 2021

Accepted: 06 May 2021

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Havelund KOmer MPeled DAncona DAudrito G(2024)Operational and Declarative Runtime Verification (Keynote)Proceedings of the 7th ACM International Workshop on Verification and Monitoring at Runtime Execution10.1145/3679008.3685541(3-12)Online publication date: 13-Sep-2024
https://dl.acm.org/doi/10.1145/3679008.3685541
Havelund KKatsaros POmer MPeled DTemperekidis A(2024)TP-DejaVu: Combining Operational and Declarative Runtime VerificationVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_12(249-263)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_12
Kallwies HLeucker MSánchez C(2022)Symbolic Runtime Verification for Monitoring Under Uncertainties and AssumptionsAutomated Technology for Verification and Analysis10.1007/978-3-031-19992-9_8(117-134)Online publication date: 25-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19992-9_8

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents