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

Kentaro Go, Norio Shiratori

    Research output: Contribution to journalArticle

    5 Citations (Scopus)

    Abstract

    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
    Volume25
    Issue number2
    DOIs
    Publication statusPublished - 1999

    Fingerprint

    Decomposition
    Specifications
    Formal specification
    Synchronization
    Association reactions
    Chemical analysis

    Keywords

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

    ASJC Scopus subject areas

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

    Cite this

    A decomposition of a formal specification : An improved constraint-oriented method. / Go, Kentaro; Shiratori, Norio.

    In: IEEE Transactions on Software Engineering, Vol. 25, No. 2, 1999, p. 258-273.

    Research output: Contribution to journalArticle

    @article{7fda140f72444fde9833561dffadbc71,
    title = "A decomposition of a formal specification: An improved constraint-oriented method",
    abstract = "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.",
    keywords = "Bisimulation, Constraint-oriented method, Decomposition, Equivalence, Formal specification, LOTOS",
    author = "Kentaro Go and Norio Shiratori",
    year = "1999",
    doi = "10.1109/32.761449",
    language = "English",
    volume = "25",
    pages = "258--273",
    journal = "IEEE Transactions on Software Engineering",
    issn = "0098-5589",
    publisher = "Institute of Electrical and Electronics Engineers Inc.",
    number = "2",

    }

    TY - JOUR

    T1 - A decomposition of a formal specification

    T2 - An improved constraint-oriented method

    AU - Go, Kentaro

    AU - Shiratori, Norio

    PY - 1999

    Y1 - 1999

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

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

    KW - Bisimulation

    KW - Constraint-oriented method

    KW - Decomposition

    KW - Equivalence

    KW - Formal specification

    KW - LOTOS

    UR - http://www.scopus.com/inward/record.url?scp=0032675795&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=0032675795&partnerID=8YFLogxK

    U2 - 10.1109/32.761449

    DO - 10.1109/32.761449

    M3 - Article

    AN - SCOPUS:0032675795

    VL - 25

    SP - 258

    EP - 273

    JO - IEEE Transactions on Software Engineering

    JF - IEEE Transactions on Software Engineering

    SN - 0098-5589

    IS - 2

    ER -