LARVA: a tool for runtime monitoring of Java programs. 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 a tool LARVA, for the runtime verification of real-time properties of Java programs. Properties can be expressed in a number of notations, including timed-automata enriched with stopwatches, Lustre, and a subset of 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, it gives other useful information, as for instance what is the impact of monitoring the system with respect to the monitored properties.
Keywords for this software
References in zbMATH (referenced in 6 articles )
Showing results 1 to 6 of 6.
- Renard, Matthieu; Falcone, Yliès; Rollet, Antoine; Jéron, Thierry; Marchand, Hervé: Optimal enforcement of (timed) properties with uncontrollable events (2019)
- Ahrendt, Wolfgang; Chimento, Jesús Mauricio; Pace, Gordon J.; Schneider, Gerardo: Verifying data- and control-oriented properties combining static and runtime verification: theory and tools (2017)
- Neykova, Rumyana; Bocchi, Laura; Yoshida, Nobuko: Timed runtime monitoring for multiparty conversations (2017)
- de Boer, Frank S.; de Gouw, Stijn: Combining monitoring with run-time assertion checking (2014)
- Pinisetty, Srinivas; Falcone, Yliès; Jéron, Thierry; Marchand, Hervé; Rollet, Antoine; Nguena Timo, Omer: Runtime enforcement of timed properties revisited (2014)
- Colombo, Christian; Pace, Gordon J.; Abela, Patrick: Safer asynchronous runtime monitoring using compensations (2012)