Systematic modelling of embedded systems: Managing non-formal aspects

Numerous (tool-supported) mathematical languages, formalisms and methods exist to create models and verify their properties. As their name suggests, formal methods for verifying and designing the systems focus on the formal, mathematical world. However, the steps to construct a model and to justify that it represents the system correctly with respect to its purpose are not entirely formal. Currently, a limited number of methods exist to guide through some of these non-formal steps. It is left to the modeller's experience and talent to learn how to construct and validate the model (justify that it correctly represents the system).
In this thesis, we argue that not all modelling steps, decisions and actions have to be unstructured and "out of the blue?. Steps, such as abstraction, can be explicitly named and placed in the modelling process. To date, these steps have been recognised, but not all of them have been gathered to form a modelling methodology that can help the modeller when designing the model.
The work presented in this thesis aims to improve embedded systems modelling by designing a method that complements the existing modelling languages and tools. The method focuses on non-formal, non-mathematical design aspects of software modelling techniques. We focus on modelling the software environment of high-tech, software- controlled systems consisting of mechanical and electronic components. Furthermore, we look at automata and state-based techniques.
We present a method that outlines modelling steps for constructing a model and justifying the model's adequacy. For constructing the model, our method provides the following components:
* A process to follow to design an adequate model and verify the requirements; at the same time this process can be used to explain how the model has been constructed, when performing model justification.
* Top-level reference conceptual models to frame the model construction and justification process. These conceptual models emphasise the gap between formal domain in which we can obtain formal proofs about model properties; and the informal world that we represent with the model.
* Structures including the following
- The taxonomy of modelling decisions
- Classifications of modelling assumptions
* A structure of the argument for justifying the model

The method can be used with other formal methodologies for modelling, as it aims is to complement them. Furthermore, the structures we provide aim to increase the knowledge of what the non-formal steps are when constructing and
justifying the model.