著者

青木 翼 長谷川 哲夫 宮本 博暢 渡邊 竜明

出版者

一般社団法人情報処理学会

雑誌

情報処理学会研究報告ソフトウェア工学(SE) (ISSN:09196072)

巻号頁・発行日

vol.2008, no.29, pp.203-210, 2008-03-18

被引用文献数

1

---

モデル検査によりソフトウェア設計の品質を向上させることが注目されている.一方,モデル検査を開発に適用するノウハウはまだ不足している.本論文ではモデル検査をソフトウェア開発に適用させるためのガイドラインについて報告をする.このガイドラインではモデル検査を実施する目的と効果,モデル検査が適用できる箇所,モデルや検証式を作成する手順,モデルや検証式の記述テクニックの4点について説明を行っている.While improvement of the quality of software design using model checking is required, the current know-how pertaining to the application of model checking is insufficient. This paper describes the guideline for model checking in UPPAAL, which consists of 4 sections explaining the objectives and outcomes of model checking, target documentation, process, techniques of models and verification expressions building.