シーケンス図からの時間性能モデル検査用オブザーバ生成手法(テスト・検証(一般セッション))

スポンサーリンク

概要

論文の詳細を見る
多種のシステムを低コストで短期間に開発しなければならない組込みソフトウェアなどの分野でも、ソフトウェアの大規模化が進む一方で大量販売により出荷後の不具合修正コストは大きく、モデル検査手法のような設計検証の自動化技術がより容易に使えるようになることに期待が高まっている。設計者にとってモデル検査の敷居が高い理由のひとつは、検証したい性質を時相論理式で与える点がある。本稿では、モデル検査ツールUPPAALを対象として、シーケンスチャートから検証したい性質を表現するオブザーバを機械的に生成する手法を提案する。注目するシーケンスに対応する可能性のある挙動の完全な監視と、注目しない事象の透明化を特徴とする。また、本手法を通信プロトコルのアプリケーションに適用してオーバーヘッドの評価を行った。
2006-03-23

著者

関連論文

もっと見る

スポンサーリンク