In: Proc. 4th Int. Workshop on Petri Nets and Performance Models (PNPM'91), Melbourne, Australia, pages 116-124. IEEE Comp. Soc. Press, December 1991.
Abstract: In this paper we present a graph model based on Petri nets that can be used as a software development tool for parallel computational programs written in the occam language. In parallel computing the cooperation aspect of concurrency is emphasized, rather than the competitive aspect of multiple processes found in operating system applications. In developing and debugging a parallel computational program, users often want to ensure that their program will terminate (that is, it stops in finite time) and be determinate (that is, the same input data always produce the same result). Using the Petri net graph model, termination and determinacy can be mathematically defined, and algorithms for detecting these properties developed. In fact, the graph model defines an operational semantics for a non-trivial subset of occam, and can be used as a pedagogical aid as well as a tool for developing and synthesizing occam programs in parallel computing applications.