Verification and refinement for system requirements

Kukhwan Song, Atsushi Togashi, Norio Shiratori

    Research output: Contribution to journalArticle

    Abstract

    Due to the large and complex information processing systems, formal description methods are needed for specification of systems and their efficient and reliable designs. During the early stage of system design, it is often necessary to modify or change system requirements which may influence the whole system design. We have proposed a new flexible description methodology, which copes with the modifications or changes in the system requirements, in order to obtain the formal specification of the system. We have also shown that function requirements can be modeled by a Logical Petri Net (LPN), which is a kind of extended Petri Nets, in order to derive the formal specification. In this paper, we propose a verification method of system requirements that contain some kinds of logical errors. Further, we show a method to decompose and refine a requirement description hierarchically, and discuss how to derive a formal specification from a requirement description flexibly along our refinement method against the changes of the requirement description in the system.

    Original languageEnglish
    Pages (from-to)1468-1478
    Number of pages11
    JournalIEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
    VolumeE78-A
    Issue number11
    Publication statusPublished - 1995 Nov

    Fingerprint

    Refinement
    Petri nets
    Requirements
    Systems analysis
    Formal Specification
    Petri Nets
    System Design
    Specifications
    Formal specification
    Information Processing
    Specification
    Decompose
    Necessary
    Methodology

    ASJC Scopus subject areas

    • Hardware and Architecture
    • Information Systems
    • Electrical and Electronic Engineering

    Cite this

    Verification and refinement for system requirements. / Song, Kukhwan; Togashi, Atsushi; Shiratori, Norio.

    In: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences, Vol. E78-A, No. 11, 11.1995, p. 1468-1478.

    Research output: Contribution to journalArticle

    Song, Kukhwan ; Togashi, Atsushi ; Shiratori, Norio. / Verification and refinement for system requirements. In: IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences. 1995 ; Vol. E78-A, No. 11. pp. 1468-1478.
    @article{ac39608d4e5649009ae686ca56bbb28e,
    title = "Verification and refinement for system requirements",
    abstract = "Due to the large and complex information processing systems, formal description methods are needed for specification of systems and their efficient and reliable designs. During the early stage of system design, it is often necessary to modify or change system requirements which may influence the whole system design. We have proposed a new flexible description methodology, which copes with the modifications or changes in the system requirements, in order to obtain the formal specification of the system. We have also shown that function requirements can be modeled by a Logical Petri Net (LPN), which is a kind of extended Petri Nets, in order to derive the formal specification. In this paper, we propose a verification method of system requirements that contain some kinds of logical errors. Further, we show a method to decompose and refine a requirement description hierarchically, and discuss how to derive a formal specification from a requirement description flexibly along our refinement method against the changes of the requirement description in the system.",
    author = "Kukhwan Song and Atsushi Togashi and Norio Shiratori",
    year = "1995",
    month = "11",
    language = "English",
    volume = "E78-A",
    pages = "1468--1478",
    journal = "IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences",
    issn = "0916-8508",
    publisher = "Maruzen Co., Ltd/Maruzen Kabushikikaisha",
    number = "11",

    }

    TY - JOUR

    T1 - Verification and refinement for system requirements

    AU - Song, Kukhwan

    AU - Togashi, Atsushi

    AU - Shiratori, Norio

    PY - 1995/11

    Y1 - 1995/11

    N2 - Due to the large and complex information processing systems, formal description methods are needed for specification of systems and their efficient and reliable designs. During the early stage of system design, it is often necessary to modify or change system requirements which may influence the whole system design. We have proposed a new flexible description methodology, which copes with the modifications or changes in the system requirements, in order to obtain the formal specification of the system. We have also shown that function requirements can be modeled by a Logical Petri Net (LPN), which is a kind of extended Petri Nets, in order to derive the formal specification. In this paper, we propose a verification method of system requirements that contain some kinds of logical errors. Further, we show a method to decompose and refine a requirement description hierarchically, and discuss how to derive a formal specification from a requirement description flexibly along our refinement method against the changes of the requirement description in the system.

    AB - Due to the large and complex information processing systems, formal description methods are needed for specification of systems and their efficient and reliable designs. During the early stage of system design, it is often necessary to modify or change system requirements which may influence the whole system design. We have proposed a new flexible description methodology, which copes with the modifications or changes in the system requirements, in order to obtain the formal specification of the system. We have also shown that function requirements can be modeled by a Logical Petri Net (LPN), which is a kind of extended Petri Nets, in order to derive the formal specification. In this paper, we propose a verification method of system requirements that contain some kinds of logical errors. Further, we show a method to decompose and refine a requirement description hierarchically, and discuss how to derive a formal specification from a requirement description flexibly along our refinement method against the changes of the requirement description in the system.

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

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

    M3 - Article

    AN - SCOPUS:0029404332

    VL - E78-A

    SP - 1468

    EP - 1478

    JO - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

    JF - IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences

    SN - 0916-8508

    IS - 11

    ER -