162306a36Sopenharmony_ci.. SPDX-License-Identifier: GPL-2.0 262306a36Sopenharmony_ci 362306a36Sopenharmony_ci== 462306a36Sopenharmony_cirv 562306a36Sopenharmony_ci== 662306a36Sopenharmony_ci-------------------- 762306a36Sopenharmony_ciRuntime Verification 862306a36Sopenharmony_ci-------------------- 962306a36Sopenharmony_ci 1062306a36Sopenharmony_ci:Manual section: 1 1162306a36Sopenharmony_ci 1262306a36Sopenharmony_ciSYNOPSIS 1362306a36Sopenharmony_ci======== 1462306a36Sopenharmony_ci 1562306a36Sopenharmony_ci**rv** *COMMAND* [*OPTIONS*] 1662306a36Sopenharmony_ci 1762306a36Sopenharmony_ciDESCRIPTION 1862306a36Sopenharmony_ci=========== 1962306a36Sopenharmony_ci 2062306a36Sopenharmony_ciRuntime Verification (**RV**) is a lightweight (yet rigorous) method 2162306a36Sopenharmony_cifor formal verification with a practical approach for complex systems. 2262306a36Sopenharmony_ciInstead of relying on a fine-grained model of a system (e.g., a 2362306a36Sopenharmony_cire-implementation a instruction level), RV works by analyzing the trace 2462306a36Sopenharmony_ciof the system's actual execution, comparing it against a formal 2562306a36Sopenharmony_cispecification of the system behavior. 2662306a36Sopenharmony_ci 2762306a36Sopenharmony_ciThe **rv** tool provides the interface for a collection of runtime 2862306a36Sopenharmony_civerification (rv) monitors. 2962306a36Sopenharmony_ci 3062306a36Sopenharmony_ciCOMMANDS 3162306a36Sopenharmony_ci======== 3262306a36Sopenharmony_ci 3362306a36Sopenharmony_ci**list** 3462306a36Sopenharmony_ci 3562306a36Sopenharmony_ci List all available monitors. 3662306a36Sopenharmony_ci 3762306a36Sopenharmony_ci**mon** 3862306a36Sopenharmony_ci 3962306a36Sopenharmony_ci Run monitor. 4062306a36Sopenharmony_ci 4162306a36Sopenharmony_ciOPTIONS 4262306a36Sopenharmony_ci======= 4362306a36Sopenharmony_ci 4462306a36Sopenharmony_ci**-h**, **--help** 4562306a36Sopenharmony_ci 4662306a36Sopenharmony_ci Display the help text. 4762306a36Sopenharmony_ci 4862306a36Sopenharmony_ciFor other options, see the man page for the corresponding command. 4962306a36Sopenharmony_ci 5062306a36Sopenharmony_ciSEE ALSO 5162306a36Sopenharmony_ci======== 5262306a36Sopenharmony_ci 5362306a36Sopenharmony_ci**rv-list**\(1), **rv-mon**\(1) 5462306a36Sopenharmony_ci 5562306a36Sopenharmony_ciLinux kernel *RV* documentation: 5662306a36Sopenharmony_ci<https://www.kernel.org/doc/html/latest/trace/rv/index.html> 5762306a36Sopenharmony_ci 5862306a36Sopenharmony_ciAUTHOR 5962306a36Sopenharmony_ci====== 6062306a36Sopenharmony_ci 6162306a36Sopenharmony_ciDaniel Bristot de Oliveira <bristot@kernel.org> 6262306a36Sopenharmony_ci 6362306a36Sopenharmony_ci.. include:: common_appendix.rst 64