@ARTICLE\{IMM2007-05060,
    author       = "A. Brekling and M. R. Hansen and J. Madsen",
    title        = "A Timed-Automata Model of Multiprocessor System-on-Chips",
    year         = "2007",
    journal      = "",
    volume       = "",
    editor       = "",
    number       = "",
    publisher    = "",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5060-full.html",
    abstract     = "In this article we develop a timed-automata model of Multiprocessor System-on-
Chips (MPSoC). The model describes MPSoC at system level in the sense that it
captures how a model of an application is mapped onto a model of an execution
platform. An application is given in terms of a parallel composition of tasks, where
a task should meet some timing constraints and there may be causal dependencies
among tasks. An execution platform consists of a collection of processing elements,
where each processing element executes a number of tasks according to a given
scheduling strategy.
Analysis of MPSoC is a major challenge due to the freedom of interrelated choices
concerning the application level, the configuration of the execution platform and the
mapping of the application onto this platform.
Our timed-automata model captures fundamental concepts of the application and
major components of the execution platform as well as their interaction in a succinct
manner. The model is expressed in {UPPAAL,} thereby giving a tool supporting
simulation and verification of timing properties. So far this tool has been used
in connection with design space exploration of rather small (though non-trivial)
examples only."
}