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