zbMATH — the first resource for mathematics

Time-triggered runtime verification. (English) Zbl 1291.68248
Summary: The goal of runtime verification is to monitor the behavior of a system to check its conformance to a set of desirable logical properties. The literature of runtime verification mostly focuses on event-triggered solutions, where a monitor is invoked when an event of interest occurs (e.g., change in the value of some variable). At invocation, the monitor evaluates the set of properties of the system that are affected by the occurrence of the event. This constant invocation introduces two major defects to the system under scrutiny at run time: (1) significant overhead, and (2) unpredictability of behavior. These defects are serious obstacles when applying runtime verification on safety-critical systems that are time-sensitive by nature.
To circumvent the aforementioned defects in runtime verification, in this article, we introduce a novel time-triggered approach, where the monitor takes samples from the system with a constant frequency, in order to analyze the system’s health. We describe the formal semantics of time-triggered monitoring and discuss how to optimize the sampling period using minimum auxiliary memory. We show that such optimization is NP-complete and consequently introduce a mapping to Integer Linear Programming. Experiments on a real-time benchmark suite show that our approach introduces bounded overhead and effectively reduces the involvement of the monitor at run time by using negligible auxiliary memory. We also show that in some cases it is even possible to reduce the overall overhead of runtime verification by using our time-triggered approach when the structure of the system allows choosing a long enough sampling period.

