Modelling and Analyses of Embedded Systems Design

Aske Wiid Brekling

    Research output: Book/ReportPh.D. thesisResearch

    721 Downloads (Pure)

    Abstract

    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.
    Original languageEnglish
    Place of PublicationKgs. Lyngby, Denmark
    PublisherTechnical University of Denmark
    Publication statusPublished - 2010
    SeriesIMM-PHD-2011-236

    Projects

    Models and Analyses for Embedded Systems Design

    Brekling, A. W., Hansen, M. R., Madsen, J., Sparsø, J., Ravn, A. P. & Vain, J.

    Forskningsrådsfinansiering

    01/04/200702/02/2011

    Project: PhD

    Cite this

    Brekling, A. W. (2010). Modelling and Analyses of Embedded Systems Design. Technical University of Denmark. IMM-PHD-2011-236