Research
Real Time Scheduling
Real-time systems are systems that interact with their environment in such a way that for certain inputs the corresponding outputs have to occur within given time bounds. Many embedded systems, in particular those in safety critical applications, are of this type. The practical importance of this class of systems has led to a large body of research on the specification, verification and analysis of real-time systems. We develop distribution and scheduling techniques taking the constraints of distributed computer architectures into account, in particular the combination of caches and pipelines.
Verification of Hybrid Systems
Many embedded systems operate within or even comprise coupled networks of both discrete and continuous components. The behavior of such hybrid discrete-continuous systems cannot be fully understood without explicitly modeling the interaction of discrete and continuous dynamics. Tools for building such models and for simulating their dynamics are commercially available. Simulation is, however, inherently incomplete and has to be complemented by verification, which amounts to showing that the coupled dynamics of the embedded system and its environment is well-behaved, e.g. that it may never reach an undesirable state or that it will converge to a desirable state, regardless of the actual disturbance. Unfortunately, theories and tool support for verifying hybrid systems are not yet mature. Recent industrial trials, e.g. performed by Ford in the context of the Mobies initiative, indicate that current verification tools fall short with respect to both the dimensionality of the continuous state spaces and the size of the discrete state spaces they can handle. Breakthrough in both directions, thereby reconciling the seemingly contradictory demands placed by these dimensions with respect to fully symbolic representations facilitating symbolic model checking, is thus needed.
The Steiner Problem in Phylogeny
One subject in the field of phylogenetics is finding the most probable evolutionary tree to a given set of DNA-sequences. If one assumes that mutations can only occur by alteration of single nucleotides, and each of these alternations occures with the same probability, then the “most probably” evolutionary tree is the one with the fewest alternations. This tree is also called the “most parsimony” tree. Thus finding the SMT over the given DNA-Sequences with Hamming metric gives us the most probable evolutionary tree, which gives information about the relatedness of species.
