Skip to main content


Tool support for verifying trace inclusion with uppaal


Timothy Bourke and Arcot Sowmya




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

    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}


Served by Apache on Linux on seL4.