通信ソフトウェアのテストにおけるMSCで記述された要求仕様のペトリネットを利用した意味検証と充足検証の方法 (<小特集>コンカレント・コラボレーション技術論文小特集)

概要

論文の詳細を見る
本論文は通信システムソフトウェアのテストの方法について記述する. テストの中でも要求仕様の意味検証に着目する. 要求仕様の記述形式はITU-T勧告のメッセージシーケンスヂャート(MSC)を使用する. 本論文はMSCで記述されたシステムの動作要求仕様を表すシナリオを想定し, 仕様として矛盾がないか否かの意味検証を行う方法を示す. 意味検証は, ペトリネットの既存の研究結果を有効に利用すべく, MSCをペトリネットでモデル化し, MSCの意味検証問題をペトリネットの部分可到達問題に帰着して行う. モデル化の際にその正当性についての議論も行い仕様が無矛盾であることと, 仕様にあるすべてのイベントが実行可能であることは等価であることを示す. 更に意味検証の方法として部分可到達問題を線形時間で解くアルゴリズムを示した. 次に実際に作成されたシステムの動作実行結果を表すトレースログが要求仕様であるシナリオを充足するか否かの充足検証についても考察する. 充足検証もペトリネットでモデル化し, 発火系列が与えられた場合の部分可到達問題に帰着し, この問題を線形時間で解くアルゴリズムを示す.
社団法人電子情報通信学会の論文
1997-07-25