The increasing success in miniaturization enables the design of more and more complex hardware and software systems on the one hand, and broadens the fields of application for these systems on the other hand. Nowadays, information processing systems can be found not only in the context of classical mainframes and personal computers, but they increasingly arise in Embedded Systems, which perform complex control and data processing tasks (embedded into surrounding technical systems). In many fields of everyday life we find typical applications of such Embedded Systems, for instance in automotive applications, aviation, telecommunications, controlling of manufacturing processes or instrumented homes.

Two focal points of our research result from the situation described above:

The increasing complexity of today‘s hardware and software systems renders it impossible to design these systems by hand. Computer assistance for the design is indispensable. For this reason we are investigating automated design methods for hard- and software systems .

In addition, it becomes more and more difficult to guarantee the correctness of highly complex designs. However, since these designs are used in safety-critical areas, tradeoffs concerning dependability are not acceptable. It becomes more and more important to consider dependability issues in early phases of system engineering and to spend enough effort in verifying the correctness of designs. Hence our second focus lies on formal methods for verification of hard- and software systems .

• Formal verification by equivalence checking and model checking: 
  We are developing formal methods to prove the correctness of information processing systems. Formal verification in general guarantees the equivalence of specifications (in abstract form) and their corresponding implementations (in more concrete form).
  
  
  We develop specialized model checking methods for specifications consisting in a set of temporal properties of the system. In this context the challenges lie both in efficient representations of the sets of all possible states of large systems and in coping with partial information. Partial information occurs in implementations which are not completely finished or which contain components designed by third-party providers, so that certain implementation details are not disclosed. Our focus lies on the development of efficient data structures and algorithms, especially in the development of methods which use approximations for reasons of efficiency, but which are able to provide definite answers all the same.
  
  
  

   

• Error diagnosis:
  We investigate localization of errors in erroneous designs in order to assist the designer during error correction.
  
  

   

• VLSI design, especially FPGA synthesis:
  In VLSI design we develop algorithms for an automated mapping of behavioral specifications to FPGAs. FPGAs (Field Programmable Gate Arrays) are reconfigurable computing devices with flexible applications due to the fact that they obtain their final functionality not until they are configured by the user. Moreover, they can be dynamically reconfigured at run time.
     

   

• Real-time operating systems:
  In the context of the new graduate school „Embedded Microsystems“ we investigate the automated generation of real-time operating systems which are able to satisfy hard restrictions concerning memory, run times and power consumption.