| Abstract: |
In many of today`s technical appliances, embedded systems are deployed on an increasing scale. This trend is expected to massively gain in importance, especially for applications in consumer
and automotive electronics, telecommunications, medical engineering, and avionics. Embedded systems can be characterized as follows:
- They mostly consist of both hardware and software and perform control or communication tasks within an overall system, to which they are connected via networks, sensors, and actors.
- In general, they are heterogeneous, often distributed systems with real-time requirements which may work on both transformative and reactive domains.
- They typically are not directly visible to the user who interacts unconciously with them.
The design of embedded systems poses significant challenges since system complexity grows rapidly. In particular, very elaborate design methods are necessary, and quality requirements are high
because embedded systems often realize safety-critical functions. Hence the use of design automation tools has become indispensable. These can - based on a formal representation - analyze system
properties and prove the correctness of the design. Then the implementation can be synthesized by automatically generating hardware and software descriptions. This enables a more flexible,
faster, and less expensive design process than without automation.
Within this context, the following topics are subject of this monograph:
- A formal representation model called FunState is introduced which is especially suited to support embedded systems design. FunState serves as an internal design representation
and can be used for modeling mixed hardware/software systems for analysis and synthesis purposes.
- Based on FunState, a formal verification approach is presented which makes it possible to automatically check whether desired system properties are satisfied. In contrast to
conventional verification techniques, formal verification can prove the correctness of a system`s model mathematically.
- In order to generate an implementation, the execution order of functional parts within the system has to be determined, often in compliance with additional constraints. A novel,
FunState-based approach to this so-called scheduling is explained.
For the above-mentioned applications, mainly symbolic methods based on interval diagram techniques are suggested in this work. These new techniques can be used for enhancing the
efficiency of existing approaches. One of the main challenges facing design methods is to cope with extraordinarily large state spaces of the system which have to be traversed. During the last
years, symbolic methods have attracted great attention in this regard. By means of implicit enumeration, they can achieve significant savings in terms of the computational resources required
during the design process. |
