Model-Based Design of Embedded Systems
Our research topics generally address all issues related to model-based design methodologies for embedded systems. Embedded systems are application-specific computer systems that communicate directly with a surrounding system through sensors and actuators. Embedded systems are found in many telecommunication devices, consumer electronics, home appliances, industrial equipment, and are increasingly used in avionics and automotive applications.
The development of embedded systems is much more difficult than for traditional computer systems: First of all, due to safety-critical applications, the correctness of these systems plays a crucial role and software updates can not be easily made for embedded systems that are already in use. Second, embedded systems usually have to satisfy a couple of non-functional properties like reduced energy consumption, reliability and real-time behavior. For this reason, many embedded systems are based on heterogeneous multi-processors to reduce energy consumption while increasing performance at the same time. However, this raises the big problems
- to model a system consisting of parallel behaviors with a common model of time,
- to make sure that this concurrent system satisfies given functional specifications,
- and to correctly map this model to application-specific state-of-the-art computer architectures so that non-functional requirements are optimized.
A model-based design flow as the one proposed by our research starts with a model of the system that already consists of subsystems that describe concurrent behaviors. The original model must already be executable and should be architecture-independent, i.e., decisions about the later implementation in hardware or software are not yet made. By means of simulation, one can make sure that the system has the general desired functionality, at least with the simulated traces (use cases). Then, one may apply formal verification techniques to verify that given temporal and functional specifications are satisfied, e.g. by means for model-checking or interactive theorem proving. Once the correctness is guaranteed, the system is partitioned into hardware and software components and the desired processor architectures are selected. It may be the case that several components run as software on the same processor, and it may also be the case that these decisions are changed a runtime later on so that adaptable embedded systems were obtained. To make use of architecture-specific tools, one then has to translate the components to domain specific programming languages like C (for software synthesis) or Verilog (for hardware synthesis). It is also possible to generate application-specific processors that are integrated with other components. Thus, our design flow covers the following typical design tasks:
Many of our research results have already been integrated into our model-based design framework Averest, which is freely available.