Runtime Verification with Particle Filtering - Runtime Verification - page 155

Fig. 2. DBN D composed from the HMM H and the monitor DFA M , when observation o t is
missing due to a gap, and peek event q t provides information about possible states of the DFA at
time t
Fig. 3. DFA used to detect violations of a locking discipline
4.2 Running Example
Consider a monitor for a locking discipline for a structure type S in a program. The
structure type S contains a lock field (i.e., a field that refers to a lock), protected fields,
and unprotected fields. There is a monitor instance for each combination of a thread and
a structure of type S . The monitor checks that, when the thread accesses a protected
field of the instance of S , the thread holds the lock associated with the instance. The
DFA is shown in Figure 3; the parameterization by a thread and a structure is implicit.
Fig. 4. Graphical representation of the transition and observation probability distributions of an
HMM model of a system that usually follows the locking discipline