Calculus-based Runtime Verification

Authors: Xuan Qi, Changzhi Zhao

Abstract:

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.

Keywords: calculus, eagle logic, monitor synthesis, runtime verification

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1084390

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.