Model checking process with goal oriented requirements analysis

Hideto Ogawa*, Fumihiro Kumeno, Shinichi Honiden

*Corresponding author for this work

Research output: Contribution to journalConference articlepeer-review

2 Citations (Scopus)


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, specification-level 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
Article number4724569
Pages (from-to)377-384
Number of pages8
JournalNeonatal, Paediatric and Child Health Nursing
Publication statusPublished - 2008
Externally publishedYes
Event15th Asia-Pacific Software Engineering Conference, APSEC 2008 - Beijing, China
Duration: 2008 Dec 22008 Dec 5

ASJC Scopus subject areas

  • Pediatrics


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

Cite this