Skip to main content

TS

Tool support for verifying trace inclusion with uppaal

Authors

Timothy Bourke and Arcot Sowmya

NICTA

UNSW

Abstract

Trace inclusion against a deterministic Timed Automata can be verified with the Uppaal model checking tool by constructing a test automaton that traps illegal synchronisation possibilities. Constructing the automaton manually is tedious and error prone. This paper presents a tool that does it automatically for a subset of Uppaal models.

Certain features of Uppaal, namely selection bindings and channel arrays, complicate the construction. We first formalise these features, and then show how to incorporate them directly in the testing construction. To do so we limit the forms of subscript that can be used to specify synchronisations; striving for a balance between practicability and program complexity. Unfortunately, some combinations of selection bindings and universal quantifiers cannot be effectively manipulated. The tool does not yet validate the determinism requirements, nor handle committed states or broadcast channels.

BibTeX Entry

  @techreport{Bourke_Sowmya_07:tr,
    author           = {Bourke, Timothy and Sowmya, Arcot},
    number           = {UNSW-CSE-TR-0723},
    month            = dec,
    year             = {2007},
    keywords         = {timed automata, trace inclusion, uppaal},
    title            = {Tool support for verifying trace inclusion with Uppaal},
    institution      = {Uni. of NSW, Computer Science and Engineering},
    address          = {Sydney}
  }

Download

Served by Apache on Linux on seL4.