Chapter 6. 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.
6.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.
6.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.
6.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 |
|---|---|---|
|
| Displays the available monitors one per line. |
|
|
| Display the available reactors one per line. |
|
|
| 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. |
|
|
|
The |
|
|
|
Lists available reactors with the select reaction for a specific MONITOR inside "[]". The default is the no operation ( Writing the name of a reactor integrates it to a specific MONITOR. |
|
|
|
Initiates the
Writing | |
|
|
Enables reactors. Writing | |
|
| Displays the Monitor description | |
|
|
Displays the current status of the Monitor. Writing |
