Formal methods for design and simulation of embedded systems

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.