Top

previous chapter Time-Triggered Runtime Verification of Componen...

next chapter Runtime Verification Through Forward Chaining

Hint

Swipe to navigate through the chapters of this book

2015 | OriginalPaper | Chapter

Monitoring for a Decidable Fragment of MTL-\(\int \)

Read first chapter

Authors: André de Matos Pedro, David Pereira, Luís Miguel Pinho, Jorge Sousa Pinto

Publisher: Springer International Publishing

Published in: Runtime Verification

» Get access to the full-text

Abstract

Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTL-\(\int \), we propose a new approach for the runtime verification of hard real-time systems. The novelty of our technique is that it is based on incremental evaluation, allowing us to effectively treat duration properties (which play a crucial role in real-time systems). We describe the two levels of operation of our approach: offline simplification by quantifier removal techniques; and online evaluation of a three-valued interpretation for formulas of our fragment. Our experiments show the applicability of this mechanism as well as the validity of the provided complexity results.

Please log in to get access to this content

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

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

Testen Sie jetzt 30 Tage kostenlos.

inform now

Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996) MathSciNetCrossRefMATH

Alur, R., Henzinger, T.A.: Logics and models of real time: a survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992) CrossRef

Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry. Algorithms and Computation in Mathematics. Springer, Heidelberg (2006) MATH

Bouyer, P., Chevalier, F., Markey, N.: On the expressiveness of TPTL and MTL. Inf. Comput. 208(2), 97–116 (2010) MathSciNetCrossRefMATH

Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.B.: On expressiveness and complexity in real-time model checking. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 124–135. Springer, Heidelberg (2008) CrossRef

Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition: a synopsis. SIGSAM Bull. 10(1), 10–12 (1976) CrossRef

Gordon, R.A.: The Integrals of Lebesgue. Denjoy, Perron, and Henstock. Graduate studies in mathematics. American Mathematical Society, Providence (1994) CrossRefMATH

Hansen, M.R., Van Hung, D.: A theory of duration calculus with application. In: George, C.W., Liu, Z., Woodcock, J. (eds.) Domaine Modeling. LNCS, vol. 4710, pp. 119–176. Springer, Heidelberg (2007) CrossRef

Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning About Systems. Cambridge University Press, New York (2004) CrossRefMATH

10.

Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990) CrossRef

11.

Lakhneche, Y., Hooman, J.: Metric temporal logic with durations. Theor. Comput. Sci. 138(1), 169–199 (1995) MathSciNetCrossRefMATH

12.

Pedro, A.M., Pereira, D., Pinho, L.M., Pinto, J.S.: Logic-based schedulability analysis for compositional hard real-time embedded systems. SIGBED Rev. 12(1), 56–64 (2015) CrossRef

13.

Ničković, D., Piterman, N.: From Mtl to deterministic timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 152–167. Springer, Heidelberg (2010) CrossRef

14.

Ouaknine, J., Worrell, J.B.: Safety metric temporal logic is fully decidable. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 411–425. Springer, Heidelberg (2006) CrossRef

15.

Ouaknine, J., Worrell, J.B.: Some recent results in metric temporal logic. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 1–13. Springer, Heidelberg (2008) CrossRef

16.

Pike, L., Goodloe, A., Morisset, R., Niller, S.: Copilot: a hard real-time runtime monitor. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 345–359. Springer, Heidelberg (2010) CrossRef

17.

Pnueli, A.: The temporal logic of programs. SFCS 1977, pp. 46–57. IEEE Computer Society, Washington (1977)

18.

Shin, I., Lee, I.: Periodic resource model for compositional real-time guarantees. RTSS 2003, pp. 2-. IEEE Computer Society, Washington (2003)

19.

Tarski, A.: Introduction to Logic and to the Methodology of Deductive Sciences. Dover Books on Mathematics Series. Dover Publications, New York (1995) MATH

Title

Monitoring for a Decidable Fragment of MTL-

Book

Runtime Verification

Print ISBN: 978-3-319-23819-7

Electronic ISBN: 978-3-319-23820-3

https://doi.org/10.1007/978-3-319-23820-3

DOI

https://doi.org/10.1007/978-3-319-23820-3_11

Authors:

André de Matos Pedro
David Pereira
Luís Miguel Pinho
Jorge Sousa Pinto

Publisher

Springer International Publishing

Sequence number

Premium Partner

Image Credits