summaryrefslogtreecommitdiffstats
path: root/Documentation/tools/rv/rv.rst
diff options
context:
space:
mode:
Diffstat (limited to 'Documentation/tools/rv/rv.rst')
-rw-r--r--Documentation/tools/rv/rv.rst63
1 files changed, 63 insertions, 0 deletions
diff --git a/Documentation/tools/rv/rv.rst b/Documentation/tools/rv/rv.rst
new file mode 100644
index 0000000000..cee93dc21a
--- /dev/null
+++ b/Documentation/tools/rv/rv.rst
@@ -0,0 +1,63 @@
+.. SPDX-License-Identifier: GPL-2.0
+
+==
+rv
+==
+--------------------
+Runtime Verification
+--------------------
+
+:Manual section: 1
+
+SYNOPSIS
+========
+
+**rv** *COMMAND* [*OPTIONS*]
+
+DESCRIPTION
+===========
+
+Runtime Verification (**RV**) is a lightweight (yet rigorous) method
+for formal verification with a practical approach for complex systems.
+Instead of relying on a fine-grained model of a system (e.g., a
+re-implementation a instruction level), RV works by analyzing the trace
+of the system's actual execution, comparing it against a formal
+specification of the system behavior.
+
+The **rv** tool provides the interface for a collection of runtime
+verification (rv) monitors.
+
+COMMANDS
+========
+
+**list**
+
+ List all available monitors.
+
+**mon**
+
+ Run monitor.
+
+OPTIONS
+=======
+
+**-h**, **--help**
+
+ Display the help text.
+
+For other options, see the man page for the corresponding command.
+
+SEE ALSO
+========
+
+**rv-list**\(1), **rv-mon**\(1)
+
+Linux kernel *RV* documentation:
+<https://www.kernel.org/doc/html/latest/trace/rv/index.html>
+
+AUTHOR
+======
+
+Daniel Bristot de Oliveira <bristot@kernel.org>
+
+.. include:: common_appendix.rst