Beta 1


Title Modelling and Verification of MPSoC
Author Brekling, Aske Wiid (Computer Science and Engineering, Informatics and Mathematical Modelling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
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 2006
Abstract This thesis presents a formal model based on the system-level MPSoC simulation framework ARTS [10, 11]. This model formalizes all notions regarding timing and synchronization in such a manner that some properties of systems can be verified. The full semantics for the model is provided together with examples of how systems are specified in this semantics. In developingMultiprocessor System-on-Chips (MPSoC), many interrelated choices have to be considered at the levels of the application, the operating system and the configuration of the platform. Choices regarding properties of systems have great consequences in unforseen areas of the system. This makes it a major challenge to develop correctly implemented MPSoC together with arguments for decisions leading to the solution. Decisions leading to the implementation of such systems are many, and most are non-trivial and complex. In the development phase it is not enough to simply look at the different layers of the systems independently, as a minor change at one layer can greatly influence other layers. Tools providing means for analysis at system level (i.e. taking all layers into account) are in high demand. Especially tools for verification of properties of the systems are desirable, as verification can provide guarantees that the given criteria for the system properties are met.
Series IMM-Thesis-2006-99
Keywords Timed automata; UPPAAL; Multiprocessor System-on-Chip (MP-SoC); ARTS; Verification
Fulltext
Original PDF imm4936.pdf (0.97 MB)
Admin Creation date: 2007-06-11    Update date: 2007-09-21    Source: dtu    ID: 200688    Original MXD