Skip to main content

TS

Automatically transforming and relating uppaal models of embedded systems

Authors

Timothy Bourke and Arcot Sowmya

NICTA

UNSW

Abstract

Relations between models are important for effective automatic validation, for comparing implementations with specifications, and for increased understanding of embedded systems designs. Timed automata may be used to model a system at multiple levels of abstraction, and timed trace inclusion is one way to relate the models.

It is known that a deterministic and tau-free timed automaton can be transformed such that reachability analysis can decide timed trace inclusion with another timed automaton. Performing the transformation manually is tedious and error-prone. We have developed a tool that does it automatically for a large subset of Uppaal models.

Certain features of the Uppaal modeling language, namely selection bindings and channel arrays, complicate the transformation. We formalize these features and extend the validation technique to incorporate them. We find it impracticable to manipulate some forms of channel array subscripts, and some combinations of selection bindings and universal quantifiers; doing so either requires premature parameter instantiation or produces models that Uppaal rejects.

BibTeX Entry

  @inproceedings{Bourke_Sowmya_08,
    publisher        = {ACM},
    author           = {Bourke, Timothy and Sowmya, Arcot},
    month            = oct,
    editor           = {{Chairs: Luca de Alfaro, Jens Palsberg}},
    year             = {2008},
    keywords         = {timed trace inclusion, uppaal, model transformation},
    title            = {Automatically transforming and relating Uppaal models of embedded systems},
    booktitle        = {Proceedings of the 8th International Conference on Embedded Software},
    pages            = {59--68},
    address          = {Atlanta, Georgia, USA}
  }

Download

Served by Apache on Linux on seL4.