Petri net modelling of Occam programs for detecting indeterminacy, non-termination and deadlock anomalies
Proceedings of the Fourth International Workshop on Petri Nets and Performance Models (1991)
Melbourne, Victoria, Australia
Dec. 2, 1991 to Dec. 5, 1991
Zhiwei Xu , Dept. of Comput. Sci., New York Polytech. Univ., NY, USA
The authors 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.<
concurrency control, Occam, parallel programming, Petri nets, software engineering
Zhiwei Xu and O. de Vel, "Petri net modelling of Occam programs for detecting indeterminacy, non-termination and deadlock anomalies," Proceedings of the Fourth International Workshop on Petri Nets and Performance Models(PNPM), Melbourne, Victoria, Australia, , pp. 116-124.