1*afc70ccbSDaniel Bristot de Oliveira.. SPDX-License-Identifier: GPL-2.0 2*afc70ccbSDaniel Bristot de Oliveira 3*afc70ccbSDaniel Bristot de Oliveira== 4*afc70ccbSDaniel Bristot de Oliveirarv 5*afc70ccbSDaniel Bristot de Oliveira== 6*afc70ccbSDaniel Bristot de Oliveira-------------------- 7*afc70ccbSDaniel Bristot de OliveiraRuntime Verification 8*afc70ccbSDaniel Bristot de Oliveira-------------------- 9*afc70ccbSDaniel Bristot de Oliveira 10*afc70ccbSDaniel Bristot de Oliveira:Manual section: 1 11*afc70ccbSDaniel Bristot de Oliveira 12*afc70ccbSDaniel Bristot de OliveiraSYNOPSIS 13*afc70ccbSDaniel Bristot de Oliveira======== 14*afc70ccbSDaniel Bristot de Oliveira 15*afc70ccbSDaniel Bristot de Oliveira**rv** *COMMAND* [*OPTIONS*] 16*afc70ccbSDaniel Bristot de Oliveira 17*afc70ccbSDaniel Bristot de OliveiraDESCRIPTION 18*afc70ccbSDaniel Bristot de Oliveira=========== 19*afc70ccbSDaniel Bristot de Oliveira 20*afc70ccbSDaniel Bristot de OliveiraRuntime Verification (**RV**) is a lightweight (yet rigorous) method 21*afc70ccbSDaniel Bristot de Oliveirafor formal verification with a practical approach for complex systems. 22*afc70ccbSDaniel Bristot de OliveiraInstead of relying on a fine-grained model of a system (e.g., a 23*afc70ccbSDaniel Bristot de Oliveirare-implementation a instruction level), RV works by analyzing the trace 24*afc70ccbSDaniel Bristot de Oliveiraof the system's actual execution, comparing it against a formal 25*afc70ccbSDaniel Bristot de Oliveiraspecification of the system behavior. 26*afc70ccbSDaniel Bristot de Oliveira 27*afc70ccbSDaniel Bristot de OliveiraThe **rv** tool provides the interface for a collection of runtime 28*afc70ccbSDaniel Bristot de Oliveiraverification (rv) monitors. 29*afc70ccbSDaniel Bristot de Oliveira 30*afc70ccbSDaniel Bristot de OliveiraCOMMANDS 31*afc70ccbSDaniel Bristot de Oliveira======== 32*afc70ccbSDaniel Bristot de Oliveira 33*afc70ccbSDaniel Bristot de Oliveira**list** 34*afc70ccbSDaniel Bristot de Oliveira 35*afc70ccbSDaniel Bristot de Oliveira List all available monitors. 36*afc70ccbSDaniel Bristot de Oliveira 37*afc70ccbSDaniel Bristot de Oliveira**mon** 38*afc70ccbSDaniel Bristot de Oliveira 39*afc70ccbSDaniel Bristot de Oliveira Run monitor. 40*afc70ccbSDaniel Bristot de Oliveira 41*afc70ccbSDaniel Bristot de OliveiraOPTIONS 42*afc70ccbSDaniel Bristot de Oliveira======= 43*afc70ccbSDaniel Bristot de Oliveira 44*afc70ccbSDaniel Bristot de Oliveira**-h**, **--help** 45*afc70ccbSDaniel Bristot de Oliveira 46*afc70ccbSDaniel Bristot de Oliveira Display the help text. 47*afc70ccbSDaniel Bristot de Oliveira 48*afc70ccbSDaniel Bristot de OliveiraFor other options, see the man page for the corresponding command. 49*afc70ccbSDaniel Bristot de Oliveira 50*afc70ccbSDaniel Bristot de OliveiraSEE ALSO 51*afc70ccbSDaniel Bristot de Oliveira======== 52*afc70ccbSDaniel Bristot de Oliveira 53*afc70ccbSDaniel Bristot de Oliveira**rv-list**\(1), **rv-mon**\(1) 54*afc70ccbSDaniel Bristot de Oliveira 55*afc70ccbSDaniel Bristot de OliveiraLinux kernel *RV* documentation: 56*afc70ccbSDaniel Bristot de Oliveira<https://www.kernel.org/doc/html/latest/trace/rv/index.html> 57*afc70ccbSDaniel Bristot de Oliveira 58*afc70ccbSDaniel Bristot de OliveiraAUTHOR 59*afc70ccbSDaniel Bristot de Oliveira====== 60*afc70ccbSDaniel Bristot de Oliveira 61*afc70ccbSDaniel Bristot de OliveiraDaniel Bristot de Oliveira <bristot@kernel.org> 62*afc70ccbSDaniel Bristot de Oliveira 63*afc70ccbSDaniel Bristot de Oliveira.. include:: common_appendix.rst 64