Institutional Repository

Functionality decomposition by compositional correctness preserving transformation

Show simple item record Brinksma, E Langerak, R 2018-05-30T08:56:17Z 2018-05-30T08:56:17Z 1995
dc.identifier.citation Brinksma E & Langerak R (1995) Functionality decomposition by compositional correctness preserving transformation. South African Computer Journal, Number 13, 1995 en
dc.identifier.issn 2313-7835
dc.description.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. en
dc.language.iso en en
dc.publisher South African Computer Society (SAICSIT) en
dc.subject Process algebra en
dc.subject Correctness preserving transformation en
dc.subject Decomposition en
dc.subject Bisimulation en
dc.title Functionality decomposition by compositional correctness preserving transformation en
dc.type Article en

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search UnisaIR


My Account