A transformation system for concurrent processes |
| |
Authors: | Nicoletta De Francesco Antonella Santone |
| |
Affiliation: | (1) Dipartimento di Ingegneria dell'Informazione, Università di Pisa, I-56126 Pisa, Italy (e-mail: {nico,santone}@iet.unipi.it) , IT |
| |
Abstract: | Program transformation techniques have been extensively studied in the framework of functional and logic languages, where
they were applied mainly to obtain more efficient and readable programs. All these works are based on the Unfold/Fold program
transformation method developed by Burstall and Darlington in the context of their recursive equational language. The use
of Unfold/Fold based transformations for concurrent languages is a relevant issue that has not yet received an adequate attention.
In this paper we define a transformation methodology for CCS. We give a set of general rules which are a specialization of
classical program transformation rules, such as Fold and Unfold. Moreover, we define the general form of other rules, “oriented”
to the goal of a transformation strategy, and we give conditions for the correctness of these rules. We prove that a strategy
using the general rules and a set of goal oriented rules is sound, i.e. it transforms CCS programs into equivalent ones. We
show an example of application of our method. We define a strategy to transform, if possible, a full CCS program into an equivalent
program whose semantics is a finite transition system. We show that, by means of our methodology, we are able to a find finite
representations for a class of CCS programs which is larger than the ones handled by the other existing methods. Our transformational
approach can be seen as unifying in a common framework a set of different techniques of program analysis. A further advantage
of our approach is that it is based only on syntactic transformations, thus it does not requires any semantic information.
Received: 24 April 1997 / 19 November 1997 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|