Research Projects - Specification and Verification of Concurrent Systems

Specification and Verification of Concurrent Systems

M. C. Escher: Encounter Cooperations Financial Support,

Master's Theses, Term Projects

Publications

Tools

Current Members: Former Members: Links
The research in the scope of the project "Specification and Verification of Concurrent Systems" currently focuses on Petri nets, unfolding techniques, non-interleaving semantics and graph transformation systems. Our group has a long tradition of research in this area. For more information visit the pages of our former projects.

In concurrency theory there is a large variety of models. Our main interest lies on Petri nets, process calculi such as CCS and the pi-calculus, and graph transformation systems.

Verification and analysis of concurrent systems is especially challenging since it means taking into account interferences and conflicts between the subcomponents of a system. Even for finite-state systems concurrency typically leads to a huge state space, even for small system descriptions, a phenomenon called state space explosion. One solution is to employ unfolding techniques in order to minimize the growth of the state space.

Further problems arise in the verification of infinite-state systems, although automated techniques exist for restricted classes of models. One possible solution would be to resort to non-complete but automatic analysis techniques, which are allowed to answer "don't know" in some cases. Below the descriptions of some specific research projects are listed.

Multi-agent systems (Astrid Kiehn)

Giving autonomy to the components of a concurrent system one obtains so-called multiagent systems. The components (now called agents) are autonomous in their decisions and actions and may have learning facilities. There is an increasing interest in multiagent systems as the internet supplies the infrastructure and many applications for a respective software technology. As it is open and under permanent change, the agents must be able to cope with partial, uncertain knowledge and, based on this, adapt their behaviour.

Due to its pragmatic reasoning the belief-desire-intention (BDI) model has turned out to be a useful abstraction tool for describing, explaining and predicting the behaviour of agents. We consider mathematical formalism for specifying and verifying BDI-based systems.

Graph transformation systems (Barbara König)

Graph rewriting can be seen as a general framework in which to specify and reason about concurrent and distributed systems. The topology and connection structure of these systems can often be naturally represented in terms of nodes and connecting edges, and their dynamic evolution can be expressed by graph rewriting rules. There are several graph transformation approaches, among them the well-known double-pushout approach introduced by Ehrig.

We are especially interested in the verification and static analysis of graph transformation systems. In this context we developed a theory of bisimulation for graph transformation systems and introduced analysis techniques, based on type systems and unfoldings respectively.


Cooperations

Financial Support


Master's Theses, Term Projects

Have a look at the topics which are currently offered. If you are interested in another topic please contact us directly.

Publications

[Postscript] [PDF]

Tools


Links to Related Sites

Formal Models of Concurrency:

Tools:

Formal Verification in Industry (examples):

Mailing Lists:


Last modified: Tue Aug 27 09:48:21 MET DST 2002