1 RV: Runtime Verification 1 RV: Runtime Verification
2 2
3 Runtime Verification (RV) is a lightweight (ye 3 Runtime Verification (RV) is a lightweight (yet rigorous) method that
4 complements classical exhaustive verification 4 complements classical exhaustive verification techniques (such as model
5 checking and theorem proving) with a more prac 5 checking and theorem proving) with a more practical approach for
6 complex systems. 6 complex systems.
7 7
8 The rv tool is the interface for a collection 8 The rv tool is the interface for a collection of monitors that aim
9 analysing the logical and timing behavior of L 9 analysing the logical and timing behavior of Linux.
10 10
11 Installing RV 11 Installing RV
12 12
13 RV depends on the following libraries and tool 13 RV depends on the following libraries and tools:
14 14
15 - libtracefs 15 - libtracefs
16 - libtraceevent 16 - libtraceevent
17 17
18 It also depends on python3-docutils to compile 18 It also depends on python3-docutils to compile man pages.
19 19
20 For development, we suggest the following step 20 For development, we suggest the following steps for compiling rtla:
21 21
22 $ git clone git://git.kernel.org/pub/scm/lib 22 $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtraceevent.git
23 $ cd libtraceevent/ 23 $ cd libtraceevent/
24 $ make 24 $ make
25 $ sudo make install 25 $ sudo make install
26 $ cd .. 26 $ cd ..
27 $ git clone git://git.kernel.org/pub/scm/lib 27 $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtracefs.git
28 $ cd libtracefs/ 28 $ cd libtracefs/
29 $ make 29 $ make
30 $ sudo make install 30 $ sudo make install
31 $ cd .. 31 $ cd ..
32 $ cd $rv_src 32 $ cd $rv_src
33 $ make 33 $ make
34 $ sudo make install 34 $ sudo make install
35 35
36 For further information, please see rv manpage 36 For further information, please see rv manpage and the kernel documentation:
37 Runtime Verification: 37 Runtime Verification:
38 Documentation/trace/rv/runtime-verificatio 38 Documentation/trace/rv/runtime-verification.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.