Scenario-based verification of real-time systems using UPPAAL

Abstract This paper 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 problem of scenario-based verification reduces to a computation tree logic (CTL) real-time model checking problem. In case 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 realtime model checker UPPAAL to accomplish these tasks. The proposed two approaches have been implemented in the UPPAAL tool and built as a tool chain, respectively.

We try out the prototype verification tools on a number of examples and case studies. Experimental results indicate that these methods are viable, computationally feasible,and the tools are effective.