Formal methods for design and simulation of embedded systems

Mikkel Koefoed Jakobsen

Research output: Book/ReportPh.D. thesisResearch

778 Downloads (Pure)

Abstract

Cyper physical systems (CPSs) are present in many variants in our daily life. The complexity of developing a CPS is quickly increasing and the interaction between different CPSs is increasingly important. The interaction of the systems is becomming more and more fluent and seamless.

This thesis presents the development of a formal systems modelling (ForSyDe) framework for modelling CPSs. The formalism of the framework makes computer aided design (CAD) a possibility for developing CPSs. The framework consists of four models of computation (MoCs): synchronous (SY), synchronous data flow (SDF), discrete event (DE), and continuous time (CT).

Usage of the framework is demonstrated with two use cases. A company use case featuring a hearing aid calibration device and the distributed energy harvesting aware routing (DEHAR) algorithm for wireless sensor networks (WSNs). These two use cases illustrate different design challenges. With the ForSyDe framework, the use cases are expressed as homogeneous and heterogeneous models.

The company use case illustrates that the ForSyDe framework handles systems with well defined interactions very well. The WSN use case illustrates that networked systems with complex interaction are more challenging to express naturally, yet the ForSyDe framework is able to express such systems.
Original languageEnglish
Place of PublicationKgs. Lyngby
PublisherTechnical University of Denmark
Number of pages190
Publication statusPublished - 2013
SeriesPHD-2013
Number289
ISSN0909-3192

Projects

Formal methods for design and simulation of embedded systems

Jakobsen, M. K., Madsen, J., Hansen, M. R., Dragoni, N., Plosila, J. P. & Vain, J.

1/3 FUU, 1/3 inst 1/3 Andet

01/06/200930/08/2013

Project: PhD

Cite this

Jakobsen, M. K. (2013). Formal methods for design and simulation of embedded systems. Technical University of Denmark. PHD-2013, No. 289