上流設計からモデル検査プロセスまでの一貫設計検証環境～UML記述からSPINモデル検査器用プロセス定義及び線形時相論理式への自動変換手法

摘要

SPINモデル検査器を実行するには，専用の仕様記述言語PROMELAで対象モデルを記述する．また，検査対象の仕様の記述には線形時相論理（LTL）式を用いる．本研究では，システム開発の上流設計段階で使われるUML 図を，PROMELAコード及びLTL式に自動変換する手法を提案する．UMLのステートマシン図と配置図を組みで利用し，ステートマシン図に，対象モデルの振る舞いや配置状況，要求仕様を記述し，PROMELAコードへの自動変換を実現する．一方，要求仕様として，UMLのシーケンス図を仕様パターンに準拠した記法に制限·展開することで，LTL式の自動生成を実現する．以上の機能を有する援用ツール群を試作し，ある通信プロトコルを対象とした上位設計に対する自動変換を実施し，評価を行った．