1*102227b9SDaniel Bristot de Oliveira# SPDX-License-Identifier: GPL-2.0-only 2*102227b9SDaniel Bristot de Oliveira# 3*102227b9SDaniel Bristot de Oliveiramenuconfig RV 4*102227b9SDaniel Bristot de Oliveira bool "Runtime Verification" 5*102227b9SDaniel Bristot de Oliveira depends on TRACING 6*102227b9SDaniel Bristot de Oliveira help 7*102227b9SDaniel Bristot de Oliveira Enable the kernel runtime verification infrastructure. RV is a 8*102227b9SDaniel Bristot de Oliveira lightweight (yet rigorous) method that complements classical 9*102227b9SDaniel Bristot de Oliveira exhaustive verification techniques (such as model checking and 10*102227b9SDaniel Bristot de Oliveira theorem proving). RV works by analyzing the trace of the system's 11*102227b9SDaniel Bristot de Oliveira actual execution, comparing it against a formal specification of 12*102227b9SDaniel Bristot de Oliveira the system behavior. 13