Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2009)
Nov. 23, 2009 to Nov. 27, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2009.13
The use of runtime verification, as a lightweight approach to guarantee properties of systems, has been increasingly employed on real-life software. In this paper, we present the tool LARVA, for the runtime verification of properties of Java programs, including real-time properties. Properties can be expressed in a number of notations, including timed-automata enriched with stopwatches, Lustre, and a subset of the duration calculus. The tool has been successfully used on a number of case-studies, including an industrial system handling financial transactions. LARVA also performs analysis of real-time properties, to calculate, if possible, an upper-bound on the memory and temporal overheads induced by monitoring. Moreover, through property analysis, LARVA assesses the impact of slowing down the system through monitoring, on the satisfaction of the properties.
runtime verification, monitoring of real-time properties, resource-bounded monitoring
C. Colombo, G. J. Pace and G. Schneider, "LARVA --- Safer Monitoring of Real-Time Java Programs (Tool Paper)," 2009 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2009)(SEFM), Hanoi, 2009, pp. 33-37.