モデル模査における妥当性確認を目的とした並行システムの表現手法

摘要

並行ソフトウェアシステムのモデル検査においては，モデルが正確で十分な精度を備えていることが求められる．本論文は，モデルの理解を視覚的に支援する，有限状態機械の直観的な表現手法を提案する．対象とするモデルはFSPで，表現手法はLTS表現に基づいている．提案する4種類の図法により，LTS表現の状態爆発を抑制したり，並行システムにしばしば現れる特徴的な状態遷移を明示的に表現することが可能となる．FSP記述を提案図法により可視化し，モデルの理解支援を対話的に行うツールを作成した．