Functionality decomposition by compositional correctness preserving transformation

Ed Brinksma, Rom Langerak, Peter J. Broekroelofs

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademic

    4 Citations (Scopus)
    15 Downloads (Pure)

    Abstract

    In this paper 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 languageEnglish
    Title of host publicationComputer Aided Verification
    Subtitle of host publication5th International Conference, CAV '93, Elounda, Greece, June 28–July 1, 1993. Proceedings
    EditorsCostas Courcoubetis
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer
    Pages371-384
    Number of pages14
    ISBN (Electronic)978-3-540-47787-7
    ISBN (Print)978-3-540-56922-0
    DOIs
    Publication statusPublished - 1993
    Event5th International Conference on Computer Aided Verification, CAV 1993 - Elounda, Greece
    Duration: 28 Jun 19931 Jul 1993
    Conference number: 5

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume679
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference5th International Conference on Computer Aided Verification, CAV 1993
    Abbreviated titleCAV
    CountryGreece
    CityElounda
    Period28/06/931/07/93

      Fingerprint

    Cite this

    Brinksma, E., Langerak, R., & Broekroelofs, P. J. (1993). Functionality decomposition by compositional correctness preserving transformation. In C. Courcoubetis (Ed.), Computer Aided Verification: 5th International Conference, CAV '93, Elounda, Greece, June 28–July 1, 1993. Proceedings (pp. 371-384). (Lecture Notes in Computer Science; Vol. 679). Berlin, Heidelberg: Springer. https://doi.org/10.1007/3-540-56922-7_31