A decomposition of a formal specification: An improved constraint-oriented method

Kentaro Go*, Norio Shiratori

*Corresponding author for this work

    Research output: Contribution to journalArticlepeer-review

    5 Citations (Scopus)


    In this paper, the authors propose a decomposition method for a formal specification that divides the specification into two subspecifications composed by a parallel operator. To make these specification behaviors equivalent before and after decomposition, the method automatically synthesizes an additional control specification, which contains the synchronization information of the decomposed subspecifications. The authors prove that a parallel composition of the decomposed subspecifications synchronized with the control specification is strongly equivalent with the original (monolithic) specification. The authors also write formal specifications of the OSI application layer's association-control service and decompose it using their method as an example of decomposition of a practical specification. Their decomposition method can be applied to top-down system development based on stepwise refinement.

    Original languageEnglish
    Pages (from-to)258-273
    Number of pages16
    JournalIEEE Transactions on Software Engineering
    Issue number2
    Publication statusPublished - 1999


    • Bisimulation
    • Constraint-oriented method
    • Decomposition
    • Equivalence
    • Formal specification
    • LOTOS

    ASJC Scopus subject areas

    • Electrical and Electronic Engineering
    • Computer Graphics and Computer-Aided Design
    • Software


    Dive into the research topics of 'A decomposition of a formal specification: An improved constraint-oriented method'. Together they form a unique fingerprint.

    Cite this