Calculi and Algebras of Concurrency: Extensions, Tools and Applications

Description

Project Title:: Calculi and Algebras of Concurrency: Extensions, Tools and Applications
Acronym:: CONCUR 2
Number:: 7166
Work Area:: Theories for Concurrency & Real Time; Specification & Verification
Coordinator:: Technische Universiteit Eindhoven
Dept. Mathematics & Computing Science
Postbus 513
NL - 5600 MB EINDHOVEN
Coordinator Country:: NL
Partners: Ålborg Universitet DK
INRIA F
CWI NL
SICS S
University of Edinburgh UK
University of Sussex UK
University of Oxford UK
Associate Partners
ECRC D
INPG F
Chalmers University of Technology S
Sharp Laboratories of Europe UK
Contact Point:: Prof. Dr. J.C.M. Baeten
Telephone:: +31/40 47 4124
Fax:: +31/40 46 3922
E-Mail:: josb@win.tue.nl
Keywords:: concurrency, process calculus, CCS, CSP, ACP
Start Date:: 1 September 92
Duration:: 36 months
Status:: running
Abstract:: Concurrency theory is important for the specification and verification of concurrent and distributed systems. CONCUR 2 will extend process algebra and logical calculi to incorporate real-time aspects, probabilistic non-determinism, value passing and infinite state spaces. CONCUR 2 aims for a unified view on process algebra, and will design, specify and implement supporting software tools, and common formats and interfaces for such tools. The project is a continuation of CONCUR 1 (3006).

AIMS

The objectives of CONCUR 2 are to:
- Extend process algebra and related logical calculi in the three directions that emerged as the most promising during CONCUR 1: real-time and probabilistic non-determinism, abstract datatypes and value passing, and infinite state spaces. For these extensions a wide range of potential applications exists.
- Obtain a unified view of process algebra at an advanced level. This means a unified view of the application of the different styles and mathematical approaches (CCS, MEIJE - operational semantics; CSP - model-based semantics; ACP - axiomatic semantics) as well as a coherent picture of the family of extensions that is being developed.
- Design, specify and implement common formats and interfaces that allow parallel and consistent tool development of many sites.
- Design, specify and implement prototype tools that allow construction and analysis of process algebra descriptions involving the three directions of extension mentioned above.

APPROACH AND METHODS

The project should deliver both a significant extension of theory and notation of process algebras and related calculi, exemplified by a substantial range of case studies, as well as some de facto software standards concerning tool design and tool interfacing. To this end, three lines of research will be pursued:
- theoretical research, on the extension and unification of process algebras and calculi
- tool development, ie the design, specification and implementation of prototype software tools, plus common formats and interfaces for them
- the application of the theory and tools in relevant case-studies.

PROGRESS AND RESULTS

The project is making good progress in all areas of its workplan. Extensions of process algebras and logical calculi that incorporate real-time aspects, probabilistic non-determinism, value passing, message passing, and infinite state spaces are further developed.
In order to unify different approaches, there is new work on the general theory of SOS-semantics, and its connection to axiomatisations; also, new work on general process algebra (especially in the real-time area) that has a wide range of tailor-made subcalculi.
A first version of the CONCUR2 toolset is available. Through a fixed exchange format based on transition systems, a wide range of tools supporting the design, specification and verification of concurrent and distributed systems can work together. Updates and extensions of the different tools are also achieved.

POTENTIAL

The strength of the consortium derives from its combination of the largest academic teams working on process algebra, as well as on the fact that all the partners have long-standing experience in tool design for process algebra. In addition, each partner has access to industrial groups who can suggest or evaluate realistic case-studies. The partners share the ambition to see process algebra and calculi becoming a realistic tool for industrial system designers within the next five years.

LATEST PUBLICATIONS

Baeten J C M and Bergstra J A Non interleaving process algebra Proc. concur'93, LNCS (1993)
Prasad K V S A calculus of value broadcasts Proc. parle'93, LNCS 694 (1993)
Hansson H Modelling real-time and reliability In: Formal Methods in Fault Tolerance, Vytopil J, FDed, Kluwer (1993)
Hennessy M and Liu X A modal logic for message passing processes Proc. cav'93, LNCS 697 (1993)
Cerans K, Godskesen J and Larsen K G Timed modal specification - theory and tools Proc. cav'93, LNCS 697 (1993)

INFORMATION DISSEMINATION ACTIVITIES

All CONCUR2 partners publish widely in international journals and conference proceedings. Notably, the series of CONCUR conferences should be mentioned. The Fourth international conference on concurrency theory (CONCUR'93) was held in AugustÊ23-26, 1993 in Hildesheim, Germany. A one-day Workshop on Process Algebra and Performance Modelling was held in Edinburgh on May 21, 1993.

Sven Müßig, last update 07-nov-1995. Your feedback is welcome.