Specifying Systems of Cooperating Processes

Abstract

Programming distributed computer systems is still a difficult organizational problem. A viable approach to render this problem manageable are coordination languages which describe distributed process systems. They strictly separate the specification of process communication structures from those of the computations to be performed by the processes. The coordination language K2 to be proposed in this paper is based on a variant of coloured Petri-nets which primarily defines process systems with deterministic behaviour, but also allows for controlled forms of nondeterminism. Net-based specification of cooperating processes combine the advantages of an underlying calculus which facilitates formal analysis and verification of an orderly system behaviour, graphical representations which clearly expose structural dependencies among system components, and last not least of an interactively controlled simulation by stepwise execution and the possibility to display intermediate states of token distributions. They also provide various forms of net abstractions including recursive specifications which allow for the systematic construction of large systems from small subsystems by net composition. The K2 approach includes compilers to convert these specifications into executable code.

Keywords

distributed computing, cooperating processes, coloured Petri-nets, formal verification
[Content] [What's new?] [Hotlist] [Chair] [CS Dept] [Technical Faculty] [CAU Kiel]
Claus Aßmann <ca@informatik.uni-kiel.de>