Abstract
We present an algorithm for the decomposition of processes in a process algebraic framework. Decomposition, or the refinement of
process substructure, is an important design principle in the top-down development of concurrent systems. In the approach that we follow
the decomposition is based on a given partition of the actions of a system specification, such that for each partition class a subprocess
must be created that realizes the actions in that class. In addition a suitable synchronization structure between the subprocesses must be
present to ensure that the composite behaviour of the subprocesses is properly related to the behaviour of the original specification. We
present our results for the process-algebraic specification language LOTOS and give a compositional algorithm for the transformation
of the original specification into the required subprocesses. The resulting specification is observation congruent with the original,
and, interestingly enough, the subprocesses inherit much of the structure of the original specification. The correctness preserving
transformation has been implemented in a tool and has been used for the derivation of protocol specifications from formal descriptions
of the desired service. This is possible as it can be shown that the required synchronization mechanisms between the subprocesses can
be readily implemented over (reliable) asynchronous media.
Original language | English |
---|---|
Pages (from-to) | 2-13 |
Number of pages | 12 |
Journal | South African computer journal |
Volume | 13 |
Publication status | Published - 1995 |
Keywords
- FMT-PA: PROCESS ALGEBRAS