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

Kentaro Go, Norio Shiratori

    研究成果: Article

    5 引用 (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.

    元の言語English
    ページ(範囲)258-273
    ページ数16
    ジャーナルIEEE Transactions on Software Engineering
    25
    発行部数2
    DOI
    出版物ステータスPublished - 1999

      フィンガープリント

    ASJC Scopus subject areas

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

    これを引用