Model checking process with goal oriented requirements analysis

Hideto Ogawa, Fumihiro Kumeno, Shinichi Honiden

研究成果: Conference contribution

5 引用 (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, 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.

元の言語English
ホスト出版物のタイトルProceedings - 15th Asia-Pacific Software Engineering Conference, APSEC 2008
ページ377-384
ページ数8
出版物ステータスPublished - 2008 12 1
イベント15th Asia-Pacific Software Engineering Conference, APSEC 2008 - Beijing, China
継続期間: 2008 12 22008 12 5

出版物シリーズ

名前Proceedings - Asia-Pacific Software Engineering Conference, APSEC
ISSN(印刷物)1530-1362

Other

Other15th Asia-Pacific Software Engineering Conference, APSEC 2008
China
Beijing
期間08/12/208/12/5

    フィンガープリント

ASJC Scopus subject areas

  • Software

これを引用

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