This text presents, in roughly anti-chronological order, the main lines of research which I have pursued over the years. Though I am currently not active in the oldest two or three, I still notice their concepts influencing my present work from time to time.

Design of Dependable Systems

Present-day design languages like the UML and ordinary realisations of formal-method support for system development do not match the juridical requirements in safety-critical application domains like rail or aviation. I work on the adapting methods integrating formal methods into standard-conformant development and tools and integrate them into standard conformant design processes.

Test Technologies

A particular focus of my work are test technologies. If models are used in the design process, tests can be derived systematically or even partly automatic.

Applications in the Rail Domain

Currently, my research is driven by striving to apply such techniques to the development of rail system, including the issue of certification.

The Potential of Formal Methods

One main question I consider is to which extent formal methods and techniques can be profitably used. I believe that their role will continue to grow, and it will be a challenge to develop their potential to the full extent. They will not, at least for a long time, replace all other techniques and approaches. But there might be a day when the outcome of each design activity is comprehensively formally verified.

Security

My interest in security concerns mainly the security analysis of protocols and systematic methods for quantitative threat and risk analysis.

Model Checking

Model checking is a name used for procedures based on automata theory by which properties of systems can be checked automatically. I have worked on basic algorithms, mainly for infinite systems, methods integrating model checking with other techniques, and the realisation of model-checking support for commercial design tools.

Infinite Systems

Though model checking has been originally designed to analyse finite-state systems, there are ways to generalize the approach to different kinds of infinite-state systems. One case are systems whose state set is generated in a recursive manner like the graphs generated by a context-free graph grammar. Even higher-order generated systems can be model checked as shown in my habilitation thesis.

Another form of infinite systems are finite-state controllers operating on an infinite data domain. Model checking can be performed e.g. by working on the finite-state control while manipulating the data part with logical means. This is an active line of research pursued within the AVACS project.

One example of integrating model checking with other techniques is the combination with logic tools mentioned in the previous paragraph. Other important approaches which I studied consist in integrations with decomposition and abstraction refinement.

Design Support

I have worked on integrating model-checking support into the Statemate and the Rhapsody system (both Telelogic), and preparing their integration for many other design tools like ASCET and Stateflow. One use case for model checking in these systems is the verification of temporal logic properties. Others are consistency or healthiness checks which are mapped to model checking problems.

Automata Learning and Test Generation

I have worked on the use of automata-learning techniques to derive models of systems from observations on their interfaces. These models can then be used to construct test cases for regression testing, when a new system version is to be checked for compatibility with the old. This work has been applied in the domain of telecommunication.

Hoare Logics: Complexity and Expressiveness

In my PhD thesis I analysed the inherent complexity of constructing proofs in a Hoare-style program logic for a language with higher-order procedures. The results permitted to derive bounds of the power of proof systems.

My master thesis and subsequent work concerned the question of the adequateness of predicate logic for expressing the semantics of programs. Main results where characterisations of first-order structures where the logics are expressive wrt. certain classes of programs.