Using Process Algebras for the Semantic Analysis of Data Flow Networks


IEICE TRANSACTIONS on Information and Systems   Vol.E78-D    No.8    pp.959-968
Publication Date: 1995/08/25
Online ISSN: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Computer Systems
computer systems,  software theory,  data flow networks,  semantics,  formal methods,  specification and verification,  process algebras,  

Full Text: PDF>>
Buy this Article

Data flow is a paradigm for concurrent computations in which a collection of parallel processes communicate asynchronously. For nondeterministic data flow networks many semantic models have been defined, however, it is complex to reason about the semantics of a network. In this paper, we introduce a transformation between data flow networks and the LOTOS specification language to make available theories and tools developed for process algebras for the semantic analysis based on traces of the networks. The transformation does not establish a one-to-one mapping between the traces of a data flow network and the LOTOS specification, but maps each network in a specification which usually contains more traces. The obtained system specification has the same set of traces as the corresponding network if they are finite, otherwise also non fair traces are included. Formal analysis and verification methods can still be applied to prove properties of the original data flow network, allowing in case of networks with finite traces to prove also network equivalence.