(57)【要約】【課題】要求仕様からモデル検査ツールSPINのモデル記述言語の実行モデルを自動生成し早期の段階で要求仕様の検証を行う要求仕様自動検証方式を提供する。【解決手段】クライアント11のユーザは要求仕様の記述画面で必要な項目への記述を行って要求仕様をアップロードして要求仕様ファイル２に格納する。実行モデル生成処理部７は、前記ユーザからの指示により起動し、処理フローにしたがって要求仕様ファイル２から実行モデル生成に関する項目データを抽出するとともに、テンプレートファイル４から実行モデル生成に必要なテンプレートを参照し、さらに変換辞書ファイル５から実行モデル生成に関し変換を要する項目データについて辞書を参照し、実行モデルを自動生成して実行モデルファイル３に格納する。検証処理部８は、実行モデルファイル３から検証処理に必要なデータを抽出するとともに要求仕様ファイル２からも必要なデータを抽出して検証を行う。【選択図】図６
2008305079.tif 000002
【特許請求の範囲】
【請求項１】
実行モデル生成に関するデータ項目について要求仕様記述がなされた要求仕様を格納する要求仕様ファイルと、
実行モデル生成処理手段の処理で使用するテンプレート名およびテンプレートを格納するテンプレートファイルと、
実行モデル生成処理手段の処理で使用する要求仕様記述名とモデル検査ツールSPINのモデル記述言語のコードに記述する文字列との対応を辞書として格納する変換辞書ファイルと、
検証処理手段の処理で使用する検証閾値を格納する検証ファイルと、
実行モデル生成処理手段の処理によって自動生成された実行モデルを格納する実行モデルファイルと、を有し、
ユーザ指示により起動され、前記要求仕様ファイルに格納された要求仕様の中から実行モデル生成に関するデータ項目を抽出し、抽出した前記データ項目について前記テンプレートファイルに格納されたテンプレートおよび前記変換辞書ファイルに格納された辞書データを用いて実行モデルを自動的に生成する実行モデル生成処理手段と、
前記実行モデルファイルに格納された前記実行モデルについて前記要求仕様から必要なデータ項目を参照して該必要なデータ項目が前記実行モデルの所定位置に記述されているかを検証し、またモデル検査ツールSPINを起動して前記実行モデルに係るシンタックス・チェックを実行する検証処理手段と、
を備えていることを特徴とする要求仕様自動検証方式。
【請求項２】
前記要求仕様ファイルに格納され記述される要求仕様には、機能要求項目または非機能要求項目についてそれぞれ統一モデリング言語ＵＭＬのユースケース図を用いてユースケースを記述するデータ項目が設けられ、さらに形式的仕様記述言語ＶＤＭ−ＳＬの「操作定義」構文に基づき、前記ユースケース記述における前記データ項目に項目名、次のイベント、外部アクセスの項目、および前記データ項目の下位階層のデータ項目にも次のイベントの項目が設けられ、
前記実行モデル生成処理手段は、前記要求仕様ファイルに格納された前記要求仕様の前記外部アクセス、前記項目名、前記次のイベントについて前記テンプレートファイルに格納されたテンプレートおよび前記変換辞書ファイルに格納された辞書データを参照して実行モデルを自動的に生成し、前記検証処理手段は、前記実行モデルファイルに格納された前記実行モデルについて前記要求仕様から前記必要なデータ項目を参照して前記必要なデータ項目が前記実行モデルの所定位置に記述されているかを検証し、さらにモデル検査ツールSPINを起動して前記実行モデルに係るシンタックス・チェックを実行することを特徴とする請求項１記載の要求仕様自動検証方式。
【請求項３】
前記検証処理手段は、前記実行モデル生成処理手段の起動後の所定時間後に起動するよう設定され、前記所定時間後に前記実行モデル生成処理手段から起動され、該起動と同時に前記要求仕様に係る項目名および版数が通知されるとともに前記実行モデルファイルに格納された前記実行モデルについて前記要求仕様から前記項目名および版数に係る必要なデータを参照することを特徴とする請求項１記載の要求仕様自動検証方式。
【請求項４】
前記検証処理手段は、前記検証ファイルから前記検証閾値を参照し、前記検証閾値内に前記実行モデル生成処理が終了しているかを検証することを特徴とする請求項３記載の要求仕様自動検証方式。
【請求項５】
前記検証処理手段は、検査したい条件を追記するためのテンプレートが前記テンプレートファイルに格納されたテンプレートに補充され、該補充されたテンプレートに基づいて実行モデルが生成された場合には、線形時相論理の検査式をモデル検査ツールSPINに入力
して、追記された条件を含めて前記実行モデルを検証することを特徴とする請求項３記載の要求仕様自動検証方式。
【請求項６】
前記条件は、外部アクセスの項目名間での競合の有無を検査するものであることを特徴とする請求項５記載の要求仕様自動検証方式。
【請求項７】
ユーザ指示により起動と指定時間後の停止とを指示され、前記実行モデルファイルに格納されている実行コードを読み込み、モデル検証ツールSPINを動作させてシミュレーションを実行するとともに前記指定時間後に動作を停止させ、動作停止後に前記シミュレーション実行結果を出力するシミュレーション実行処理手段をさらに備えていることを特徴とする請求項１記載の要求仕様自動検証方式。
【請求項８】
前記シミュレーション実行処理手段は、前記シミュレーション実行結果として、シミュレーションチャート、または、シミュレーショントレースを出力することを特徴とする請求項７記載の要求仕様自動検証方式。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、組み込みソフトウェアを含むソフトウェア、特にイベント駆動型のソフトウェアの要求仕様を検証するにあたって、要求仕様からモデル検査ツールSPINのモデル記述言語Promelaの実行モデルを生成し当該モデルで要求仕様を自動検証する技術に関する。
【背景技術】
【０００２】
要求仕様を検証する従来技術として、モデル検査手法が当業者に知られている。
特許文献１には、ユーザ要求に対し分析情報を入力して概念モデルを生成し、次いで概念モデルの設計クラス図を、並行、並列なモジュールに分割して分割設計クラス図を生成し、分割設計クラス図によって表されるモジュールについて分割設計クラス図に展開された属性でモジュール間を接続するためのポートを定義してモジュール間通信路を決定し、次いで機能モデルの実装コードを生成し、実装コードのシミュレーションを実行して、モジュール分割の正当性を評価して機能モデルの検証を行う技術が記載されている。
また非特許文献１には、モデル検査手法のツールとしてSPINが紹介されている。
【０００３】
【特許文献１】国際公開 ＷＯ ２００６/００３７０２
【非特許文献１】B.Berard 他７名「Systems and Software Verification」Springer ,2001/08,pp.139-144
【発明の開示】
【発明が解決しようとする課題】
【０００４】
要求仕様の検証にあたって、従来技術であるモデル検査手法はモデルを記述するためモデル検査のツールに対応したモデル記述言語を作成する必要がある。
特許文献１は、ユーザ要求に対し分析情報を入力して概念モデルを生成し、次いで概念モデルの設計クラス図を、並行、並列なモジュールに分割して分割設計クラス図を生成し、分割設計クラス図によって表されるモジュールについて分割設計クラス図に展開された属性でモジュール間を接続するためのポートを定義してモジュール間通信路を決定し、次いで機能モデルの実装コードを生成し、実装コードのシミュレーションを実行して、モジュール分割の正当性を評価して機能モデルの検証を行う技術を記載しているが、要求仕様からモデル検査ツールSPINのモデル記述言語Promelaの実行モデルを自動生成することについては触れられていない。
【０００５】
非特許文献１は、モデル検査手法のツールとしてSPINを紹介している。モデル検査ツールSPINではモデルを「Promela」というモデル記述言語で記述する必要がある。しかしモデル記述言語「Promela」の習得が必要であり、更に要求仕様をモデル記述言語「Promela」で再記述が必要となり、作業工数も増加し、また、再記述による漏れ、抜け、誤りなどが発生する可能性が高い。
【０００６】
本発明は、これらの問題点を解決し、要求仕様からモデル検査ツールSPINのモデル記述言語Promelaの実行モデルを自動生成し早期の段階で要求仕様の検証を行う要求仕様自動検証方式を提供することを目的とする。
【課題を解決するための手段】
【０００７】
上記目的を達成するために本発明は、実行モデル生成に関するデータ項目について要求仕様記述がなされた要求仕様を格納する要求仕様ファイルと、実行モデル生成処理手段の処理で使用するテンプレート名およびテンプレートを格納するテンプレートファイルと、実行モデル生成処理手段の処理で使用する要求仕様記述名とモデル検査ツールSPINのモデ
ル記述言語のコードに記述する文字列との対応を辞書として格納する変換辞書ファイルと、検証処理手段の処理で使用する検証閾値を格納する検証ファイルと、実行モデル生成処理手段の処理によって自動生成された実行モデルを格納する実行モデルファイルと、を有し、ユーザ指示により起動され、前記要求仕様ファイルに格納された要求仕様の中から実行モデル生成に関するデータ項目を抽出し、抽出した前記データ項目について前記テンプレートファイルに格納されたテンプレートおよび前記変換辞書ファイルに格納された辞書データを用いて実行モデルを自動的に生成する実行モデル生成処理手段と、前記実行モデルファイルに格納された前記実行モデルについて前記要求仕様から必要なデータ項目を参照して該必要なデータ項目が前記実行モデルの所定位置に記述されているかを検証し、またモデル検査ツールSPINを起動して前記実行モデルに係るシンタックス・チェックを実行する検証処理手段と、を備えていることを特徴とする。
【発明の効果】
【０００８】
本発明によれば、要求仕様からモデル検査ツールSPINのモデル記述言語Promelaの実行モデルを自動的に生成することにより、早期の段階で要求仕様の検証を行うことで要求仕様の抜け・漏れ、誤りを抽出し手戻り作業を削減し、品質の高いソフトウェアを開発することができる。
【０００９】
また、要求仕様からモデル検査ツールSPINのモデル記述言語Promelaの実行モデルを自動的に生成する過程でイベントフローのループやイベントの遷移元が無いなどの間違いがないかを早期の段階で検証することで要求仕様の抜け・漏れ、誤りを抽出し手戻り作業を削減し、品質の高いソフトウェアを開発することができる。
【発明を実施するための最良の形態】
【００１０】
以下、本発明の実施の形態を、図面を参照しながら説明する。
図１は、本発明要求仕様自動検証に係るシステム構成概要を示す図である。図１に示すシステム構成は、本発明要求仕様自動検証を実現する上でのハードウェア環境を概略的に示したもので、本発明要求仕様自動検証に係るシステム構成は、クライアントとサーバとがネットワークで結合されるクライアントサーバシステムを用いて実現される例について説明するが、他のシステム構成であってもよい。
【００１１】
クライアント11はネットワーク10経由でサーバ１に繋がれ、周知のクライアントが備えるコンピュータハードウェア資源を用いてサーバ１に対する処理の起動やデータの表示(ダウンロードを含む)、データの設定(アップロードを含む)を行う。ネットワーク10はクライアント11とサーバ１とを連携するもので、ＬＡＮ、公衆網（インターネットを含む）など、周知のネットワーク技術を用いることができる。サーバ１のコンピュータハードウェア資源は当業者に周知のコンピュータ技術によって実現されているもので、例えばコンピュータハードウェア資源としてＣＰＵ、記憶装置(ＲＯＭ，ＲＡＭ，ＨＤＤを含む)、入出力装置(通信Ｉ/Ｆ，ディスプレイ，プリンタ，マウス，キーボードなどを含む)などを備えている。なお本発明要求仕様自動検証に係るハードウェア構成については後述する各種処理部の動作および生成処理部の動作において詳しく説明する。
【００１２】
図１では、本発明要求仕様自動検証に係る各種ファイルのデータ構造を概略的に説明している。各種ファイルのデータ構造は、本発明要求仕様自動検証に係る各種ファイルの全体構成を理解しやすくするために記載しているものである。そして各種ファイルは、上述したサーバ１の記憶装置(ＲＯＭ，ＲＡＭ，ＨＤＤを含む)に保存され、サーバ１のＣＰＵによってアクセス可能にされる。
【００１３】
図１に示す要求仕様ファイル２は、要求仕様記述がなされたデータを格納するものである。要求仕様の記述をなすために、図６のデータの流れ(１)に示すようにクライアント11
の要求仕様記述ユーザがサーバ１にログインし、サーバ１から要求仕様記述に係るデータなどをダウンロードする。クライアント11の要求仕様記述ユーザは、表示画面上において必要なデータを入力する。本発明では要求仕様記述について以下に示すような所定の規約を設けている。すなわち、本発明の要求仕様記述では、要求仕様の機能要件および非機能要件をソフトウェア開発従事者に周知のＵＭＬ(Ｕnified Ｍodeling Ｌanguage：統合モデリング言語)のユースケース図を用いたユースケース記述を基本とし、さらに要求仕様の項目の漏れ・抜けや曖昧さをなくすため形式的仕様記述言語であるソフトウェア開発従事者に周知のVDM-SL（Vienna Development Method Specification Language)の構文に基づいた項とイベントの遷移を明確にした項を追加する。なお、VDM-SLは、ISO_IEC_13817-1として標準化されているものである。
【００１４】
ユースケース記述による項目名の各項にはVDM-SLの「状態定義」構文に対応した項を設ける。すなわち
state definition
invariant
initialization
のVDM-SLの「状態定義」構文について
state definitionを「概要」
invariantを「不変条件」
initializationを「初期条件」
に対応付ける。
【００１５】
また各項目に共通するVDM-SLの「型定義」構文に対応した項を設ける。
type definition= identifier, '=', type
identifier を「外部アクセス」に対応付ける。
【００１６】
またユースケース記述によるイベントフローの各イベントには形式的仕様記述言語であるVDM-SLの「操作定義」構文に対応した項を設ける。すなわち
operation definition=identifier, parameter types
externals,
'pre', expression,
'post', expression
のVDM-SLの「操作定義」構文について
identifierを「イベント」
parameter typesを「入力データ」
externalsを「外部データ」
'pre', expressionを「事前条件」
'post', expressionを「事後条件」
に対応付ける。
【００１７】
さらに、ユースケース記述によるイベントの遷移を明確にするため「次のイベント」の項を設け、遷移先のイベント番号を記載する。これにより要求仕様の項目のイベントフローが明確になり、要求仕様をモデル検査ツールSPINのモデル記述言語Promelaの実行モデル(コード)を自動生成する過程でイベントフローのループやイベントの遷移元が無いなどの間違いがないかを早期の段階で検証することができる。
【００１８】
また、VDM-SLの「型定義」に相当する「外部アクセス」を後述する変換辞書ファイルで定義することにより、「外部アクセス」の定義が一貫して各イベントで使われているかを早期の段階で検証することができる。
【００１９】
このようにしてクライアント11の要求仕様記述ユーザによって要求仕様記述がなされたデータをサーバ１にアップロードして要求仕様ファイル２に要求仕様記述がなされたデータを要求仕様として格納する。
【００２０】
図１に示す要求仕様ファイル２において、要求仕様ファイル２のファイルの項目として下記がある。
仕様名・版数 201：仕様名は仕様記述の対象としている仕様名を格納する。仕様記述に対して一意に設定する。また版数は仕様名の版を識別する数値を格納する。
【００２１】
項目名202：ユースケースのイベントに対応した機能要求または非機能要求の項目名を格納する。
概要203：機能要求または非機能要求の概要を格納する。
【００２２】
イベント204：当該項目が起動されるイベント名を格納する。
次のイベント205：当該項目の次に起動されるイベント番号を格納する。次のイベントがない場合は「終了」と記載する。またイベント番号の後ろに（    ）で「備考」を格納してもよい。
【００２３】
外部アクセス206：外部へのアクセス対象のデータ名を列記する。
不変条件207：当該項目の各イベント内で変化しない条件。
初期条件208：当該項目が成立するために初期に必要とする条件。
【００２４】
イベントフロー209：当該項目内での一連のイベントの系列。基本系列、代替系列、例外系列からなる。
基本系列210：当該項目内での基本的なイベントの系列。
【００２５】
イベント番号・イベント211：イベントを識別するための当該項目内での一意の番号と当該イベントの説明を格納する。
事前条件212：当該イベントが成立するために事前に必要とする条件。
【００２６】
入力データ・境界値213：当該イベントの入力データと当該入力データのデータ値がとる値の範囲を格納する。
事後条件214：当該イベントの処理が終了した時にとる条件。
【００２７】
外部データ・境界値215：当該イベントの外部にアクセスするデータと当該データのデータ値がとる値の範囲を格納する。
次のイベント216：当該イベントの次に起動されるイベント番号を格納する。次のイベントがない場合は「終了」と記載する。またイベント番号の後ろに（    ）で「備考」を格納してもよい。
【００２８】
代替系列217：当該項目内での基本系列に代替するイベントの系列。代替系列も基本系列と同様にイベント番号・イベント、事前条件、入力データ・境界値、事後条件、外部データ・境界値、次のイベントのデータを持つ。
【００２９】
例外系列218：当該項目内での異常が発生した場合など例外イベントの系列。例外系列も基本系列と同様にイベント番号・イベント、事前条件、入力データ・境界値、事後条件、外部データ・境界値、次のイベントのデータを持つ。
【００３０】
図２は、本発明の実施形態に係る要求仕様ファイル２に格納された要求仕様のデータ構造例を示す図である。事例は要求仕様項目名が“入金”についての機能要求項目の例であ
り、図示していないが要求仕様ファイル２にはこれ以外の要求仕様項目名、例えば“出金”についての機能要求項目などについても要求仕様記述がなされた要求仕様が格納されている。さらには図示していないが、非機能要求項目などについても要求仕様が記述される。なお後述する検証処理部８およびシミュレーション実行処理部９では要求仕様項目、版数が指定された要求仕様についてそれぞれ処理が行われるものである。
【００３１】
実行モデルファイル３は、後述する実行モデル生成処理部７の処理フローにしたがって要求仕様ファイル２に格納された要求仕様から実行モデル生成に関するデータ項目をデータの流れ(２)に示すように抽出し、またテンプレートファイル４からデータの流れ(３)に示すようにテンプレートを参照し、さらに変換辞書ファイル５からデータの流れ(４)に示すように実行モデル生成に関して変換を要する項目データについて辞書を参照して自動的に生成したモデル検査ツールSPINのモデル記述言語Promelaのコード(実行モデル)を格納する。実行モデルを自動生成してデータを実行モデルファイル３に格納するために、クライアント11の実行モデル生成指示ユーザは、サーバ１にログインし、サーバ１内において後述する実行モデル生成処理部７の起動を指示する。図６に示す実行モデル生成処理部７は、要求仕様記述がなされた要求仕様ファイル２の要求仕様からデータの流れ(２)に示すように実行モデル生成に関する項目データを抽出するとともに、テンプレートファイル４からデータの流れ(３)に示すように実行モデル生成に必要なテンプレートを参照し、さらに変換辞書ファイル５からデータの流れ(４)に示すように実行モデル生成に関し変換を要する項目データについて辞書を参照し、実行モデルを自動生成(これについては後述する)し、データの流れ(５)に示すように実行モデルファイル３に生成したデータを格納する。
【００３２】
図１に示す実行モデルファイル３において、実行モデルファイル３のファイルの項目として下記がある。すなわち、
仕様名・版数 301：要求仕様ファイル２に格納された要求仕様の仕様名・版数に対応して、仕様名にはテスト仕様名を格納し、また版数にはテスト仕様名の版を識別する番号を格納する。
【００３３】
実行モデル302：自動生成したモデル検査ツールSPINのモデル記述言語Promelaのコードを格納する。
図３は、本発明の実施形態に係る実行モデルファイル３に格納されたモデル検査ツールSPINのモデル記述言語Promelaの実行モデル例を示す図である。
【００３４】
テンプレートファイル４は、実行モデル生成処理部７の処理において使用するモデル検査ツールSPINのモデル記述言語Promelaに係るテンプレートを格納するものであり、当該テンプレートに基づいてモデル記述言語Promelaの実行モデルを生成する。
【００３５】
図１に示すテンプレートファイル４において、テンプレートファイル４のファイルの項目として下記がある。すなわち、
テンプレート名401：テンプレートの名称を格納する。
【００３６】
テンプレート402：テンプレート種別番号とそれに対応するモデル記述言語Promelaコード化されたテンプレートを格納する。
図４は、本発明の実施形態に係るテンプレートファイル４に格納された第１のテンプレート〜第５のテンプレートの例を示す図である。
【００３７】
変換辞書ファイル５は、実行モデル生成処理部７の処理において使用する要求仕様記述名とモデル検査ツールSPINのモデル記述言語Promelaのコードに記述する文字列との対応を辞書として格納する。
【００３８】
図１に示す変換辞書ファイル５において、変換辞書ファイル５のファイルの項目として下記がある。すなわち、
要求仕様記述名501：要求仕様ファイル２に記載されている名称を格納する。
【００３９】
実行モデル記述名502：実行モデルの実行コードに記載する名称を格納する。
コメント記述名503：実行モデルのコメントに記載する名称を格納する。
図５は、本発明の実施形態に係る変換辞書ファイル５に格納された辞書のデータ構造例を示す図である。なお図５に示す辞書のデータ構造例では、上記コメント記述名503に相当する記述は略されている。
【００４０】
検証ファイル６は、後述する検証処理部８の処理フローで使用するデータを格納する。すなわち図１に示す検証ファイル６において、検証ファイル６のファイルの項目としては下記がある。
【００４１】
検証閾値601：実行モデル生成処理部７が起動されてから検証処理部８が起動するまでの時間を格納する。
実行モデル生成処理部７は、上述した図１のサーバ１内において実現される機能実現手段であって、サーバ１内におけるＣＰＵの起動に伴い記憶装置（ＲＯＭ，ＨＤＤ）に格納されているプログラムを読み込み、ＣＰＵがプログラム制御によって動作し、クライアント11とのデータのやりとりの外、サーバ１内の記憶装置（ＲＡＭ，ＨＤＤ）に展開されるファイルへのリード/ライト機能、当該ファイルに対するファイル編集機能、入出力装置へのデータ出力機能などを用いて実現される。このようなコンピュータのハードウェア資源を用いて実現される諸機能は図解せずとも当業者に広く知られているものでここではその説明を省略する。クライアント11の実行モデル生成指示ユーザはサーバ１に対して実行モデル生成処理部７の起動を指示し、これを受けて図６に示す実行モデル生成処理部７は、所定プログラムを動作させ図７Ａ，図７Ｂに示す実行モデル生成処理部７の処理フローにしたがって要求仕様記述がなされた要求仕様ファイル２の要求仕様からデータの流れ(２)に示すように実行モデル生成に関する項目データを抽出して、データの流れ(３)，(４)に示すようにテンプレートファイル４および変換辞書ファイル５を参照して実行モデルを生成し、生成した実行モデルをデータの流れ(５)に示すように実行モデルファイル３に格納する。具体的な実行モデル生成処理部７の処理フローを図７Ａ，図７Ｂに示す。図７Ａ，図７Ｂの処理フローについては後述する。
【００４２】
検証処理部８は、上述した図１のサーバ１内において実現される機能実現手段であって、サーバ１内におけるＣＰＵの起動に伴い記憶装置（ＲＯＭ，ＨＤＤ）に格納されているプログラムを読み込み、ＣＰＵがプログラム制御によって動作し、クライアント11とのデータのやりとりの外、サーバ１内の記憶装置（ＲＡＭ，ＨＤＤ）に展開されるファイルへのリード/ライト機能、当該ファイルに対するファイル編集機能、入出力装置へのデータ出力機能などを用いて実現される。このようなコンピュータのハードウェア資源を用いて実現される諸機能は図解せずとも当業者に広く知られているものでここではその説明を省略する。そして上記した実行モデル生成処理部７が起動した後、検証処理部８が起動するまでの所定時間を上記クライアント11のユーザから実行モデル生成処理部７に指示し、検証処理部８は実行モデル生成処理部７で受けた当該所定時間に係るデータをデータの流れ(６)、(７)に示すように検証ファイル６の検証閾値として保存するとともに当該所定時間後に検証処理部８が起動され、図６に示す検証処理部８は、図８に示す検証処理部８の処理フローにしたがって実行モデルファイル３に格納された実行コードについて要求仕様ファイル２の要求仕様からデータの流れ(９)に示すように必要なデータを参照しおよび検証ファイル６からデータの流れ(７)に示すように必要なデータを参照して検証し更にモデル検査ツールSPINを起動して当該実行コードに係るSyntax checkを実行する。なおモデル検査ツールSPINは、ソフトウェア開発に従事する者には広く知られている検査ツールで、本
発明ではサーバ１内の上記記憶装置（ＲＯＭ，ＨＤＤ）にあらかじめプログラム実装され検証処理部８の起動後はＣＰＵの制御の下でいつでもプログラムがrunするようにされている。具体的な検証処理部８の処理フローを図８に示す。図８の処理フローについては後述する。
【００４３】
シミュレーション実行処理部９は、上述した図１のサーバ１内において実現される機能実現手段であって、サーバ１内におけるＣＰＵの起動に伴い記憶装置（ＲＯＭ，ＨＤＤ）に格納されているプログラムを読み込み、ＣＰＵがプログラム制御によって動作し、クライアント11とのデータのやりとりの外、サーバ１内の記憶装置（ＲＡＭ，ＨＤＤ）に展開されるファイルへのリード/ライト機能、当該ファイルに対するファイル編集機能、入出力装置へのデータ出力機能などを用いて実現される。このようなコンピュータのハードウェア資源を用いて実現される諸機能は図解せずとも当業者に広く知られているものでここではその説明を省略する。クライアント11のシミュレーション実行指示ユーザはデータの流れ(10)に示すようにサーバ１に対してシミュレーション実行処理部９の起動と指定時間後の停止とを指示し、これを受けて図６に示すシミュレーション実行処理部９は、図９に示すシミュレーション実行処理部９の処理フローにしたがってデータの流れ(11)に示すように実行モデルファイル３に格納されている実行コードを読み込み、モデル検証ツールSPINを動作させてSimulation(シミュレーション)を実行し、そして指定時間後に停止させ、その後、データの流れ(12)，(13)に示すようにSimulation実行結果としてのシミュレーションチャート(図１１参照)、シミュレーショントレース(図１２参照)を出力する。なおモデル検査ツールSPINは、ソフトウェア開発に従事する者には広く知られている検査ツールで、本発明ではサーバ１内の上記記憶装置（ＲＯＭ，ＨＤＤ）にあらかじめプログラム実装されユーザのシミュレーション実行指示によりＣＰＵの制御の下でプログラムがrunするようにされている。またSimulation実行結果として出力されるシミュレーションチャートは、上記した非特許文献２にも開示されているように当業者によく知られているものである。具体的なシミュレーション実行処理部９の処理フローを図９に示す。図９の処理フローについては後述する。
【００４４】
図６は、図１に示したサーバ１内の各種ファイル、各種処理部および生成処理部並びにクライアント11を活用して本発明要求仕様自動検証を実現するための相互の結合関係およびデータの流れを示す相関図である。図６に示したそれぞれのブロックは、図１に示したサーバ１内において機能を実現するための機能ブロックであり、相互の結合関係およびデータの流れを図示番号とともに矢視線で示す。なお処理内容の詳細については後述する。
【００４５】
相互の結合関係およびデータの流れについて図６を用いて簡単に説明する。クライアントサーバシステムにおいてクライアント11がサーバ１にログインする。次いでサーバ１に対してどのような処理または生成処理を成そうとするのかの指示をクライアント11のユーザから出す。なお図６ではクライアント11を代表して一つだけ表示しているもので、図１に示すようにクライアント11はサーバ１に対して複数存在する。いま、要求仕様を記述するための指示が出されたとすると、これに応じて要求仕様の記述に係るデータのダウンロードが行われてクライアント11の画面に表示される。データの流れ(１)に示すようにクライアント11のユーザは要求仕様の記述画面で必要な項目への記述を行って記述がなされた要求仕様をサーバ１にアップロードする。要求仕様の記述にあたっては、上述した本発明が独自に採用する仕様記述の規約にしたがって実行する。
【００４６】
実行モデル生成処理部７は、クライアント11のユーザからの指示により起動し、図７Ａ，図７Ｂに示す処理フローにしたがって要求仕様ファイル２の要求仕様からデータの流れ(２)に示すように実行モデル生成に関する項目データを抽出するとともに、テンプレートファイル４からデータの流れ(３)に示すように実行モデル生成に必要なテンプレートを参照し、さらに変換辞書ファイル５からデータの流れ(４)に示すように実行モデル生成に関
し変換を要する項目データについて辞書を参照し、実行モデルを自動生成(これについては後述する)し、データの流れ(５)に示すように実行モデルファイル３に生成したデータを格納する。
【００４７】
上記した実行モデル生成処理部７が起動した後、検証処理部８が起動するまでの所定時間を上記クライアント11のユーザから実行モデル生成処理部７に指示し、検証処理部８は実行モデル生成処理部７で受けた当該所定時間に係るデータをデータの流れ(６)、(７)に示すように検証ファイル６の検証閾値として保存する。そして検証処理部８は当該所定時間後に実行モデル生成処理部７から起動され、図８に示す検証処理部８の処理フローにしたがってまずデータの流れ(７)に示すように検証ファイル６の検証閾値が読み出され当該検証閾値内に上記実行モデル生成処理部７の処理が終了したかを検証し、次いで実行モデルファイル３からデータの流れ(８)に示すように検証処理に必要なデータを抽出するとともに要求仕様ファイル２からもデータの流れ(９)に示すように検証処理部８の検証処理に必要なデータを抽出して検証を行う。またモデル検査ツールSPINを起動して当該実行コードに係るSyntax check(構文チェック)を実行する。
【００４８】
シミュレーション実行処理部９は、クライアント11からのデータの流れ(10)に示す起動指示および指定時間後に停止の指示により起動し、図９に示すシミュレーション実行処理部９の処理フローにしたがってデータの流れ(11)に示すように実行モデルファイル３に格納されている実行コードを読み込み、モデル検証ツールSPINを動作させてSimulationを実行し、そして指定時間後に停止させ、その後、データの流れ(12)，(13)に示すようにSimulation実行結果としてのシミュレーションチャート(図１１参照)、またはシミュレーショントレース(図１２参照)を出力する。
【００４９】
図７Ａ，図７Ｂは、本発明の実施形態に係る実行モデル生成処理部７の実行モデル生成処理フローを示す図である。同図において、ステップはSと略記する。図７Ａにおいて、
S1  要求仕様ファイル２の要求仕様から外部アクセスを参照する。またテンプレートファイル４の第１のテンプレートを実行モデルファイル３の当該仕様名  版数に相当する実行モデルにコピーする。そして第１のテンプレートの“A”に変換辞書ファイル５で変換した外部アクセスの文字列を格納し、第１のテンプレートのコメントの“B”に変換辞書ファイル５で変換した外部アクセスの文字列を格納する。この際、外部アクセスが複数ある場合は、当該数分第１のテンプレートに示す“chan”の行を追加し同様の処理をする。
【００５０】
S2  要求仕様ファイル２の要求仕様から項目名を参照する。またテンプレートファイル４の第２のテンプレートを上記ステップS1で生成した実行モデルの後ろに追加する。そして第２のテンプレートの“A”に変換辞書ファイル５で変換した項目名の文字列を格納し、第２のテンプレートのコメントの“B”に変換辞書ファイル５で変換した項目名の文字列を格納する。この際、項目名が複数ある場合は、当該数分第２のテンプレートを追加し同様の処理をする。
【００５１】
S3  要求仕様ファイル２の要求仕様から外部アクセスを参照する。またテンプレートファイル４の第３のテンプレートを上記ステップS2で生成した実行モデルの後ろに追加する。そして第３のテンプレートの“A”に変換辞書ファイル５で変換した外部アクセスの文字列を格納し、第３のテンプレートのコメントの“B”に変換辞書ファイル５で変換した外部アクセスの文字列を格納する。この際、外部アクセスが複数ある場合は、第３のテンプレートを追加し同様の処理をする。
【００５２】
S4  上記ステップS2で生成した実行モデルを参照する。次いで次のイベント（要求仕様ファイル２の要求仕様の項目名の３項目後ろ）を参照する。次のイベントの数−１の数分第２のテンプレートの“od”の手前に第５のテンプレートを追加する。そして第２のテン
プレートの“C”に次のイベントの外部データについて、変換辞書ファイル５で変換した外部データの文字列を格納し、第２のテンプレートのコメントの“D”に変換辞書ファイル５で変換した外部データの文字列を格納する。この際、外部データが複数ある場合は当該数分
C!get
C!put
の行を追加し同様の処理をする。また、外部データがない場合は
C!get
C!put
を削除し
skip
と記載する。
【００５３】
第５のテンプレートの“A”に当該イベントの外部データについて、変換辞書ファイル５で変換した外部データの文字列を格納し、第５のテンプレートのコメントの“B”に変換辞書ファイル５で変換した外部データの文字列を格納する。外部データが複数ある場合は当該数分
A!get
A!put
の行を追加し同様の処理をする。外部データがない場合は
A!get
A!put
を削除し
skip
と記載する。
【００５４】
図７Ｂにおいて、
S5  上記ステップS4で生成した実行モデルを参照する。そして上記ステップS4で生成したイベントについて、当該イベントの次のイベントを参照する。次のイベントが有る場合::  またはodの手前に第４のテンプレートを追加する。この場合字下げをして追加する。そして第４のテンプレートの“A”に次のイベントの外部データについて、変換辞書ファイル５で変換した外部データの文字列を格納し、第４のテンプレートのコメントの“B”に変換辞書ファイル５で変換した外部データの文字列を格納する。この際、外部データが複数ある場合は当該数分
A!get
A!put
の行を追加し同様の処理をする。外部データがない場合は
A!get
A!put
を削除し
skip
と記載する。
【００５５】
S6  次のイベントが複数有る場合は、次のイベントの数−１の数分第４のテンプレートの“od”の手前に第５のテンプレートを追加する。そして第５のテンプレートの“A”に当該イベントの外部データについて、変換辞書ファイル５で変換した外部データの文字列を格納し、第５のテンプレートのコメントの“”Bに変換辞書ファイル５で変換した外部データの文字列を格納する。外部データが複数ある場合は当該数分
A!get
A!put
の行を追加し同様の処理をする。外部データがない場合は
A!get
A!put
を削除し
skip
と記載する。
【００５６】
S7  上記ステップS5及び上記ステップS6で生成した実行モデルを参照する。上記ステップS5及び上記ステップS6で生成したイベントについて、当該イベントの次のイベントを参照する。そして階層を深くして同様に上記ステップS5及び上記ステップS6の処理を繰り返す。更に当該イベントの次のイベントがなくなるまで（「終了」を検出するまで）上記ステップS5及び上記ステップS6の処理を繰り返す。この処理の理解を助けるため図１０に図２に示した要求仕様ファイル例に対応するイベントフローを参考として示しておく。図１０において矩形は「イベント」を表し、菱形は「分岐」を表している。
【００５７】
S8  上記ステップS1〜S7の処理中に変換辞書ファイル５で変換エラーがでた場合はエラーを文字列とともに出力する。例えば、
変換エラー  不明紙幣収納庫  実行モデル記述名なし
と出力する。
【００５８】
図８は、本発明の実施形態に係る検証処理部８の検証処理フローを示す図である。検証処理部８が検証処理を始めるにあたって、当該検証処理は、実行モデル生成処理部７が起動した後の指定時間後に起動するようにユーザにより指定され、指定された指定時間は図６のデータの流れ(6)に示すように検証ファイル６の検証閾値に格納され、さらに実行モデル生成処理部７から当該指定時間後に起動され、起動と同時に実行モデル生成処理部６から仕様名  版数が通知されるようになっている。同図において、ステップはSと略記する。図８において、
S11  検証ファイル６の検証閾値を読み出し、当該検証閾値で実行モデル生成処理部７が終了していない場合は、ループしていると判断して検証エラーを出力し、実行モデル生成処理部７を停止させる。例えば、
検証エラー  実行モデル検証処理部  ループ
と出力する。なお不具合箇所は実行モデルのコードの生成状況で確認できる。
【００５９】
S12  生成された実行モデルファイル３の当該仕様名  版数  の実行モデルを参照し、要求仕様ファイル２の当該仕様名  版数  の要求仕様に係る項目名のイベント番号が実行モデルの当該実行モデルのコメントに記述されているかを確認し、記述されていない場合は検証エラーをイベント番号とともに出力する。例えば、
検証エラー  例外系列１  遷移元なし
と出力する。
【００６０】
S13  モデル検査ツールSPINのRun Syntax Check を起動し、外部アクセスと外部データの矛盾などのエラーが検出されたときはSyntax Errorとして出力する。
図９は、本発明の実施形態に係るシミュレーション実行処理部９のシミュレーション実行処理フローを示す図である。同図において、ステップはSと略記する。図９において、
S21  実行モデルファイル３の当該仕様名  版数を指定する。
【００６１】
S22  モデル検査ツールSPINのRun Simulation を起動する。
S23  一定時間後Simulation を停止する。
S24  Simulation-chart ; Simulation-traceを出力する。
【００６２】
シミュレーション結果の出力例として、図１１にシミュレーションチャート(Simulation-chart)を示し、また図１２にシミュレーショントレース(Simulation-trace)を示す。
このように本発明は、要求仕様をモデル検査ツールSPINのモデル記述言語Promelaのコード(実行モデル)を自動生成することで、モデル検査ツールSPINを動作させSyntax check
およびSimulationが可能となる。これにより「外部アクセス」と「外部データ」の矛盾などのエラー検出および、外部アクセスへの各要求仕様イベントのアクセス状況により不具合箇所を確認でき、これらにより早期に要求仕様の検証を行うことで要求仕様の抜け・漏れ、誤りを抽出し手戻り作業を削減し、品質の高いソフトウェアを開発することが可能となる。
【００６３】
また上記においてさらに、図４に示すテンプレートを補充し、且つLTL（Linear Temporal Logic ：線形時相論理)の検査式をモデル検査ツールSPINに入力して、SPINのモデル検査を実行すれば、外部アクセスの項目名間での競合の有無の検査をすることもできる。
【００６４】
この場合、図４に示すテンプレートに対して追加するテンプレートは、
図４に示す第１のテンプレートを
mtype={get,put};
chan A=[1]of {mtype};   /* B */
mtype state_AC;
とする。Cは変換辞書ファイル５で変換した項目名の文字列を格納する。ACは外部アクセスと項目名の組合せについて展開する。
【００６５】
また図４に示す第２のテンプレートを
active proctype A()    /*B */
{
state_AC=idle;
do
::C!get; /*D */
state_AC=critical;
C!put;
state_AC=idle;
od
}
とする。
【００６６】
また図４に示す第４のテンプレートを
do
::A!get; /*B */
state_AC=critical;
A!put;
state_AC=idle;
od
とする。Cは変換辞書ファイル５で変換した項目名の文字列を格納する。
【００６７】
また図４に示す第５のテンプレートを
::A!get; /*B */
state_AC=critical;
A!put;
state_AC=idle;
とする。Cは変換辞書ファイル５で変換した項目名の文字列を格納する。
【００６８】
そして実行モデル生成処理部７に上記において追加したテンプレートのA〜Cを埋める処理を追加する。
またLTL（Linear Temporal Logic）の検査式として「複数の「項目名」に対応するプロセスが同時に同一外部アクセスのクリティカル領域にいることはない」との条件で検査する。すなわち、
!<>((q11)&&(q12)&& ・・・&&(q1n)
・・・・
!<>((qk1)&&(qk2)&&  ・・・&&(qkn)
を記述する。
ここで
qkn,“state_kn==critical”
ｋは外部アクセスの通番、nは項目名の通番
である。ただしkをアクセスしていないnは除外する。
【００６９】
このように本発明は、自動生成されたモデル検査ツールSPINのモデル記述言語Promelaのコード(実行モデル)に検査したい条件を追記し、SPINのRun Verificationを実行することで状態を網羅的に検証することができる。
【図面の簡単な説明】
【００７０】
【図１】本発明要求仕様自動検証に係るシステム構成概要を示す図である。
【図２】本発明の実施形態に係る要求仕様ファイルに格納された要求仕様のデータ構造例を示す図である。
【図３】本発明の実施形態に係る実行モデルファイルに格納されたモデル検査ツールSPINのモデル記述言語Promelaの実行モデル例を示す図である。
【図４】本発明の実施形態に係るテンプレートファイルに格納された第１のテンプレート〜第５のテンプレートの例を示す図である。
【図５】本発明の実施形態に係る変換辞書ファイルに格納された辞書のデータ構造例を示す図である。
【図６】本発明の実施形態に係るサーバ内の各種ファイル、各種処理部、生成処理部およびクライアントの相互の結合関係およびデータの流れを示す相関図である。
【図７Ａ】本発明の実施形態に係る実行モデル生成処理部の実行モデル生成処理フローを示す図である。
【図７Ｂ】本発明の実施形態に係る実行モデル生成処理部の実行モデル生成処理フローを示す図である。
【図８】本発明の実施形態に係る検証処理部の検証処理フローを示す図である。
【図９】本発明の実施形態に係るシミュレーション実行処理部のシミュレーション実行処理フローを示す図である。
【図１０】図２に示した要求仕様ファイル例に対応するイベントフローを示す図である。
【図１１】シミュレーション結果の出力であるシミュレーションチャートの例を示す図である。
【図１２】シミュレーション結果の出力であるシミュレーショントレースの例を示す図である。
【符号の説明】
【００７１】
１      サーバ
２      要求仕様ファイル
３      実行モデルファイル
４      テンプレートファイル
５      変換辞書ファイル
６      検証ファイル
７      実行モデル生成処理部
８      検証処理部
９      シミュレーション実行処理部
１０      ネットワーク
１１      クライアント
【図１】
2008305079.tif 000003
【図２】
2008305079.tif 000004
【図３】
2008305079.tif 000005
【図４】
2008305079.tif 000006
【図５】
2008305079.tif 000007
【図６】
2008305079.tif 000008
【図７Ａ】
2008305079.tif 000009
【図７Ｂ】
2008305079.tif 000010
【図８】
2008305079.tif 000011
【図９】
2008305079.tif 000012
【図１０】
2008305079.tif 000013
【図１１】
2008305079.tif 000014
【図１２】
2008305079.tif 000015