162306a36Sopenharmony_ciRV: Runtime Verification 262306a36Sopenharmony_ci 362306a36Sopenharmony_ciRuntime Verification (RV) is a lightweight (yet rigorous) method that 462306a36Sopenharmony_cicomplements classical exhaustive verification techniques (such as model 562306a36Sopenharmony_cichecking and theorem proving) with a more practical approach for 662306a36Sopenharmony_cicomplex systems. 762306a36Sopenharmony_ci 862306a36Sopenharmony_ciThe rv tool is the interface for a collection of monitors that aim 962306a36Sopenharmony_cianalysing the logical and timing behavior of Linux. 1062306a36Sopenharmony_ci 1162306a36Sopenharmony_ciInstalling RV 1262306a36Sopenharmony_ci 1362306a36Sopenharmony_ciRV depends on the following libraries and tools: 1462306a36Sopenharmony_ci 1562306a36Sopenharmony_ci - libtracefs 1662306a36Sopenharmony_ci - libtraceevent 1762306a36Sopenharmony_ci 1862306a36Sopenharmony_ciIt also depends on python3-docutils to compile man pages. 1962306a36Sopenharmony_ci 2062306a36Sopenharmony_ciFor development, we suggest the following steps for compiling rtla: 2162306a36Sopenharmony_ci 2262306a36Sopenharmony_ci $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtraceevent.git 2362306a36Sopenharmony_ci $ cd libtraceevent/ 2462306a36Sopenharmony_ci $ make 2562306a36Sopenharmony_ci $ sudo make install 2662306a36Sopenharmony_ci $ cd .. 2762306a36Sopenharmony_ci $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtracefs.git 2862306a36Sopenharmony_ci $ cd libtracefs/ 2962306a36Sopenharmony_ci $ make 3062306a36Sopenharmony_ci $ sudo make install 3162306a36Sopenharmony_ci $ cd .. 3262306a36Sopenharmony_ci $ cd $rv_src 3362306a36Sopenharmony_ci $ make 3462306a36Sopenharmony_ci $ sudo make install 3562306a36Sopenharmony_ci 3662306a36Sopenharmony_ciFor further information, please see rv manpage and the kernel documentation: 3762306a36Sopenharmony_ci Runtime Verification: 3862306a36Sopenharmony_ci Documentation/trace/rv/runtime-verification.rst 39