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

Other

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

Fingerprint

Model checking
Specifications
Temporal logic

ASJC Scopus subject areas

  • Software

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]

Model checking process with goal oriented requirements analysis. / Ogawa, Hideto; Kumeno, Fumihiro; Honiden, Shinichi.

Proceedings - 15th Asia-Pacific Software Engineering Conference, APSEC 2008. 2008. p. 377-384 4724569.

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

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., 4724569, pp. 377-384, 15th Asia-Pacific Software Engineering Conference, APSEC 2008, Beijing, China, 08/12/2.
Ogawa H, Kumeno F, Honiden S. Model checking process with goal oriented requirements analysis. In Proceedings - 15th Asia-Pacific Software Engineering Conference, APSEC 2008. 2008. p. 377-384. 4724569
Ogawa, Hideto ; Kumeno, Fumihiro ; Honiden, Shinichi. / Model checking process with goal oriented requirements analysis. Proceedings - 15th Asia-Pacific Software Engineering Conference, APSEC 2008. 2008. pp. 377-384
@inproceedings{37d3e2e1e80841f4a4f85be6d1d80c4d,
title = "Model checking process with goal oriented requirements analysis",
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.",
author = "Hideto Ogawa and Fumihiro Kumeno and Shinichi Honiden",
year = "2008",
month = "12",
day = "1",
language = "English",
isbn = "9780769534466",
pages = "377--384",
booktitle = "Proceedings - 15th Asia-Pacific Software Engineering Conference, APSEC 2008",

}

TY - GEN

T1 - Model checking process with goal oriented requirements analysis

AU - Ogawa, Hideto

AU - Kumeno, Fumihiro

AU - Honiden, Shinichi

PY - 2008/12/1

Y1 - 2008/12/1

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

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

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

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

M3 - Conference contribution

AN - SCOPUS:67650513360

SN - 9780769534466

SP - 377

EP - 384

BT - Proceedings - 15th Asia-Pacific Software Engineering Conference, APSEC 2008

ER -