Modelling and Verification of MPSoC | Aske Brekling
| | 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. | | Keywords | Timed automata, UPPAAL, Multiprocessor System-on-Chip (MP-SoC), ARTS, Verification | | Type | Master's thesis [Academic thesis] | | Year | 2006 | | Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU | | Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby | | Series | IMM-Thesis-2006-99 | | Note | Supervised by Associate Professor Michael R. Hansen and Professor Jan Madsen, IMM. | | Electronic version(s) | [pdf] | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|