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.
Using Process Algebras for the Semantic Analysis of Data flow Networks
BERNARDESCHI, CINZIA;SIMONCINI, LUCA
1995-01-01
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
