Coordinating Functional Processes using Petri Nets

Abstract

Functional programs are well suited for concurrent execution due to the Church-Rosser property. However, for many applications there is still need to explicitly specify process systems instead of relying on compilers. Coordination languages provide one viable solution to the problem of specifying concurrent process systems, since they do not interfere with the properties of the language used for the algorithmic specification of the processes. The coordination language K2 to be proposed in this paper is based on a variant of colored Petri nets. It primarily defines process systems with deterministic behavior since it is restricted to so-called synchronization graphs, but also allows for controlled forms of nondeterminism. Specifications based on Petri nets offer several advantages. An underlying net calculus facilitates formal analysis and verification of basic behavioral system properties such as safety and liveness. Graphical representations clearly expose structural dependencies among system components. System validation may be supported by interactively controlled stepwise execution and the display of intermediate system states. Our variant of colored Petri nets provides several forms of net abstractions which facilitate the systematic construction of complex systems from small subsystems by composition. Recursive specifications can be used to adapt the structure of a process system to actual problem sizes, to varying input parameters, and to the number of processing sites that are actually available.
[Content] [What's new?] [Hotlist] [Chair] [CS Dept] [Technical Faculty] [CAU Kiel]
Claus Aßmann <ca@informatik.uni-kiel.de>