2 0 0 0 OA モデル検査による設計検証
- 著者
- 吉岡 信和 田辺 良則 田原 康之 長谷川 哲夫 磯部 祥尚
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- コンピュータ ソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.31, no.4, pp.4_40-4_65, 2014-10-24 (Released:2014-12-24)
機器の高速化やネットワークの発展に伴い,多数の機器やコンポーネントを連携させ,高度な機能を提供する並行分散システムが一般的になってきている.そのようなシステムでは,振舞いの可能性が膨大であり,従来のレビューやシミュレーションで設計の振舞いの正しさを保証することは困難である.それに対して,網羅的にかつ自動的に振舞いに関する性質を調べるモデル検査技術が注目されている.本稿では,モデル検査技術の背景と5つの代表的なモデル検査ツールを紹介し,その応用事例や最新の研究動向を解説する.
2 0 0 0 OA 抽象化を用いた検証ツール
- 著者
- 田辺 良則 高井 利憲 高橋 孝一
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- コンピュータ ソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.22, no.1, pp.1_2-1_44, 2005-01-26 (Released:2008-09-09)
- 被引用文献数
- 1
モデル検査技法は,仕様に対する設計の妥当性検証への適用において,近年大きな成功をおさめている.この技法の適用範囲をさらに広げるためには,状態数爆発問題を解決することが必要である.この問題を解決する方法として注目されている抽象化技法,およびそれを実装したツールを紹介する.
1 0 0 0 OA Java PathFinderにおける探索打ち切りポリシーを用いたヒューリスティック探索
- 著者
- 前岡 淳 田辺 良則 石川 冬樹
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- コンピュータ ソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.30, no.3, pp.3_109-3_122, 2013-07-25 (Released:2013-08-31)
Java PathFinder (JPF)に代表されるソフトウェアモデル検査技術は,テスト工程における不具合検出に有効であるが,状態爆発への対応が課題となる.この課題を解決する手法として優先度に基づくヒューリスティック探索手法が提案されている.プログラムによって適する探索手法や優先度の付け方が異なるため,有効なヒューリスティック探索手法が多数存在することがのぞましい.本論文では,「範囲限定探索」に基づくヒューリスティック探索手法を提案する.従来手法は,ヒューリスティック関数によって各状態から不具合に早く到達できるかを見積もり,これに基づいて探索順序を決定する.これに対して提案手法では,「探索打ち切りポリシー関数」によって各状態から不具合に早く到達できるかを判断し,見込みが低い場合にはその状態からの探索を打ち切る.提案手法の有効性を検証するためにJPFに実装し,検証ツール評価用に作成されたテストプログラムを用いて既存手法との比較実験を行った.Javaによるテストプログラムを用いた実験の結果,提案手法が状態数比で2倍以上優位となるケースを確認し,ヒューリスティック探索の適用の幅が広がることを示した.