Abstract
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.
Original language | English |
---|---|
Book series | Lecture Notes in Computer Science |
Volume | 5850 |
Pages (from-to) | 676-691 |
Number of pages | 15 |
ISSN | 0302-9743 |
DOIs | |
Publication status | Published - 2009 |
Event | 16th International Symposium on Formal Methods (FM'09) - Eindhoven, Netherlands Duration: 19 May 2010 → … Conference number: 16 |
Conference
Conference | 16th International Symposium on Formal Methods (FM'09) |
---|---|
Number | 16 |
Country/Territory | Netherlands |
City | Eindhoven |
Period | 19/05/2010 → … |