We propose an approach to automatic verification of real-time systems against scenario-based requirements. A real-time system is modeled as a network of Timed Automata (TA), and a scenario-based requirement is specified as a Live Sequence Chart (LSC). We define a trace-based semantics for a kernel subset of the LSC language. By equivalently translating an LSC chart into an observer TA and then non-intrusively composing this observer with the original system model, the problem of verifying a real-time system against a scenario-based requirement reduces to a classical real-time model checking problem. We show how this is accomplished in the context of the Uppaal model checker. © 2009 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Larsen, K. G., Li, S., Nielsen, B., & Pusinskas, S. (2009). Verifying real-time systems against scenario-based requirements. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5850 LNCS, pp. 676–691). https://doi.org/10.1007/978-3-642-05089-3_43
Mendeley helps you to discover research relevant for your work.