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.
| Originalsprog | Engelsk |
|---|---|
| Bogserie | Lecture Notes in Computer Science |
| Vol/bind | 5850 |
| Sider (fra-til) | 676-691 |
| Antal sider | 15 |
| ISSN | 0302-9743 |
| DOI | |
| Status | Udgivet - 2009 |
| Begivenhed | 16th International Symposium on Formal Methods (FM'09) - Eindhoven, Holland Varighed: 19 maj 2010 → … Konferencens nummer: 16 |
Konference
| Konference | 16th International Symposium on Formal Methods (FM'09) |
|---|---|
| Nummer | 16 |
| Land/Område | Holland |
| By | Eindhoven |
| Periode | 19/05/2010 → … |
Bibliografisk note
Titel:Proceeding of Second World Congress on Formal Methods (FM 2009)
Oversat titel:
Oversat undertitel:
Forlag:
Springer
ISBN (Trykt):
3-642-05088-3
ISBN (Elektronisk):
978-3-642-05088-6
Publikationsserier:
Lecture Notes in Computer Science, Springer, 5850
Redaktører:
Ana Cavalcanti
Dennis Dams