DESIMOCは、UMLシーケンス図と状態マシン図によって記述したモデルを入力とする。オブジェクト間通信では、各オブジェクトの状態に応じたメッセージ送信と非同期メッセージによって様々な動作シナリオが生じるが、DESIMOCは全ての動作シナリオを網羅的に探索し、検査項目に違反する動作シナリオを検出する。" />

大会名称
2010年 情報科学技術フォーラム(FIT)
大会コ-ド
F
開催年
2010
発行日
2010/8/20
セッション番号
4B
セッション名
モデル検査・検証・信頼性
講演日
2010/09/08
講演場所(会議室等)
B会場(総合学習プラザ1F 第6講義室)
講演番号
B-018
タイトル
状態遷移を持つオブジェクト間通信のモデル検査技術
著者名
大貫 智洋上野 浩一郎磯田 誠
キーワード
モデル検査, Model Checking
抄録
分散システムなど複数のオブジェクトが互いに通信を行うシステムでは、オブジェクトの振舞いによって様々な動作シナリオが生じるため、人手によるレビューで全ての不具合を発見することは困難である。これに対し我々は、オブジェクト間通信の仕様をモデル検査するツール""DESIMOC""を開発した。
DESIMOCは、UMLシーケンス図と状態マシン図によって記述したモデルを入力とする。オブジェクト間通信では、各オブジェクトの状態に応じたメッセージ送信と非同期メッセージによって様々な動作シナリオが生じるが、DESIMOCは全ての動作シナリオを網羅的に探索し、検査項目に違反する動作シナリオを検出する。
本文pdf
PDF download (324.3KB)