抄録
B-028
UMLシーケンス図の構造記述から線形時相論理式への自動変換手法
◎宮本直樹・和崎克己（信州大）
システムの仕様を検証する手法として，モデル検査が注目されている．モデル検査で要求仕様を検証するためには，時相論理式で仕様の性質を記述することが多い．特に，時間の進み方が一直線である性質を記述できる線形時相論理（LTL）式が用いられる．本研究では，モデルの振る舞いを時系列で記述できるUMLのシーケンス図を，LTL式に自動変換する手法を提案する．シーケンス図の複合フラグメント要素に仕様パターン名を記入し，LTL式と要求仕様を一意に対応付けることで，自動変換を実現する．また，複合フラグメント要素を組み合わせることで，LTL式同士の論理演算を実現した．自動変換により，LTL式の記述の負担軽減を図る．