Chapter 8. Runtime verification of the real-time kernel Runtime verification is a lightweight and rigorous method to check the behavioral equivalence between system events and their formal specifications. Runtime verification has monitors integrated in the kernel that attach to tracepoints . If a system state deviates from defined specifications, the runtime verification program activates reactors to inform or enable a reaction, such as capturing the event in log files or a system shutdown to prevent failure propagation in an extreme case. 8.1. Runtime monitors and reactors The runtime verification (RV) monitors are encapsulated inside the RV monitor abstraction and coordinate between the defined specifications and the kernel trace to capture runtime events in trace files. The RV monitor includes: Reference Model is a reference model of the system. Monitor Instance(s) is a set of instance for a monitor, such as a per-CPU monitor or a per-task monitor. Helper functions that connect the monitor to the system. In addition to verifying and monitoring a system at runtime, you can enable a response to an unexpected system event. The forms of reaction can vary from capturing an event in the trace file to initiating an extreme reaction, such as a shut-down to avoid a system failure on safety critical systems. Reactors are reaction methods available for RV monitors to define reactions to system events as required. By default, monitors provide a trace output of the actions. 8.2. Online runtime monitors Runtime verification (RV) monitors are classified into following types: Online monitors capture events in the trace while the system is running. Online monitors are synchronous if the event processing is attached to the system execution. This will block the system during the event monitoring. Online monitors are asynchronous, if the execution is detached from the system and is run on a different machine. This however requires saved execution log files. Offline monitors process traces that are generated after the events have occurred. Offline runtime verification capture information by reading the saved trace log files generally from a permanent storage. Offline monitors can work only if you have the events saved in a file. 8.3. The user interface The user interface is located at /sys/kernel/tracing/rv and resembles the tracing interface. The user interface includes the mentioned files and folders. Settings Description Example commands available_monitors Displays the available monitors one per line. # cat available_monitors available_reactors Display the available reactors one per line. # cat available_reactors enabled_monitors Displays enabled monitors one per line. You can enable more than one monitor at the same time. Writing a monitor name with a '!' prefix disables the monitor and truncating the file disables all enabled monitors. # cat enabled_monitors # echo wip > enabled_monitors # echo '!wip'>> enabled_monitors monitors/ The monitors/ directory resembles the events directory on the tracefs file system with each monitor having its own directory inside monitors/ . # cd monitors/wip/ monitors/MONITOR/reactors Lists available reactors with the select reaction for a specific MONITOR inside "[]". The default is the no operation ( nop ) reactor. Writing the name of a reactor integrates it to a specific MONITOR. # cat monitors/wip/reactors monitoring_on Initiates the tracing_on and the tracing_off switcher in the trace interface. Writing 0 stops the monitoring and 1 continues the monitoring. The switcher does not disable enabled monitors but stops the per-entity monitors from monitoring the events. reacting_on Enables reactors. Writing 0 disables reactions and 1 enables reactions. monitors/MONITOR/desc Displays the Monitor description monitors/MONITOR/enable Displays the current status of the Monitor. Writing 0 disables the Monitor and 1 enables the Monitor.

Commands: