Modelling and Analyses of Embedded Systems Design

We present the MoVES languages: a language with which embedded systems can be specified at a stage in the development process where an application is identified and should be mapped to an execution platform (potentially multi- core). We give a formal model for MoVES that captures and gives semantics to the elements of specifications in the MoVES language. We show that even for seem- ingly simple systems, the complexity of verifying real-time constraints can be overwhelming - but we give an upper limit to the size of the search-space that needs examining. Furthermore, the formal model exposes important scheduling situations that become central in establishing timed-automata models that can be used for analysis of MoVES specifications effectively. Finally we present the MoVES tool, which can conduct automatic verification of interesting properties of MoVES specifications. In several examples, we use the MoVES tool to conduct analysis that identifies timing anomalies. We also conduct design space exploration in an example using the MoVES tool. And we show that it can be used for analysis of systems that, in size, resemble industrially-interesting systems. We find that semantically-based verification is a promising approach for assisting developers of embedded systems. We provide examples of system verifications that, in size and complexity, point in the direction of industrially-interesting systems.