Tool Support for Holistic Modelling of Distributed Embedded Systems in Creol

A holistic approach to modelling embedded systems is advocated: Many aspects of a system should be analysed in isolation to keep the task manageable, but they often influence each other during integration in a way that the desired system becomes unrealisable. A tool-supported approach that aims at integrated models of different concerns based on formal methods is suggested to solve this problem. This approach uses Creol, which is a language designed for object-oriented modelling of distributed systems. We report on ongoing work on the design and the implementation of tools that support modelling, validation, and verification. We focus on sensor networks, which are distributed system that consists of many embedded devices with tight constraints on computational power, energy availability, and timeliness. The described tools are a compiler that performs static checks and optimisations, an interpreter that defines a formal semantics, and a prototypical LTL model checker. This supports seamless development with formal methods.