1102227b9SDaniel Bristot de Oliveira# SPDX-License-Identifier: GPL-2.0-only 2102227b9SDaniel Bristot de Oliveira# 3*79257534SDaniel Bristot de Oliveiraconfig DA_MON_EVENTS 4*79257534SDaniel Bristot de Oliveira bool 5*79257534SDaniel Bristot de Oliveira 6*79257534SDaniel Bristot de Oliveiraconfig DA_MON_EVENTS_IMPLICIT 7*79257534SDaniel Bristot de Oliveira select DA_MON_EVENTS 8*79257534SDaniel Bristot de Oliveira bool 9*79257534SDaniel Bristot de Oliveira 10*79257534SDaniel Bristot de Oliveiraconfig DA_MON_EVENTS_ID 11*79257534SDaniel Bristot de Oliveira select DA_MON_EVENTS 12*79257534SDaniel Bristot de Oliveira bool 13*79257534SDaniel Bristot de Oliveira 14102227b9SDaniel Bristot de Oliveiramenuconfig RV 15102227b9SDaniel Bristot de Oliveira bool "Runtime Verification" 16102227b9SDaniel Bristot de Oliveira depends on TRACING 17102227b9SDaniel Bristot de Oliveira help 18102227b9SDaniel Bristot de Oliveira Enable the kernel runtime verification infrastructure. RV is a 19102227b9SDaniel Bristot de Oliveira lightweight (yet rigorous) method that complements classical 20102227b9SDaniel Bristot de Oliveira exhaustive verification techniques (such as model checking and 21102227b9SDaniel Bristot de Oliveira theorem proving). RV works by analyzing the trace of the system's 22102227b9SDaniel Bristot de Oliveira actual execution, comparing it against a formal specification of 23102227b9SDaniel Bristot de Oliveira the system behavior. 2404acadcbSDaniel Bristot de Oliveira 2504acadcbSDaniel Bristot de Oliveiraconfig RV_REACTORS 2604acadcbSDaniel Bristot de Oliveira bool "Runtime verification reactors" 2704acadcbSDaniel Bristot de Oliveira default y 2804acadcbSDaniel Bristot de Oliveira depends on RV 2904acadcbSDaniel Bristot de Oliveira help 3004acadcbSDaniel Bristot de Oliveira Enables the online runtime verification reactors. A runtime 3104acadcbSDaniel Bristot de Oliveira monitor can cause a reaction to the detection of an exception 3204acadcbSDaniel Bristot de Oliveira on the model's execution. By default, the monitors have 3304acadcbSDaniel Bristot de Oliveira tracing reactions, printing the monitor output via tracepoints, 3404acadcbSDaniel Bristot de Oliveira but other reactions can be added (on-demand) via this interface. 35