TY - GEN
T1 - NuRV
T2 - 19th International Conference on Runtime Verification, RV 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019
AU - Cimatti, Alessandro
AU - Tian, Chun
AU - Tonetta, Stefano
N1 - Publisher Copyright:
© 2019, The Author(s).
PY - 2019
Y1 - 2019
N2 - We present NuRV, an extension of the nuXmv model checker for assumption-based LTL runtime verification with partial observability and resets. The tool provides some new commands for online/offline monitoring and code generations into standalone monitor code. Using the online/offline monitor, LTL properties can be verified incrementally on finite traces from the system under scrutiny. The code generation currently supports C, C++, Common Lisp and Java, and is extensible. Furthermore, from the same internal monitor automaton, the monitor can be generated into SMV modules, whose characteristics can be verified by Model Checking using nuXmv. We show the architecture, functionalities and some use scenarios of NuRV, and we compare the performance of generated monitor code (in Java) with those generated by a similar tool, RV-Monitor. We show that, using a benchmark from Dwyer’s LTL patterns, besides the capacity of generating monitors for long LTL formulae, our Java-based monitors are about 200x faster than RV-Monitor at generation-time and 2–5x faster at runtime.
AB - We present NuRV, an extension of the nuXmv model checker for assumption-based LTL runtime verification with partial observability and resets. The tool provides some new commands for online/offline monitoring and code generations into standalone monitor code. Using the online/offline monitor, LTL properties can be verified incrementally on finite traces from the system under scrutiny. The code generation currently supports C, C++, Common Lisp and Java, and is extensible. Furthermore, from the same internal monitor automaton, the monitor can be generated into SMV modules, whose characteristics can be verified by Model Checking using nuXmv. We show the architecture, functionalities and some use scenarios of NuRV, and we compare the performance of generated monitor code (in Java) with those generated by a similar tool, RV-Monitor. We show that, using a benchmark from Dwyer’s LTL patterns, besides the capacity of generating monitors for long LTL formulae, our Java-based monitors are about 200x faster than RV-Monitor at generation-time and 2–5x faster at runtime.
UR - https://www.scopus.com/pages/publications/85075737595
U2 - 10.1007/978-3-030-32079-9_23
DO - 10.1007/978-3-030-32079-9_23
M3 - Conference Paper
AN - SCOPUS:85075737595
SN - 9783030320782
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 382
EP - 392
BT - Runtime Verification
A2 - Finkbeiner, Bernd
A2 - Mariani, Leonardo
PB - Springer
Y2 - 8 October 2019 through 11 October 2019
ER -