Game-Based Monitors for Scenario-Based Specification

Run-time verification techniques based on monitors have become the basic means of detecting software failures in dynamic and open environments. One challenging problem is how the monitor can provide sufficient indications before the real failures, so that the system has enough time to act before the failures cause serious harm. To this end, this paper proposes the main idea on how to generate monitors from a scenario-based specification called property sequence chart based on game theory. The monitors are interpreted in multivalued semantics: satisfied, infinitely controllable, system finitely controllable, system urgently controllable, environment finitely controllable, environment urgently controllable, violated. Through the multi-valued semantics definition, the monitors can provide enough information to help the system to take measures for failure prevention or recovery.