Modelling and Analysis of Concurrent Processes Connected by Streams

概要

論文の詳細を見る
A network of concurrent processes connected by streams is worth notice as a simple method for representing nontrivial problems by combining simple modules. We define such a network as a subclass of general communicating concurrent processes. A network in this class has some restrictions, for example, a stream must have only one producer and one consumer. However this is a practical class which can be used to represent many problems, and some representative classes of concurrent processes such as Hoare's CSP belong to this class. In this paper, we formulate the analysis of networks in this class based on the theory of Petri nets. We have clarified some general characteristic features of this class, a major one being that the class is livelock-free. The analysis includes the detection of deadlocks, dead code and the possibility of termination, along with the determination of a necessary buffer size for each stream. Here, we applied the analysis to networks described by the programming language Stella, which we developed, but the analysis is independent of specific languages. In order to achieve the above analysis, we implemented an automatic analysis system called SPRAT on a VAX-11/750. We successfully analyzed many networks which belong to this class using SPRAT.
一般社団法人情報処理学会の論文
1987-01-31