研究目標 7「検証支援ツールの入出力インタフェースの開発」

3.7.1 当初の想定

(1) 想定する仮説等

これまでに設計した機能モジュールを実装し，統合することにより，本研究の目的であ る UML で記述された設計ドキュメントを対象とした SMV による検証を支援するツールを実 現することが可能となる．

ここで，どのような環境上でツールを実装するかについて検討する必要がある．ここで は，Java などの，UML を用いた開発に広く用いられている環境での実装を行う．

(2) 当初の到達目標と期待される効果

ここで設定する到達目標としては，各機能モジュールの実装ならびに機能モジュールの 統合による検証支援ツールの開発とする．また，検証支援ツールの開発の一環として，UML モデリングツールの出力を直接扱うための入力インタフェースおよび，NuSMV の出力を整 形するための出力インタフェースについても併せて開発する．

検証支援ツールの実装により，本研究の目的であるモデル検査を用いたソフトウェアの 設計支援環境が実現される．そして，検証支援ツールの入出力インタフェースを開発する ことにより，ツールの利便性の向上が期待される．

3.7.2 研究プロセスと成果

(1) 研究プロセス

本研究目標を達成するため，以下のプロセスに従って研究開発を実施した．

1. 機能モジュールの設計書を元に，ツール作成を外注するための仕様書を作成する．

2. 上述の機能モジュールを統合した，検証支援ツールの仕様書を作成する．

(2) 具体的な研究成果の内容 １．機能モジュールの仕様書の作成

本研究で開発する検証支援ツールの概要を図 3-7-1 に示す．本ツールは 5 つの機能モジ ュールと，入出力インタフェースから構成される．まず，機能モジュールの 1 つである候 補提示モジュールを実装するため，候補提示モジュールの設計書をもとに仕様書を作成し た．その上で 8 月上旬に開発業者への発注を行い，9 月中旬に納品および検収を完了した．

70

図 3-7-1:検証支援ツールの概要

次に，残りの 4 つの機能モジュールについては 1 つの機能モジュール（抽象化・変換モ ジュール）として仕様書を作成した．その上で，11 月上旬に開発業者への発注を行い，12 月上旬に納品および検収を完了した．

２．検証支援ツールの仕様書の作成

上述の機能モジュールを統合し，検証支援ツールを完成させるため，まず入出力インタ フェースの設計を行った．

本ツールの入力インタフェースは，astah* community で作成された UML の状態マシン図 とシーケンス図のモデリングデータ(*.asta)と，仕様テンプレートに基づいて記述された 要求仕様(*.ctl)を読み込むことが可能である．*.ctl ファイルはテキストファイル形式で 作成するものとする．

次に，本ツールは抽象化・変換モジュールが生成した SMV プログラム(*.smv)をモデル検 査ツール NuSMV へと入力して検証を行う．NuSMV による検証結果は検証結果ファイル (*.out)として保存される．*.out ファイルはテキストファイル形式で保存されるものとす る．

本ツールの出力インタフェースは，NuSMV が出力した検証結果ファイルを読み込み，整 形済みの検証結果ファイル(*.result)を出力する．また，もし検査式が満たされなかった 場合は，NuSMV が生成した反例を違反箇所情報(*.ce)として出力する．

また，本ツールはコマンドラインで起動する．起動方法を図 3-7-1 に示す．

図 3-7-1:検証支援ツールの起動方法

検証支援ツールについては 12 月下旬に開発業者への発注を行い，1 月上旬に納品および 検収を完了した．

java –jar umltool.jar プロジェクトファイル名.asta 検査式ファイル名.ctl

71 3.7.3 課題とその対応

(1) 課題と問題点

本研究では，機能モジュールの実装のため，作成した設計書をもとに仕様書を作成した．

また，検証支援ツールの実装のため，入出力インタフェースの設計を行った．ここで想定 される課題は，入出力インタフェースにどこまでの機能を持たせるか，となる．

ここではツールの最低限の機能として，入力インタフェースには，モデリングデータお よび仕様テンプレートによる検査特性の読み込み機能を持たせることとする．また出力イ ンタフェースは，NuSMV が出力した検証結果の整形機能を持たせることとする．

今後の課題として，開発したツールの適用実験を通して，ユーザから意見や要望をいた だくことで，入出力インタフェースの評価を行う必要がある．

将来の応用方法としては，本研究で開発した入出力インタフェースは，同様の用途をも つ検証ツールを開発する場合，そのインタフェースへの応用が可能である．

72