Date Added: Aug 2009
The use of runtime verification, as a lightweight approach to guarantee properties of systems, has been increasingly employed on real-life software. This paper presents 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.