1102227b9SDaniel Bristot de Oliveira# SPDX-License-Identifier: GPL-2.0-only 2102227b9SDaniel Bristot de Oliveira# 3102227b9SDaniel Bristot de Oliveiramenuconfig RV 4102227b9SDaniel Bristot de Oliveira bool "Runtime Verification" 5102227b9SDaniel Bristot de Oliveira depends on TRACING 6102227b9SDaniel Bristot de Oliveira help 7102227b9SDaniel Bristot de Oliveira Enable the kernel runtime verification infrastructure. RV is a 8102227b9SDaniel Bristot de Oliveira lightweight (yet rigorous) method that complements classical 9102227b9SDaniel Bristot de Oliveira exhaustive verification techniques (such as model checking and 10102227b9SDaniel Bristot de Oliveira theorem proving). RV works by analyzing the trace of the system's 11102227b9SDaniel Bristot de Oliveira actual execution, comparing it against a formal specification of 12102227b9SDaniel Bristot de Oliveira the system behavior. 13*04acadcbSDaniel Bristot de Oliveira 14*04acadcbSDaniel Bristot de Oliveiraconfig RV_REACTORS 15*04acadcbSDaniel Bristot de Oliveira bool "Runtime verification reactors" 16*04acadcbSDaniel Bristot de Oliveira default y 17*04acadcbSDaniel Bristot de Oliveira depends on RV 18*04acadcbSDaniel Bristot de Oliveira help 19*04acadcbSDaniel Bristot de Oliveira Enables the online runtime verification reactors. A runtime 20*04acadcbSDaniel Bristot de Oliveira monitor can cause a reaction to the detection of an exception 21*04acadcbSDaniel Bristot de Oliveira on the model's execution. By default, the monitors have 22*04acadcbSDaniel Bristot de Oliveira tracing reactions, printing the monitor output via tracepoints, 23*04acadcbSDaniel Bristot de Oliveira but other reactions can be added (on-demand) via this interface. 24