Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets
Contributo in Atti di convegno
Data di Pubblicazione:
2017
Citazione:
Event-Based Runtime Verification of Temporal Properties Using Time Basic Petri Nets / M. Camilli, A. Gargantini, P. Scandurra, C. Bellettini (LECTURE NOTES IN COMPUTER SCIENCE). - In: NASA Formal Methods / [a cura di] C. Barrett, M. Davies, T. Kahsai. - [s.l] : Springer, 2017 Apr 09. - ISBN 9783319572871. - pp. 115-130 (( Intervento presentato al 9. convegno Nasa Formal Methods tenutosi a Moffett Field nel 2017 [10.1007/978-3-319-57288-8_8].
Abstract:
We introduce a formal framework to provide an efficient event-based monitoring technique, and we describe its current implementation as the MahaRAJA software tool. The framework enables the quantitative runtime verification of temporal properties extracted from occurring events on Java programs. The monitor continuously evaluates the conformance of the concrete implementation with respect to its formal specification given in terms of Time Basic Petri nets, a particular timed extension of Petri nets. The system under test is instrumented by using simple Java annotations on methods to link the implementation to its formal model. This allows a separation between implementation and specification that can be used for other purposes such as formal verification, simulation, and model-based testing. The tool has been successfully used to monitor at runtime and test a number of benchmarking case-studies. Experiments show that our approach introduces bounded overhead and effectively reduces the involvement of the monitor at run time by using negligible auxiliary memory. A comparison with a number of state-of-the-art runtime verification tools is also presented.
Tipologia IRIS:
03 - Contributo in volume
Keywords:
Formal methods @ runtime; Petri nets; Runtime verification; Temporal properties; Timing analysis
Elenco autori:
M. Camilli, A. Gargantini, P. Scandurra, C. Bellettini
Link alla scheda completa:
Titolo del libro:
NASA Formal Methods