Functionality Decomposition by Compositional Correctness Preserving Transformation

Hendrik Brinksma, Romanus Langerak

Research output: Contribution to journal › Article › Academic › peer-review

54 Downloads (Pure)

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 languageUndefined
Pages (from-to)2-13
Number of pages12
JournalSouth African computer journal
Volume13
Publication statusPublished - 1995

Keywords

  • EWI-6395
  • IR-66257
  • FMT-PA: PROCESS ALGEBRAS

Cite this

Brinksma, Hendrik ; Langerak, Romanus. / Functionality Decomposition by Compositional Correctness Preserving Transformation. In: South African computer journal. 1995 ; Vol. 13. pp. 2-13.
@article{451eacc4a1e848349fbb61bb7adf47e0,
title = "Functionality Decomposition by Compositional Correctness Preserving Transformation",
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.",
keywords = "EWI-6395, IR-66257, FMT-PA: PROCESS ALGEBRAS",
author = "Hendrik Brinksma and Romanus Langerak",
year = "1995",
language = "Undefined",
volume = "13",
pages = "2--13",
journal = "South African computer journal",
issn = "1015-7999",
publisher = "South African Institute of Computer Scientists and Information Technologists",

}

Brinksma, H & Langerak, R 1995, 'Functionality Decomposition by Compositional Correctness Preserving Transformation' South African computer journal, vol. 13, pp. 2-13.

Functionality Decomposition by Compositional Correctness Preserving Transformation. / Brinksma, Hendrik; Langerak, Romanus.

In: South African computer journal, Vol. 13, 1995, p. 2-13.

Research output: Contribution to journal › Article › Academic › peer-review

TY - JOUR

T1 - Functionality Decomposition by Compositional Correctness Preserving Transformation

AU - Brinksma, Hendrik

AU - Langerak, Romanus

PY - 1995

Y1 - 1995

N2 - 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.

AB - 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.

KW - EWI-6395

KW - IR-66257

KW - FMT-PA: PROCESS ALGEBRAS

M3 - Article

VL - 13

SP - 2

EP - 13

JO - South African computer journal

JF - South African computer journal

SN - 1015-7999

ER -

Brinksma H, Langerak R. Functionality Decomposition by Compositional Correctness Preserving Transformation. South African computer journal. 1995;13:2-13.

Access to Document