Scenario-based verification of real-time systems using Uppaal

This article proposes two approaches to tool-supported automatic verification of dense real-time systems against scenario-based requirements, where a system is modeled as a network of timed automata (TAs) or as a set of driving live sequence charts (LSCs), and a requirement is specified as a separate monitored LSC chart. We make timed extensions to a kernel subset of the LSC language and define a trace-based semantics. By translating a monitored LSC chart to a behavior-equivalent observer TA and then non-intrusively composing this observer with the original TA-modeled real-time system, the problems of scenario-based verification reduce to computation tree logic (CTL) real-time model checking problems. When the real-time system is modeled as a set of driving LSC charts, we translate these driving charts and the monitored chart into a behavior-equivalent network of TAs by using a "one-TA-per-instance line" approach, and then reduce the problems of scenario-based verification also to CTL real-time model checking problems. We show how we exploit the expressivity of the TA formalism and the CTL query language of the real-time model checker Uppaal to accomplish these tasks. The proposed two approaches are implemented in the Uppaal tool and built as a tool chain, respectively. We carry out a number of experiments with both verification approaches, and the results indicate that these methods are viable, computationally feasible, and the tools are effective.