1 .. SPDX-License-Identifier: GPL-2.0 1 .. SPDX-License-Identifier: GPL-2.0
2 2
3 == 3 ==
4 rv 4 rv
5 == 5 ==
6 -------------------- 6 --------------------
7 Runtime Verification 7 Runtime Verification
8 -------------------- 8 --------------------
9 9
10 :Manual section: 1 10 :Manual section: 1
11 11
12 SYNOPSIS 12 SYNOPSIS
13 ======== 13 ========
14 14
15 **rv** *COMMAND* [*OPTIONS*] 15 **rv** *COMMAND* [*OPTIONS*]
16 16
17 DESCRIPTION 17 DESCRIPTION
18 =========== 18 ===========
19 19
20 Runtime Verification (**RV**) is a lightweight 20 Runtime Verification (**RV**) is a lightweight (yet rigorous) method
21 for formal verification with a practical appro 21 for formal verification with a practical approach for complex systems.
22 Instead of relying on a fine-grained model of 22 Instead of relying on a fine-grained model of a system (e.g., a
23 re-implementation a instruction level), RV wor 23 re-implementation a instruction level), RV works by analyzing the trace
24 of the system's actual execution, comparing it 24 of the system's actual execution, comparing it against a formal
25 specification of the system behavior. 25 specification of the system behavior.
26 26
27 The **rv** tool provides the interface for a c 27 The **rv** tool provides the interface for a collection of runtime
28 verification (rv) monitors. 28 verification (rv) monitors.
29 29
30 COMMANDS 30 COMMANDS
31 ======== 31 ========
32 32
33 **list** 33 **list**
34 34
35 List all available monitors. 35 List all available monitors.
36 36
37 **mon** 37 **mon**
38 38
39 Run monitor. 39 Run monitor.
40 40
41 OPTIONS 41 OPTIONS
42 ======= 42 =======
43 43
44 **-h**, **--help** 44 **-h**, **--help**
45 45
46 Display the help text. 46 Display the help text.
47 47
48 For other options, see the man page for the co 48 For other options, see the man page for the corresponding command.
49 49
50 SEE ALSO 50 SEE ALSO
51 ======== 51 ========
52 52
53 **rv-list**\(1), **rv-mon**\(1) 53 **rv-list**\(1), **rv-mon**\(1)
54 54
55 Linux kernel *RV* documentation: 55 Linux kernel *RV* documentation:
56 <https://www.kernel.org/doc/html/latest/trace/ 56 <https://www.kernel.org/doc/html/latest/trace/rv/index.html>
57 57
58 AUTHOR 58 AUTHOR
59 ====== 59 ======
60 60
61 Daniel Bristot de Oliveira <bristot@kernel.org> 61 Daniel Bristot de Oliveira <bristot@kernel.org>
62 62
63 .. include:: common_appendix.rst 63 .. include:: common_appendix.rst
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.