Klaus Dräger

Klaus Dräger (Ph.D. Student) Reactive Systems Group Universität des Saarlandes Phone: +49 681 302 5613 Fax: +49 681 302 5636 eMail: draeger at cs.uni-sb.de Building: E 1.3 Room: 508

About me

I am a member of the Reactive Systems Group at Saarland University. My research interests are model checking and verification of complex real-time systems.

Research

Verification of complex concurrent real-time systems is a challenging topic. In order to prove that a given system satisfies a desired property, one needs to deal with an infinite state space (due to the real-time aspect and infinite data domains) as well as a complex control structure (due to the parallelism between the system components.)

Abstraction refinement is a highly effective method for dealing with infinite state spaces. In this approach, a finite-state abstraction of the system is constructed in such a way that if the abstraction is correct, then so is the system. If the abstraction exhibits an error, then either this error also exists in the concrete system, or it can be removed by a suitable refinement of the abstraction. In our paper Slicing Abstractions, we introduced a new model-based refinement loop that incorporates local refinements and slicing operations in order to obtain much smaller and more focused abstractions.

Since the complex control structure of highly concurrent systems makes reasoning about such systems hard, there is a lot of interest in compositional methods, by which one can derive properties of individual components which can be used to reason about the system as a whole. We recently introduced subsequence invariants, a class of invariants of the possible sequences of synchronization events in a system, which can be efficiently computed for each process and yet hold for the entire system.

Publications

Some possible student projects

Integrating Partial Order Reduction with Abstraction Refinement:

Partial order reduction and abstraction refinement are two fundamentally different approaches for tackling the complexity inherent in concurrent systems. In this project, ways of integrating both methods will be investigated.

The essential idea of partial order reduction is exploiting the fact that, in particular in concurrent systems, many pairs of transitions are independent of each other, so that the order in which they are taken makes no difference. When exploring the state space, one can then reduce the set of transitions one considers in each state.

In the abstraction refinement approach, a system is reduced to a much simpler abstraction which is examined for the desired property. If this check fails, additional information can be derived from the failure and used to refine the abstraction, and the process is repeated.

Your goals for this thesis are to:

• make yourself familiar with the approaches described above and with our abstraction refinement tool SLAB,
• investigate ways of using partial order reduction techniques in order to slow the growth of the abstraction during the refinement process, and
• implement them in Java as an extension of SLAB.

A modular interpolating theorem prover

In abstraction refinement, one of the central questions is how to come up with new predicates with which states can be distinguished. One very nice technique for this, used in our SLAB tool, is the computation of Craig interpolants. These are formulae that represent the essence of how, at some state s, a path from an initial state si to s and a path from s to an error state se fail to be consistent.

Our abstraction refinement tool SLAB uses Andrey Rybalchenko’s clp prover for checking satisfiability and finding interpolants, which is limited to linear arithmetic and uninterpreted function symbols. We would like to be able to handle other theories, for example lists. In order to do so, we need decision procedures that can not only decide whether a set of formulae involving lists is true, but can also compute Craig interpolants.

In order to achieve this, we would like very much to complement clp with another interpolating theorem prover. This would be split into subtopics that can be distributed among several theses, for example implementation of

• a base program able to deal with formulae from combinations of theories
• a module for the theory of linear inequalities
• a module for the theory of uninterpreted function symbols with equality
• a module for the theory of single-linked lists
• etc.

Linear Duration Invariants

The most basic formal model to deal with real-time systems are timed automata, which are just finite automata augmented with clocks to keep track of the passing of time. A more powerful version of timed automata, stopwatch automata, is obtained by allowing the automaton to temporarily halt some of the clocks. These automata are of interest if one is interested in measuring the amount of time that some property holds. Unfortunately, unlike for timed automata, reachability is undecidable for stopwatch automata.

Linear duration invariants are a decidable subset of stopwatch properties, modeling aspects like “During any time interval of at least 1 second, process P has access to resource R for at least 20% of the time”.

The aim of this thesis is adding the capability to deal with these constraints to our abstraction refinement tool SLAB. Your goals would therefore be to:

• learn about the predicate abstraction approach as implemented in SLAB,
• familiarize yourself with linear duration invariants,
• figure out how to represent them in SLAB, and
• implement your solution in Java.