trace/rv/runtime-verification.rst

26 A monitor is the central part of the runtime verification of a system. The
27 monitor stands in between the formal specification of the desired (or
31 *RV monitor* abstraction. A *RV monitor* includes a reference model of the
32 system, a set of instances of the monitor (per-cpu monitor, per-task monitor,
33 and so on), and the helper functions that glue the monitor to the system via
36  Linux   +---- RV Monitor ----------------------------------+ Formal
39   |   Linux kernel    |     |     Monitor    |     |     Reference   |
54 In addition to the verification and monitoring of the system, a monitor can
81 monitor process the traces generated by a system after the events, generally by
86 an *asynchronous* monitor has its execution detached from the system. Each type
87 of monitor has a set of advantages. For example, *offline* monitors can be
94 monitor's ability to process them in the same system, only the *offline*
96 on higher overhead than the simple handling of an event by a monitor, then a
150 - Writing to it enables a given monitor
151 - Writing a monitor name with a '!' prefix disables it
169 Note that it is possible to enable more than one monitor concurrently.
191 Each monitor will have its own directory inside "monitors/". There the
192 monitor-specific files will be presented. The "monitors/" directory resembles
201    wakeup in preemptive per-cpu testing monitor.
205 **monitors/MONITOR/desc**
207 - Reading shows a description of the monitor *MONITOR*
209 **monitors/MONITOR/enable**
211 - Writing "0" disables the *MONITOR*
212 - Writing "1" enables the *MONITOR*
213 - Reading return the current status of the *MONITOR*
215 **monitors/MONITOR/reactors**
217 - List available reactors, with the select reaction for the given *MONITOR*
219 - Writing the name of a reactor enables it to the given MONITOR.