Verifying real-time systems against scenario-based requirements

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

Research output: Contribution to journalConference article in JournalResearchpeer-review

4 Citations (Scopus)
447 Downloads (Pure)

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 languageEnglish
Book seriesLecture Notes in Computer Science
Volume5850
Pages (from-to)676-691
Number of pages15
ISSN0302-9743
DOIs
Publication statusPublished - 2009
Event16th International Symposium on Formal Methods (FM'09) - Eindhoven, Netherlands
Duration: 19 May 2010 → …
Conference number: 16

Conference

Conference16th International Symposium on Formal Methods (FM'09)
Number16
CountryNetherlands
CityEindhoven
Period19/05/2010 → …

    Fingerprint

Cite this