summaryrefslogtreecommitdiff
path: root/tools/verification/rv/README.txt
diff options
context:
space:
mode:
Diffstat (limited to 'tools/verification/rv/README.txt')
-rw-r--r--tools/verification/rv/README.txt38
1 files changed, 38 insertions, 0 deletions
diff --git a/tools/verification/rv/README.txt b/tools/verification/rv/README.txt
new file mode 100644
index 000000000000..e96be0dfff59
--- /dev/null
+++ b/tools/verification/rv/README.txt
@@ -0,0 +1,38 @@
+RV: Runtime Verification
+
+Runtime Verification (RV) is a lightweight (yet rigorous) method that
+complements classical exhaustive verification techniques (such as model
+checking and theorem proving) with a more practical approach for
+complex systems.
+
+The rv tool is the interface for a collection of monitors that aim
+analysing the logical and timing behavior of Linux.
+
+Installing RV
+
+RV depends on the following libraries and tools:
+
+ - libtracefs
+ - libtraceevent
+
+It also depends on python3-docutils to compile man pages.
+
+For development, we suggest the following steps for compiling rtla:
+
+ $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtraceevent.git
+ $ cd libtraceevent/
+ $ make
+ $ sudo make install
+ $ cd ..
+ $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtracefs.git
+ $ cd libtracefs/
+ $ make
+ $ sudo make install
+ $ cd ..
+ $ cd $rv_src
+ $ make
+ $ sudo make install
+
+For further information, please see rv manpage and the kernel documentation:
+ Runtime Verification:
+ Documentation/trace/rv/runtime-verification.rst