Model checking process with goal oriented requirements analysis

Hideto Ogawa, Fumihiro Kumeno, Shinichi Honiden

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Citations (Scopus)

Abstract

Model checking is a powerful technique for verifying the correctness of a system's specification. But even when the specification has been verified to be correct, there is still the question of whether the specification covers all the expected behaviors. One of the most important issues for verification is the sufficiency of verification items. In model checking, specificationlevel properties such as reachability are well-studied, but the sufficiency of a specification against the preceding requirements still remains a challenge. In this paper, we propose a model-checking process with goal oriented requirements analysis, in which goal descriptions in a natural language are systematically refined into linear temporal logic formulae. Furthermore, the coverage of the verification result can be evaluated against the goal model. We developed a tool that supports the process, and applied it to an example. This process lowers the technical barriers to model checking and improves the sufficiency of system verification.

Original languageEnglish
Title of host publicationProceedings - 15th Asia-Pacific Software Engineering Conference, APSEC 2008
Pages377-384
Number of pages8
Publication statusPublished - 2008 Dec 1
Externally publishedYes
Event15th Asia-Pacific Software Engineering Conference, APSEC 2008 - Beijing, China
Duration: 2008 Dec 22008 Dec 5

Publication series

NameProceedings - Asia-Pacific Software Engineering Conference, APSEC
ISSN (Print)1530-1362

Other

Other15th Asia-Pacific Software Engineering Conference, APSEC 2008
CountryChina
CityBeijing
Period08/12/208/12/5

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Model checking process with goal oriented requirements analysis'. Together they form a unique fingerprint.

  • Cite this

    Ogawa, H., Kumeno, F., & Honiden, S. (2008). Model checking process with goal oriented requirements analysis. In Proceedings - 15th Asia-Pacific Software Engineering Conference, APSEC 2008 (pp. 377-384). [4724569] (Proceedings - Asia-Pacific Software Engineering Conference, APSEC).