Verifying real-time systems against scenario-based requirements

Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, Saulius Pusinskas

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

4 Citationer (Scopus)
473 Downloads (Pure)

Abstrakt

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.
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind5850
Sider (fra-til)676-691
Antal sider15
ISSN0302-9743
DOI
StatusUdgivet - 2009
Begivenhed16th International Symposium on Formal Methods (FM'09) - Eindhoven, Holland
Varighed: 19 maj 2010 → …
Konferencens nummer: 16

Konference

Konference16th International Symposium on Formal Methods (FM'09)
Nummer16
LandHolland
ByEindhoven
Periode19/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

Fingeraftryk Dyk ned i forskningsemnerne om 'Verifying real-time systems against scenario-based requirements'. Sammen danner de et unikt fingeraftryk.

Citationsformater