MoVES - A tool for Modelling and Verification of Embedded Systems |
| | Abstract | Embedded computer systems are making their way into more and more devices, from household appliances to mobile phones, PDAs and cars. Many of these systems have a limited amount of resources such memory and power, and must perform in a timely manner imposed by their application domain.
As it becomes harder to improve computer performance using sequential execution, the trend moves toward using Multi-processor System-on-Chip (MPSoC) designs, integrating multiple processing elements connected through an on-chip network. One or more applications are divided among these processing elements.
As these systems become more complex, the interaction between hardware and software becomes more unpredictable and problems such as memory overflow, data loss and missed deadlines are more likely to occur. System-level verification, of schedulability and resource usage, has therefore become one of the most relevant fields of study in designing real-time systems.
This thesis proposes a model of MPSoCs, where the interaction of all subcomponents of the MPSoC is captured in an exact formal way. This allows for formal verification using model-checking of properties such as schedulability and resource usage. The model is implemented using timed-automata in UPPAAL [3].
A tool is built, on top of the timed-automata model, which allows designers of embedded systems to analyze MPSoC systems early in the design phase.
The timed-automata model has been evaluated using a number of synthetic applications in order to demonstrate correct behavior. It has also been shown that the tool is able to handle real-life applications from a smart phone, with more than 100 tasks. | | Type | Master's thesis [Academic thesis] | | Year | 2007 | | Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU | | Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby | | Series | IMM-Thesis-2007-43 | | Note | Supervised by Associate Professor Michael R. Hansen and Professor Jan Madsen, IMM, DTU. | | Electronic version(s) | [pdf] | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|