Calculus-based Runtime Verification

In this paper, a uniform calculus-based approach for synthesizing monitors checking correctness properties specified by a large variety of logics at runtime is provided, including future and past time logics, interval logics, state machine and parameterized temporal logics. We present a calculus mechanism to synthesize monitors from the logical specification for the incremental analysis of execution traces during test and real run. The monitor detects both good and bad prefix of a particular kind, namely those that are informative for the property under investigation. We elaborate the procedure of calculus as monitors.

Authors:

• Xuan Qi
• Changzhi Zhao

Keywords:

• calculus
• eagle logic
• monitor synthesis
• runtime verification

References:

[1] Kupferman, O. and M. Y. Vardi, "Model checking of safety properties,"
in: N. Halbwachs and D. Peled, editors, Computer Aided Verification:
11th International Conference Proceedings, CAV-99, Trento, Italy, July
6-10, 1999 (LNCS 1633) (1999), pp.172-183.
[2] Pnueli, A. "The temporal logic of programs." In: Proceedings of the 18th
IEEE Symposium on the Foundations of Computer Science (FOCS), 1977,
pp.46-57.
[3] Havelund, K., Rosu, G. "Monitoring Programs using rewriting." In
proceedings of Inter- national Conference on Automated Software
Engineering (ASE-01), 2001, pp.135-143.
[4] Havelun, K., Rosu, G. "Synthesizing monitors for Safety Properties." In
Tools and Algorithms for Construction and Analysis of Systems
(TACAS-02), 2002, pp.342-356.
[5] Drusinsky, D. "The Temporal Rover and the ATG Rover." In SPIN Model
Checking and Software Verification, volume 1885 of LNCS, 2000,
pp.323-330.
[6] Drusinsky, D. "Monitoring Temporal Rules Combined with Time Series."
In CAV-03, volume 2725 of LNCS, 2003, pp.114-118.
[7] Finkbeiner, B., Sipma, H. "Checking Finite Traces using Alternating
Automata." In Proceedings of the 1st International Workshop on Runtime
Verification(RV-01), 2001, pp.44-60.
[8] Giannakopoulou, D., Havelund, K. "Automata-Based Verification of
Temporal Properties on Running Programs." In Proceedings of
International Conference on Automated Software Engineering(ASE-01),
2001, pp. 412-416.
[9] Barringer, H., Goldberg, A., Havelund, K., and Sen, K. "Eagle Monitors
by Collecting Facts and Generating Obligations." Pre-Print CSPP-26,
University of Manchester, Department of Computer Science, 2003.
[10] Barringer, H., Goldberg, A., Havelund, K., and Sen, K. "Rule-Based
Runtime Verification." In Proceedings of Fifth International Conference
on Verification, Model Checking and Abstract Interpretation
(VMCAI-04), 2004.
[11] Geilen, M. "On the construction of monitors for temporal logic
properties." In Electronic Notes in Theoretical Computer Science, 55,
2001.