Runtime monitoring and verification of systems with hidden information

This paper describes a technique for runtime monitoring (RM) and runtime verification (RV) of systems with invisible events and data artifacts. Our approach combines well-known hidden markov model (HMM) techniques for learning and subsequent identification of hidden artifacts, with runtime monitoring of probabilistic formal specifications. The proposed approach entails a process in which the end-user first develops and validates deterministic formal specification assertions, s/he then identifies hidden artifacts in those assertions. Those artifacts induce the state set of the identifying HMM. HMM parameters are learned using standard frequency analysis techniques. In the verification or monitoring phase, the system emits visible events and data symbols, used by the HMM to deduce invisible events and data symbols, and sequences thereof; both types of symbols are then used by a probabilistic formal specification assertion to monitor or verify the system.