Model-based Runtime Verification Framework

Model-based runtime verification is an extension to the state-of-the-art runtime verification, aimed at checking at runtime the system implementation against the system model (consistency checking) and the system model against the system specification (safety checking). Notice that our runtime verification works at the model level, thus, we do not need to strictly synchronize this runtime verification with the system execution. In fact, we mainly use the runtime information (current states) obtained from the system execution to reduce the state space (of the system model) to be explored. It means that this model-based runtime verification might run before or after the system execution, i.e., switch alternately between a preventive pre-checking mode and a maintaining post-checking mode. In order to make it run ahead of the system execution for as long time as possible, we present two possible strategies so that this runtime verification can selectively reduce the state space (of the system model) to be explored by making the system model enriched with probabilities and additional information derived and learned at the system testing phase.