Research
This text presents, in roughly antichronological 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
ModelBased Techniques
Presentday design languages like the UML and ordinary realisations
of formalmethod support for system development do not match the
juridical requirements in safetycritical application domains like
rail or aviation. I work on the adapting methods integrating formal methods into standardconformant 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 modelchecking support for commercial design tools.
Infinite Systems
Though model checking has been originally designed to analyse
finitestate systems, there are ways to generalize the approach to
different kinds of infinitestate systems. One case are systems whose
state set is generated in a recursive manner like the graphs generated
by a contextfree graph grammar. Even higherorder generated systems
can be model checked as shown in my habilitation thesis.
Another form of infinite systems are finitestate controllers
operating on an infinite data domain. Model checking can be performed
e.g. by working on the finitestate control while manipulating the
data part with logical means. This is an active line of research
pursued within the AVACS project.
Integrated Procedures
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 modelchecking 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 automatalearning 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 Hoarestyle program logic for a language with higherorder
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
firstorder structures where the logics are expressive wrt. certain
classes of programs.
