"Higher Order or Mobility" is a property of concurrent processes which
can send or receive port addresses or entire processes and which are able
to dynamically restructure their communication structure during runtime.
It offers new means for the specification of concurrent systems, but also
introduces challenges concerning the description and verification of mobile
and higher-order processes. One prominent mobile calculus is the pi-calculus.
We began research in this area in 1996 and we are mainly interested
in the following topics:
Semantics for (imperative) higher order languages (Christine
Röckl): this line of research involved giving a pi-calculus semantics
to CIA (Concurrent Idealized Algol) . This semantics can be used to obtain
verification results for CIA by employing bisimulation techniques introduced
for the pi-calculus.
A graph-based process-calculus with a generic type system (Barbara
König): we have developed a hypergraph-based process calculus
describing mobility. Composition of process graphs can be specified using
methods from category theory, such as co-limits. Analysis of process graphs
can be conducted with a generic type system (see below).
Mechanization of process verification: we are developping automatic
or semi-automatic techniques and implementing them. Our research
can be roughly divided into two topics, one dealing with the mechanization
of bisimulation proof techniques, the other with generic type systems.
These two topics are overlapping in parts.
Proof techniques for pure bisimulation (Christine
Röckl) can be mechanized with the help of a theorem prover,
such as Isabelle/HOL
(Higher Order Logic). We conducted a case study, applying this method to
several bisimulation proofs which are not feasible any more when conducted
manually.
While proof techniques for bisimulation are complete (in the sense
that a proof could be found for every pair of bisimilar processes), mechanization
leads to a semi-automatic method where interaction with the user is required.
Generic type systems (Barbara
König): another approach is to employ non-complete, but fully
automatic methods, such as type systems. We investigate generic type
systems which can be instantiated in order to analyze certain properties
of processes, such as input/output behaviour, secrecy or absence of deadlocks.
We can give proofs for important properties of type systems (subject
reduction property, type inference, etc.) for the general case.
Sonderforschungsbereich
342 of the German Research Council "Tools and methods for parallel
computer architectures",
French-German cooperation project "Verification techniques for imperative
higher order programming languages" with the INRIA Institute at Sophia
Antipolis.