Beta 1


Title MoVES - A tool for Modelling and Verification of Embedded Systems
Author Nielsen, Jens Ellebæk
Knudsen, Kristian Staalø
Supervisor Hansen, Michael Reichhardt (Computer Science and Engineering, Informatics and Mathematical Modelling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Madsen, Jan (Computer Science and Engineering, Informatics and Mathematical Modelling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2007
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.
Series IMM-Thesis-2007-43
Fulltext
Original PDF imm5267.pdf (2.44 MB)
Admin Creation date: 2007-06-11    Update date: 2007-09-19    Source: dtu    ID: 200713    Original MXD