68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] SNU real-time benchmarks. http://www.cprover.org/goto-cc/examples/snu.html
[2] Alur, R; Dill, D, A theory of timed automata, Theor Comput Sci, 126, 183-235, (1994) · Zbl 0803.68071
[3] Artho, C; Drusinksy, D; Goldberg, A; Havelund, K; Lowry, M; Pasareanu, C; Roşu, G; Visser, W, Experiments with test case generation and runtime analysis, ASM’03 · Zbl 1021.68503
[4] Barringer, H; Goldberg, A; Havelund, K; Sen, K, Rule-based runtime verification, VMCAI’04 · Zbl 1202.68243
[5] Bauer A, Leucker M, Schallhart C Runtime verification for LTL and TLTL. ACM transactions on software Engineering and Methodology (TOSEM) (2009, in press)
[6] Bauer, A; Leucker, M; Schallhart, C, Comparing LTL semantics for runtime verification, J Log Comput, 20, 651-674, (2010) · Zbl 1213.68363
[7] Bauer, A; Leucker, M; Schallhart, C, Runtime verification for LTL and TLTL, ACM Trans Softw Eng Methodol, 20, 14, (2011)
[8] Bodden, E, Efficient hybrid typestate analysis by determining continuation-equivalent states, 5-14, (2010)
[9] Bodden, E; Hendren, L; Lam, P; Lhoták, O; Naeem, N, Collaborative runtime verification with tracematches, RV’07 · Zbl 1213.68365
[10] Bodden, E; Hendren, L; Lhoták, O, A staged static program analysis to improve the performance of runtime monitoring, ECOOP’07
[11] Bodden, E; Lam, P; Hendren, L, Finding programming errors earlier by evaluating runtime monitors ahead-of-time, FSE’08
[12] Bonakdarpour, B; Navabpour, S; Fischmeister, S, Sampling-based runtime verification, 88-102, (2011)
[13] Chang, EY; Manna, Z; Pnueli, A, Characterization of temporal property classes, 474-486, (1992)
[14] Chen, F; Roşu, G, Java-MOP: a monitoring oriented programming environment for Java, 546-550, (2005) · Zbl 1087.68550
[15] Chen, F; Roşu, G, Java-mop: a monitoring oriented programming environment for Java, TACAS’05 · Zbl 1087.68550
[16] Colin S, Mariani L (2005) Run-time verification. LNCS, vol 3472. Springer, Berlin. Chapter 18
[17] d’Amorim, M; Rosu, G, Efficient monitoring of omega-languages, 364-378, (2005) · Zbl 1081.68050
[18] Dwyer, MB; Kinneer, A; Elbaum, S, Adaptive online program analysis, ICSE ’07
[19] Falcone, Y; Fernandez, J-C; Mounier, L, Runtime verification of safety-progress properties, 40-59, (2009)
[20] Fischmeister, S; Ba, Y, Sampling-based program execution monitoring, 133-142, (2010)
[21] Giannakopoulou, D; Havelund, K, Automata-based verification of temporal properties on running programs, 412-416, (2001)
[22] Havelund, K, Runtime verification of C programs, TestCom ’08/FATES ’08
[23] Havelund K, Goldberg A (2008) Verify your runs, pp 374-383
[24] Havelund, K; Rosu, G, Monitoring Java programs with Java pathexplorer, Electron Notes Theor Comput Sci, 55, 200-217, (2001)
[25] Havelund, K; Rosu, G, Monitoring programs using rewriting, 135-143, (2001)
[26] Havelund, K; Rosu, G, Synthesizing monitors for safety properties, 342-356, (2002) · Zbl 1043.68534
[27] Havelund, K; Rosu, G, Efficient monitoring of safety properties, Softw Tools Technol Transf, 6, 158-173, (2004)
[28] Huang, X; Seyster, J; Callanan, S; Dixit, K; Grosu, R; Smolka, SA; Stoller, SD; Zadok, E, Software monitoring with controllable overhead, Softw Tools Technol Transf, 14, 327-347, (2012)
[29] Karp, RM, Reducibility among combinatorial problems, 85-103, (1972)
[30] Kim, M; Lee, I; Sammapun, U; Shin, J; Sokolsky, O, Monitoring, checking, and steering of real-time systems, Electron Notes Theor Comput Sci, 70, 95-111, (2002)
[31] Kim, M; Viswanathan, M; Ben-Abdallah, H; Kannan, S; Lee, I; Sokolsky, O, Formally specified monitoring of temporal properties, 114-122, (1999)
[32] Kim, M; Viswanathan, M; Kannan, S; Lee, I; Sokolsky, O, Java-mac: a run-time assurance approach for Java programs, Form Methods Syst Des, 24, 129-155, (2004) · Zbl 1073.68552
[33] Kim, M; Viswanathan, M; Kannan, S; Lee, I; Sokolsky, O, Java-mac: a run-time assurance approach for Java programs, Form Methods Syst Des, 24, 129-155, (2004) · Zbl 1073.68552
[34] Kupferman, O; Vardi, MY, Model checking of safety properties, 172-183, (1999) · Zbl 1046.68597
[35] Lattner, C; Adve, V, LLVM: a compilation framework for lifelong program analysis and transformation, 75, (2004)
[36] Lee, I; Kannan, S; Kim, M; Sokolsky, O; Viswanathan, M, Runtime assurance based on formal specifications, 279-287, (1999)
[37] ILP solver lp_solve. http://lpsolve.sourceforge.net/5.5/
[38] Manna, Z; Pnueli, A, A hierarchy of temporal properties, 377-410, (1990)
[39] Meredith, P; Jin, D; Chen, F; Roşu, G, Efficient monitoring of parametric context-free patterns, Autom Softw Eng, 17, 149-180, (2010)
[40] Navabpour, S; Wu, CW; Bonakdarpour, B; Fischmeister, S, Efficient techniques for near-optimal instrumentation in time-triggered runtime verification, 208-222, (2011)
[41] Pike, L; Goodloe, A; Morisset, R; Niller, S, Copilot: a hard real-time runtime monitor, 345-359, (2010)
[42] Pnueli, A, The temporal logic of programs, 46-57, (1977)
[43] Pnueli, A; Zaks, A, PSL model checking and run-time verification via testers, 573-586, (2006)
[44] Raskin, J-F; Schobbens, P-Y, The logic of event clocks—decidability, complexity and expressiveness, J Autom Lang Comb, 4, 247-286, (1999) · Zbl 0978.03015
[45] Rosu, G; Chen, F; Ball, T, Synthesizing monitors for safety properties: this time with calls and returns, 51-68, (2008)
[46] Seyster, J; Dixit, K; Huang, X; Grosu, R; Havelund, K; Smolka, SA; Stoller, SD; Zadok, E, Aspect-oriented instrumentation with GCC, 405-420, (2010) · Zbl 1284.68153
[47] Stoller, SD; Bartocci, E; Seyster, J; Grosu, R; Havelund, K; Smolka, SA; Zadok, E, Runtime verification with state estimation, 193-207, (2011)
[48] Stolz, V; Bodden, E, Temporal assertions using aspectj, Electron Notes Theor Comput Sci, 144, 109-124, (2006)
[49] Zhou, W; Sokolsky, O; Loo, BT; Lee, I, Mac: distributed monitoring and checking, 184-201, (2009)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.