Model checking process with goal oriented requirements analysis

Hideto Ogawa*, Fumihiro Kumeno, Shinichi Honiden


研究成果: Conference article査読

2 被引用数 (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.

ジャーナルNeonatal, Paediatric and Child Health Nursing
出版ステータスPublished - 2008
イベント15th Asia-Pacific Software Engineering Conference, APSEC 2008 - Beijing, China
継続期間: 2008 12月 22008 12月 5

ASJC Scopus subject areas

  • 小児科学


「Model checking process with goal oriented requirements analysis」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。