(57)【要約】  【課題】  モデル記述言語の習得を必要とせずに、動作仕様からモデル検査プログラムを生成でき、より好ましくは、検証済みの動作仕様に応じたソフトウェアを自動的に生成することも可能なモデル検査支援装置を提供する。  【解決手段】  モデル検査支援装置は、ソフトウェアの動作仕様を、変数の状態遷移関係で表した論理記述として入力する仕様入力部３と、モデル検査プログラムの雛型を格納したモデル記述言語辞書６と、仕様入力部３へ入力された論理記述から前記動作仕様の論理構造を抽出し、抽出された論理構造とモデル記述言語辞書６の雛型とを用いて、モデル検査プログラムを作成する翻訳部４とを備え、翻訳部４で作成されたモデル検査プログラムをモデル検査器１０へ出力する。【選択図】  図１
2007011605.tif 000002
【特許請求の範囲】
【請求項１】
ソフトウェアの動作仕様を、変数の状態遷移関係で表した論理記述として入力する仕様入力部と、
モデル検査プログラムの雛型を格納したモデル記述言語辞書記憶部と、
前記仕様入力部へ入力された論理記述から前記動作仕様の論理構造を抽出し、抽出された論理構造と前記モデル記述言語辞書記憶部の前記雛型とを用いて、モデル検査プログラムを作成する翻訳部とを備えたことを特徴とする、ソフトウェア動作仕様のモデル検査支援装置。
【請求項２】
前記仕様入力部が、前記変数の状態遷移関係を図形表現として入力し、
前記翻訳部は、前記仕様入力部に入力された図形表現から動作仕様の論理構造を抽出する、請求項１に記載のモデル検査支援装置。
【請求項３】
前記翻訳部により抽出された動作仕様の論理構造を記憶する論理構造記憶部と、
開発言語プログラムの雛型を格納した開発言語辞書記憶部と、
前記論理構造記憶部に記憶された論理構造と、前記開発言語辞書記憶部の前記雛型とを用いて、開発言語によるプログラムを作成するプログラム作成部とを備えた、請求項１に記載のモデル検査支援装置。
【請求項４】
請求項１〜３のいずれか一項に記載のモデル検査支援装置と、
前記モデル検査支援装置により生成されたモデル検査プログラムのモデル検査を行うモデル検査器とを備えたことを特徴とするモデル検査システム。
【請求項５】
コンピュータにソフトウェア動作仕様のモデル検査支援処理を実行させるモデル検査支援プログラムであって、
ソフトウェアの動作仕様を、変数の状態遷移関係で表した論理記述として入力する仕様入力処理と、
前記仕様入力処理で入力された論理記述から前記動作仕様の論理構造を抽出し、抽出された論理構造と、モデル記述言語辞書記憶部から取得したモデル検査プログラムの雛型とを用いて、モデル検査プログラムを作成する翻訳処理とを、コンピュータに実行させることを特徴とするモデル検査支援プログラム。
【請求項６】
前記仕様入力処理において、前記変数の状態遷移関係を図形表現として入力し、
前記翻訳処理において、前記仕様入力処理で入力された図形表現から動作仕様の論理構造を抽出する、請求項５に記載のモデル検査支援プログラム。
【請求項７】
前記翻訳処理により抽出された動作仕様の論理構造を記憶した論理構造記憶部と、
開発言語プログラムの雛型を格納した開発言語辞書記憶部とを参照し、
前記論理構造記憶部から取得した論理構造と、前記開発言語辞書記憶部から取得した前記雛型とを用いて、開発言語によるプログラムを作成するプログラム作成処理をコンピュータに実行させる、請求項５または６に記載のモデル検査支援プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェア動作仕様が、自己矛盾、不安定性、想定外動作等の不具合を含まず、正しく記述されていることを数理的に検証する装置に関し、特に、動作仕様を有限状態遷移系に変換してモデル検査法を適用する検証装置に関する。
【背景技術】
【０００２】
従来、ソフトウェア開発においては、動作仕様を経験者が査読することにより、不具合の有無を確認している。このため、不具合が完全に検出できないままにソフトウェアの設計・開発が行われることもあり、完成後の検査により不具合を発見して手直しする必要があった。従って、ソフトウェアの信頼度が十分に確保できず、また、手直しが必要なために開発効率が低下する、といった問題があった。
【０００３】
そこで、ソフトウェアの動作仕様を数理的に検証するためのモデル検査法が知られている。モデル検査法は、ソフトウェア動作仕様を状態遷移系として記述したモデル検査プログラムが、検査項目として入力された時相論理式を満足しているかどうかを数理的に検証するものであり（例えば特許文献１参照）、ソフトウェアの動作仕様に潜在する自己矛盾、不安定性、想定外動作等の不具合検出にも適用可能である（非特許文献１参照）。
【０００４】
従来、ソフトウェア動作仕様へモデル検査器を適用する際は、動作仕様から人手により図表を作成して論理構造を抽出し、モデル記述言語によりモデル検査プログラムを作成している（例えば非特許文献２参照）。
【特許文献１】特開平１０−３０１９６３号
【非特許文献１】早水、篠崎、高橋、渡邊、モデル検査器を用いた自動検針システムの仕様検証、産業技術総合研究所算譜科学グループ研究速報、ＡＩＳＴ−ＰＳ−２００３−００５
【非特許文献２】寺田、土屋、菊野、記号モデル検査を用いたステートチャートの検証、電子情報通信学会技術報告、ＳＳ９８−４１（１９９９−０１）
【発明の開示】
【発明が解決しようとする課題】
【０００５】
しかしながら、上記従来のモデル検査は、ソフトウェア開発言語と異質のモデル記述言語の習得が必要であることから、研究目的では実施されているが、実際のソフトウェア開発には採用されていない。
【０００６】
さらに、モデル検査の結果、検査項目を満足する動作仕様が得られても、その動作仕様からソフトウェアを作成する際には、開発者が動作仕様から論理構造を抽出し、ソフトウェア開発言語によりプログラミングを行うことが必要であった。
【０００７】
本発明は、上記の問題に鑑み、モデル記述言語の習得を必要とせずに、動作仕様からモデル検査プログラムを生成でき、より好ましくは、検証済みの動作仕様に応じたソフトウェアを自動的に生成することも可能なモデル検査支援装置を提供することを目的とする。
【課題を解決するための手段】
【０００８】
上記の目的を達成するために、本発明にかかるソフトウェア動作仕様のモデル検査支援装置は、ソフトウェアの動作仕様を、変数の状態遷移関係で表した論理記述として入力する仕様入力部と、モデル検査プログラムの雛型を格納したモデル記述言語辞書記憶部と、前記仕様入力部へ入力された論理記述から前記動作仕様の論理構造を抽出し、抽出された論理構造と前記モデル記述言語辞書記憶部の前記雛型とを用いて、モデル検査プログラムを作成する翻訳部とを備えたことを特徴とする。
【０００９】
また、本発明にかかるモデル検査システムは、本発明にかかるモデル検査支援装置と、前記モデル検査支援装置により生成されたモデル検査プログラムのモデル検査を行うモデル検査器とを備えたことを特徴とする。
【００１０】
また、本発明にかかるモデル検査支援プログラムは、コンピュータにソフトウェア動作仕様のモデル検査支援処理を実行させるモデル検査支援プログラムであって、ソフトウェアの動作仕様を、変数の状態遷移関係で表した論理記述として入力する仕様入力処理と、前記仕様入力処理で入力された論理記述から前記動作仕様の論理構造を抽出し、抽出された論理構造と、モデル記述言語辞書記憶部から取得したモデル検査プログラムの雛型とを用いて、モデル検査プログラムを作成する翻訳処理とを、コンピュータに実行させることを特徴とする。
【発明の効果】
【００１１】
本発明によれば、モデル記述言語の習得を必要とせずに、動作仕様からモデル検査プログラムを自動的に生成できる。その結果として、モデル検査をソフトウェア開発実務へ適用することが可能となる。
【発明を実施するための最良の形態】
【００１２】
本発明にかかるソフトウェア動作仕様のモデル検査支援装置は、ソフトウェアの動作仕様を、変数の状態遷移関係で表した論理記述として入力する仕様入力部と、モデル検査プログラムの雛型を格納したモデル記述言語辞書記憶部と、前記仕様入力部へ入力された論理記述から前記動作仕様の論理構造を抽出し、抽出された論理構造と前記モデル記述言語辞書記憶部の前記雛型とを用いて、モデル検査プログラムを作成する翻訳部とを備えた構成である。
【００１３】
上記の構成では、翻訳部が、変数の状態遷移関係で表された論理記述から動作仕様の論理構造を抽出し、抽出した論理構造に、モデル記述言語辞書記憶部の雛型を適用することにより、モデル検査プログラムを作成することができる。これにより、従来のように動作仕様から手作業により論理構造を抽出する必要がなくなり、開発効率を大幅に向上させることができる。
【００１４】
上記のモデル検査支援装置において、前記仕様入力部が、前記変数の状態遷移関係を図形表現として入力し、前記翻訳部は、前記仕様入力部に入力された図形表現から動作仕様の論理構造を抽出することが好ましい。図形表現としては、例えばフローチャート、ＰＡＤ、あるいは状態遷移図などを用いることができる。
【００１５】
上記のモデル検査支援装置において、前記翻訳部により抽出された動作仕様の論理構造を記憶する論理構造記憶部と、開発言語プログラムの雛型を格納した開発言語辞書記憶部と、前記論理構造記憶部に記憶された論理構造と、前記開発言語辞書記憶部の前記雛型とを用いて、開発言語によるプログラムを作成するプログラム作成部とをさらに備えた構成とすることが好ましい。これにより、プログラムの開発効率をさらに向上させることが可能となる。
【００１６】
また、本発明にかかるモデル検査システムは、上記したいずれかの構成にかかるモデル検査支援装置と、前記モデル検査支援装置により生成されたモデル検査プログラムのモデル検査を行うモデル検査器とを備えた構成である。
【００１７】
さらに、本発明にかかるモデル検査プログラムは、コンピュータにソフトウェア動作仕様のモデル検査支援処理を実行させるモデル検査支援プログラムであって、ソフトウェアの動作仕様を、変数の状態遷移関係で表した論理記述として入力する仕様入力処理と、前記仕様入力処理で入力された論理記述から前記動作仕様の論理構造を抽出し、抽出された論理構造と、モデル記述言語辞書記憶部から取得したモデル検査プログラムの雛型とを用いて、モデル検査プログラムを作成する翻訳処理とを、コンピュータに実行させるプログラムである。
【００１８】
上記のモデル検査プログラムは、前記仕様入力処理において、前記変数の状態遷移関係を図形表現として入力し、前記翻訳処理において、前記仕様入力処理で入力された図形表現から動作仕様の論理構造を抽出することが好ましい。
【００１９】
また、上記のモデル検査プログラムは、前記翻訳処理により抽出された動作仕様の論理構造を記憶した論理構造記憶部と、開発言語プログラムの雛型を格納した開発言語辞書記憶部とを参照し、前記論理構造記憶部から取得した論理構造と、前記開発言語辞書記憶部から取得した前記雛型とを用いて、開発言語によるプログラムを作成するプログラム作成処理をコンピュータに実行させることが好ましい。
【００２０】
以下、本発明にかかるモデル検査システムの具体的な実施形態について、図面を参照しながら説明する。なお、以下の実施形態では、ソフトウェア動作仕様をフローチャートにより図形入力し、モデル検査プログラムを作成する例を説明するが、ソフトウェア動作仕様の入力方法はこの例のみに限定されず、例えばＰＡＤ（Problem Analysis Diagram）や状態遷移図等を用いることも可能である。
（第１の実施形態）
最初に、図１を参照し、本発明の第１の実施形態にかかるモデル検査システムの概略構成について説明する。図１は、本実施形態のモデル検査システムのブロック構成図である。
【００２１】
図１に示すように、本実施形態のモデル検査システムは、ソフトウェアの動作仕様１からモデル検査プログラムを生成するモデル検査支援装置２と、モデル検査支援装置２で生成されたモデル検査プログラムを、検査項目９に従って検査し、検査結果１１を出力するモデル検査器１０とを備えている。
【００２２】
モデル検査支援装置２は、ソフトウェアのプログラム仕様書である動作仕様１からモデル検査に必要な情報を入力する仕様入力部３と、動作仕様１から論理構造を読み取り、モデル検査専用言語によりモデル検査プログラムを作成する翻訳部４とを備えている。モデル検査支援装置２は、さらに、論理構造記憶部５とモデル記述言語辞書６とを備え、これらは翻訳部４に接続されている。論理構造記憶部５は、動作仕様１から抽出した論理構造を記憶する。モデル記述言語辞書６は、状態遷移と状態遷移条件との組み合わせについて、定型的な雛型を記憶している。
【００２３】
モデル検査支援装置２およびモデル検査器１０は、例えばパーソナルコンピュータ等のコンピュータを用いて実現することが可能である。その場合、仕様入力部３および翻訳部４の機能は、当該コンピュータに所定のプログラムを実行させることによって実現される。論理構造記憶部５およびモデル記述言語辞書６は、コンピュータのハードディスクやその他の記憶媒体によって実現される。なお、モデル検査支援装置２およびモデル検査器１０は、１台のコンピュータによって実施することも可能であるが、複数台のコンピュータで実施することも可能である。
【００２４】
次に、図２を参照しながら、本実施形態のモデル検査システムの動作について説明する。
【００２５】
本実施形態のモデル検査システムにおいてモデル検査を行う場合、まず、作業者が、モデル検査に必要な項目の名前と各項目が取り得る状態とを動作仕様１から抽出し、抽出結果を仕様入力部３により入力する（ステップＳ１０）。仕様入力部３は、キーボード等の入力デバイスやディスプレイ等の出力デバイス（いずれも図示せず）を含んでおり、作業者はこれらの入出力デバイスを用いて、項目名と状態をモデル検査システムへ入力する。
【００２６】
次に、作業者は、ステップＳ１０で入力された項目名に対して割り当てる変数名を、仕様入力部３より入力する（ステップＳ１１）。この変数名は、モデル検査プログラムで用いられる変数名となる。この時、作業者が、予め定められたルールに従って変数名の割り当てを行えば、モデル検査プログラムのメンテナンス性が向上する。また、作業者は、ステップＳ１０で項目毎に入力された状態に対して割り当てる変数値を、仕様入力部３より入力する（ステップＳ１２）。この変数値も、モデル検査プログラムで用いられる。
【００２７】
なお、上記のステップＳ１０〜Ｓ１２で入力された項目および状態と、それらの各々に割り当てられた変数名および変数値とを、一覧表としてディスプレイ等に画面表示すれば、あるいは、例えば表計算ソフト等のデータとして出力すれば、次のステップＳ１３における作業者の図表作成が容易になるという利点がある。
【００２８】
次に、作業者は、ステップＳ１０〜Ｓ１２で作成された一覧表を参照し、動作仕様１の内容を表すフローチャートを作成して、仕様入力部３より入力する（ステップＳ１３）。フローチャートは、作業者が、ディスプレイの画面上で図表として作成し、入力する。この時、仕様入力部３は、予め用意された、図形記号の描画・配置機能と、図形記号間の結線機能と、図形記号への数式入力機能等を用いて、フローチャートのブロックの配置、ブロック間の結線、およびブロック内の動作内容の、作業者による入力作業を支援する。動作仕様１の内容をフローチャート化して入力・表示することで、作業者が入力結果を容易に確認することができる。
【００２９】
翻訳部４は、フローチャートの各接続線に、プログラムカウンタの値を重複しないように割り当てる（ステップＳ１４）。プログラムカウンタは、入力された項目と同様に変数として扱われる。
【００３０】
次に、翻訳部４は、フローチャートを変数毎に最初からトレースして、各変数の初期値と、次の値と、次の値へ変化するための条件式、すなわち状態遷移関係を抽出する（ステップＳ１５）。この時、変数の値が変化するための条件式にプログラムカウンタの変数を含めることにより、フローチャートの時系列を状態遷移系に表現する。
【００３１】
得られた全ての変数の状態遷移関係は、動作仕様１の論理構造として、論理構造記憶部５に記憶保存される（ステップＳ１６）。
【００３２】
次に、翻訳部４は、変数毎の状態遷移関係を、モデル記述言語辞書６に記憶されている雛型にあてはめ、モデル記述言語のプログラムコードに変換する（ステップＳ１７）。さらに、翻訳部４は、ステップＳ１７で得られたモデル記述言語のプログラムコードを所定の順序で並べ替えて、モデル検査プログラムを作成する（ステップＳ１８）。
【００３３】
以上の手順でモデル検査支援装置２により得られたモデル検査プログラムは、モデル検査器１０に入力される。モデル検査器１０は、上記のモデル検査プログラムが、別途入力された検査項目９を満足しているかどうかを、数理的に検査する（ステップＳ１９）。モデル検査器１０による検査結果は、検査結果１１として出力される。
【００３４】
作業者は、検査結果１１を見て、動作仕様１が検査項目９を満足しているかを判定し（ステップＳ２０）、満足していない場合は、動作仕様もしくは論理構造の修正を行い、再度、モデル検査を繰り返す（ステップＳ２１）。動作仕様１が検査項目９を満足している場合には、検証作業を終了する（ステップＳ２２）。
【００３５】
ここで、図２のステップＳ１０〜Ｓ２２の処理の具体例について、図３〜図１０を参照しながらより詳細に説明する。
【００３６】
例えば、プログラムの動作仕様１の内容が、「数字の値が１であれば、出力を『奇数』とする。数字の値が２であれば、出力を『偶数』とする。数字の初期値は１とし、その後の値は、出力後に非決定的に書き換えられて最初に戻り、書き換えられた数字に応じて『奇数』または『偶数』を出力する処理を繰り返し実行する。」というものであったとする。
【００３７】
この場合、上記ステップＳ１０〜Ｓ１２により、モデル検査に必要な項目と状態について、図３の一覧表に示すような変数名および変数値が割り当てられる。すなわち、項目名として抽出されるのは「数字」と「出力」であり、「数字」が取り得る状態は「１」と「２」、「出力」が取り得る状態は「奇数」と「偶数」である。
【００３８】
図３に例示した一覧表には、項目名およびその状態の他に、初期値の欄と状態の非決定性を示す欄とが設けられている。「数字」という項目については、上記プログラムの動作仕様１の記述内容に従い、初期値が「１」であることと、この項目の非決定性が「あり」であることが記述される。「非決定性」は、例えば、当該項目がランダムに選ばれる場合や、当該項目の状態が外部から入力される場合、あるいは、当該項目の状態が他の項目の処理結果などとして与えられる場合で、当該項目の状態が決定的でない場合に「あり」とされる。上記の具体例では、「数字」は、動作仕様１により非決定的に書き換えられることが明示されていることから、非決定性は「あり」と記述される。
【００３９】
図３に例示した一覧表において、項目「数字」には「num」、項目「出力」には「out」が、変数名としてそれぞれ割り当てられている。また、項目「数字」の状態である「１」と「２」には、変数値として“１”と“２”がそれぞれ割り当てられている。項目「出力」の状態である「奇数」と「偶数」には、変数値として“ODD”と“EVEN”がそれぞれ割り当てられている。さらに、項目「出力」の初期値の欄には、「数字」の初期値が「１」であることから、“ODD”が記述されている。また、項目「出力」の値は、「数字」の値によって一意に決定されるため、非決定性の欄には「なし」が記述される。
【００４０】
図４は、図３に例示した一覧表に基づいて作成され、作業者によって仕様入力部３より入力されるフローチャートである。このフローチャートでは、スタート（ステップＳ１）の後、numの値が“１”であるか否かを判断する（ステップＳ２）。ステップＳ２の結果がＹＥＳであれば変数outに“ODD”を代入し（ステップＳ３）、ステップＳ２の結果がＮＯであれば変数outに“EVEN”を代入する（ステップＳ４）。変数outへの代入後、変数numに“１”または“２”が代入され（ステップＳ５）、以上の処理が繰り返し実行される。
【００４１】
図５〜図７は、図４のフローチャートが仕様入力部３から入力された場合に、翻訳部４による図２のステップＳ１４〜Ｓ１６の処理により、フローチャートの変数毎の状態遷移関係が抽出される様子を示す。
【００４２】
翻訳部４は、まず、図５に示すように、フローチャートに含まれる全てのブロックと接続線について、各ブロックの処理または接続線の種類を判別すると共に、それぞれにＩＤ番号（１，２，・・・）を付与する。ＩＤ番号は、まず、ブロックに対して順に付与され、全てのブロックへのＩＤ番号付与が終わった後に、接続線に対してＩＤ番号の付与が行われる。
【００４３】
具体的には、ステップＳ１は、開始処理を行うブロックであり、最初のブロックであるため、「開始処理／１」とされる。ステップＳ２は、「一般条件処理／２」とされる。ステップＳ３は「一般処理／３」、ステップＳ４は「一般処理／４」とされる。ステップＳ５は「非決定処理／５」とされる。
【００４４】
さらに、ステップＳ１とステップＳ２との接続線は、「接続線／６」とされる。ステップＳ２とステップＳ３との接続線は、「Ｙｅｓ接続線／７」、ステップＳ２とステップＳ４との接続線は、「Ｎｏ接続線／８」とされる。ステップＳ３とステップＳ５との接続線は「接続線／９」、ステップＳ４とステップＳ５との接続線は「接続線／１０」、ステップＳ５とステップＳ１との接続線は「接続線／１１」とされる。
【００４５】
また、翻訳部４は、フローチャートの各接続線に、プログラムカウンタ（以下、ＰＣと表記する）を割り当てる（図２のステップＳ１４）。図５の例では、接続線／６にＰＣ＝１、Ｙｅｓ接続線／７にＰＣ＝２、Ｎｏ接続線／８にＰＣ＝３、接続線／９にＰＣ＝４を、それぞれ割り当てる。接続線／１０および接続線／１１は、接続先が他の接続線であるため、ＰＣを割り当てない。
【００４６】
次に、翻訳部４は、図３の一覧表と図５の割り当て結果に従って、フローチャートの要素の定義リストを作成する。その一例を図６に示す。図６の定義リストは、変数宣言部６１と、フローチャートの各要素の定義部６２を有する。変数宣言部６１の内容は、図３の一覧表から得られる。定義部６２の内容は、図５の割り当て結果から得られる。
【００４７】
すなわち、変数宣言部６１は、先頭行に、変数宣言部であることを表すコメントである「＃Variables」が記述され、次の行に、図３に示した変数「num」について、当該変数の変数型（整数）、変数名（num）、初期値（１）、下限値（１）、上限値（２）が定義されている。その次の行には、図３に示した変数「out」について、当該変数の変数型（シンボルセット型）、変数名（out）、初期値（ODD）、全シンボル（ODD,EVEN）が定義されている。
【００４８】
定義部６２は、先頭行に、フローチャートの要素の定義部であることを示すコメントである「＃Flow-Chart」が記述されている。２行目以降には、開始処理／１からＩＤ番号順に、各要素の定義が記述される。例えば、一般条件処理／２は分岐処理であるため、分岐条件となる変数名（num）と、比較値（１）と、比較演算子（＝）が記述される。一般処理／３は代入処理であるため、変数名（out）、代入値（ODD）が記述される。一般処理／４もこれと同様である。非決定処理／５は、ランダムな代入処理であるため、変数名(num)と、代入値候補（１／２：このスラッシュ記号は候補値の区切りを表す）が記述される。接続線／６は、前後の処理を結ぶ接続線であるため、前の処理（開始処理／１）と、後の処理（一般条件処理／２）と、この接続線のＰＣ値（１）が記述される。Ｙｅｓ接続線／７、Ｎｏ接続線／８、接続線／９についても、同様に、前の処理と、後の処理と、当該接続線のＰＣ値が記述される。接続線／１０および接続線／１１は、ＰＣ値を持たないので、前の処理と後の処理のみが記述される。
【００４９】
翻訳部４は、次に、図６の定義リストから、変数毎に、変数名と、初期値と、値域と、状態遷移を抽出する（図２のステップＳ１５）。その抽出結果を図７に示す。変数名、初期値、および値域は、定義リストの変数宣言部６１から取得される。状態遷移は、定義リストの定義部６２から取得され、状態遷移条件と代入値とをカンマで区切って列挙した態様で記述される。例えば変数numは、ＰＣ値が４のときに変数値として１または２が代入されるので、状態遷移は、図７中に示すように、「ＰＣ＝４，１／２」のように記述される。また、変数outは、ＰＣ値が２のときに変数値ODDが代入され、ＰＣ値が３のときに変数値EVENが代入されるので、状態遷移は、図７中に示すように、「ＰＣ＝２，ＯＤＤ」、「ＰＣ＝３，ＥＶＥＮ」のように記述される。以上のように抽出された状態遷移関係は、動作仕様１から得られた論理構造として、論理構造記憶部５へ記憶される。
【００５０】
翻訳部４は、次に、図２のステップＳ１７〜Ｓ１８において、図７の抽出結果に基づき、モデル記述言語辞書６を参照し、モデル検査器１０への入力言語列（モデル検査プログラム）を生成する。ここで、図８に、モデル記述言語辞書６に格納されている雛型の一例を示す。図８の例は、ＳＭＶ（Symbolic Model Verifier）言語の雛型であるが、本発明においてモデル記述言語として用いることができる言語は、これのみに限定されない。
【００５１】
図８に示した雛型において、斜体文字で示したシンボルは定型部分である。「ＶＡＲ」は、変数の宣言部分であり、値域を定義する。「ＡＳＳＩＧＮ」は、状態遷移を定義する。「ｉｎｉｔ（ｘｘ）」は変数ｘｘの初期値を定義する。「ｎｅｘｔ（ｘｘ）」は、ｃａｓｅ文（case〜esac）の中で、状態遷移条件と変数ｘｘへの代入値を定義する。ｃａｓｅ文では、コロン“：”の左側に状態遷移条件、右側に変数ｘｘへの代入値が、それぞれ記述される。なお、図８におけるｃａｓｅ文の１行目は、コロンの左側の状態遷移条件が満たされれば、1行目に記述されている代入値を変数ｘｘに代入することを意味し、２行目は、１：ｘｘと記述されていることから（１はｔｒｕｅを表す）、１行目の状態遷移条件以外の全ての場合において、変数ｘｘへ変数ｘｘの値を代入する、すなわち、変数ｘｘの値を保持することを意味する。翻訳部４は、個々のシステムに応じて、上記の雛型のｘｘの部分に変数を割り当てると共に、値域、初期値、代入値を適切に割り当てることにより、モデル検査器１０へのモデル検査プログラムを生成する。
【００５２】
図７の抽出結果から、図８の雛型を用いて翻訳部４により生成されるモデル検査プログラムの一例を図９に示す。モデル検査プログラムの冒頭の「MODULE main」という記述は、メインモジュールであることを表す。また、図９において、「＆」は積条件の演算子、「！」は否定条件の演算子である。
【００５３】
このように生成されたモデル検査プログラムは、翻訳部４からモデル検査器１０へ渡される。作業者は、モデル検査器１０へ、検査項目９として、例えば図１０に示すような時相論理式（ＥＦ）を入力する。モデル検査器１０は、入力された検査項目９をモデル検査プログラムの最後に「ＳＰＥＣ」というシンボルで追記して、モデル検査を実行する。時相論理式は、例えば、ＥＦ（Ｐ）というフォーマットを持ち、「あるパスにおいて（Exist）、将来のある時点において（Future）、Ｐが成立する」ことの真偽を返す。すなわち、図１０に示す時相論理式は、被検査プログラムが最終ステップに到達すること、つまり、ＰＣの値が４に到達すること、を表現している。検査項目は、この他に、例えば、ＥＦ（ｎｕｍ＝２）のような記述の仕方も可能である。この時相論理式は、変数ｎｕｍの値が２となることがあるかどうかを検査するための式である。また、ＡＦ（Ｐ）というフォーマットの時相論理式を用いることも可能である。これは、「全てのパスにおいて（All）、将来のある時点において（Future）、Ｐが成立する」ことの真偽を返す式である。
【００５４】
モデル検査器１０は、図２のステップＳ１９において、上述のように生成されたモデル検査プログラムを用い、時相論理式として与えられた検査項目の真偽を、検査結果１１として返す。そして、その検査結果１１を作業者が確認し、検査結果が良であれば検証作業を終了し、不良であれば、ステップＳ２１で動作仕様や論理構造の見直しを行い、再度検証作業を行う。
【００５５】
以上のように、本実施形態によれば、作業者が、動作仕様１の項目および状態に変数を割り当て、動作仕様１の内容を表すフローチャートを仕様入力部３から入力すれば、翻訳部４により、そのフローチャートから変数毎の状態遷移関係が抽出され、動作仕様１に応じたモデル検査プログラムが自動的に生成される。これにより、従来のように動作仕様から手作業により論理構造を抽出する必要がなくなり、開発効率を大幅に向上させることができる。
（第２の実施形態）
次に、図１１を参照し、本発明の第２の実施形態にかかるモデル検査システムの概略構成について説明する。図１１は、本実施形態のモデル検査システムのブロック構成図である。
【００５６】
図１１に示すように、本実施形態のモデル検査システムは、モデル検査支援装置２が、開発言語辞書８と、開発言語プログラムを作成するプログラム作成部７とを備えている点において、第１の実施形態にかかるモデル検査システムと異なっている。
【００５７】
プログラム作成部７は、モデル検査器１０による検査結果１１が良であった場合、論理構造記憶部５に記憶されている論理構造から、開発言語プログラム１２を作成する。すなわち、動作仕様１が検査項目９を満足している場合は、その動作仕様１から抽出されて論理構造記憶部５に記憶されている論理構造は当然に検査項目９を満足している。従って、その論理構造に基づいてプログラム作成部７がプログラムを生成すれば、検査項目９を満足する開発言語プログラム１２が得られる。
【００５８】
次に、図１２のフローチャートを参照して、プログラム作成部７により行われる開発言語プログラム１２の作成について説明する。なお、翻訳部４によるモデル検査プログラムの生成およびそのモデル検査プログラムを用いたモデル検査器１０による検査の手順については、第１の実施形態で図２を参照しながら説明したとおりであるため、重複した説明は省略する。
【００５９】
モデル検査器１０による検査結果１１が良であった場合（図２のステップＳ２０の結果が良の場合）、ステップＳ２２に移行して検証作業は終了する。本実施形態では、その後、プログラム作成部７が、図１２に示すように、論理構造記憶部５から、各変数の状態遷移関数を呼び出す（ステップＳ３１）。次に、プログラム作成部７は、変数毎の状態遷移関係を、開発言語辞書８に記憶されている開発言語の雛型にあてはめることにより、開発言語のプログラムソースコードに変換する（ステップＳ３２）。さらに、プログラム作成部７は、開発言語のプログラムソースコードを所定の順序で並べ替え、開発言語プログラムを完成させる（ステップＳ３３）。
【００６０】
ここで、図１２のステップＳ３１〜Ｓ３３の処理の具体例について、図１３〜図１４を参照しながらより詳細に説明する。
【００６１】
図１３は、開発言語辞書８に記憶されている開発言語の雛型の一例として、JavaScript（登録商標）言語用の雛型を示す。ただし、本発明で用いられる開発言語は、これに限定されるものではない。図１３において、斜体文字で表した部分は定型部分である。プログラム作成部７は、個々のシステムに応じて、ｘｘに変数、ｙｙｙにクラス名／メソッド名、変数型、初期値、状態遷移条件、代入値などを適切に割り当てる。図１３の雛型では、冒頭で、変数の変数型および初期値を記述する。そして、３行目以降で、状態遷移条件と、状態遷移時の代入値を記述する。
【００６２】
例えば、図７に示した論理構造に、図１３の雛型を適用することにより、図１４に示すようなプログラムソースコードが得られる。ここで、クラス名とメソッド名は、ユニークであることを条件として、プログラム作成部７が任意に付与して良い。なお、図１４の例では、JavaScript（登録商標）言語では用いないＰＣ値を省略して、図７のＰＣ値の順に処理をたどることで、ＰＣ値が示す動作順序をJavaScript（登録商標）言語の実行順序に置き換えている。さらに、プログラム作成部７は、非決定処理をRandomクラスで実装している。
【００６３】
以上のように、第２の実施形態によれば、モデル検査支援装置２は、動作仕様１に対するモデル検査プログラムを自動作成するだけでなく、検証結果１１が良であった場合、その動作仕様１の論理構造と開発言語辞書８とに基づいて、開発言語プログラム１２を自動的に生成する。これにより、プログラムの開発効率をさらに向上させることが可能となる。
【図面の簡単な説明】
【００６４】
【図１】本発明の第１の実施形態にかかるモデル検査システムの概略構成を示すブロック図である。
【図２】第１の実施形態にかかるモデル検査システムの動作を示すフローチャートである。
【図３】第１の実施形態にかかるモデル検査システムおいて、動作仕様の項目および状態に割り当てられる変数の一例を示す説明図である。
【図４】動作仕様を表すフローチャートの一例である。
【図５】図４に示すフローチャートの各要素にＩＤ番号およびプログラムカウンタを割り当てた様子を示す説明図である。
【図６】動作仕様を表すフローチャートから得られた各要素の定義リストの一例を表す説明図である。
【図７】変数毎の遷移状態関係を表すリストの一例を示す説明図である。
【図８】モデル記述言語の雛型の一例を示す説明図である。
【図９】生成されたモデル検査プログラムの一例を示す説明図である。
【図１０】検査項目の時相論理式の記述例である。
【図１１】本発明の第２の実施形態にかかるモデル検査システムの概略構成を示すブロック図である。
【図１２】第２の実施形態にかかるモデル検査システムの動作を示すフローチャートである。
【図１３】プログラムの開発言語の雛型の一例を示す説明図である。
【図１４】生成された開発言語プログラムのソースコードの一例を示す説明図である。
【符号の説明】
【００６５】
１    動作仕様
２    モデル検査支援装置
３    仕様入力部
４    翻訳部
５    論理構造記憶部
６    モデル記述言語辞書
７    プログラム作成部
８    開発言語辞書
９    検査項目
１０  検査結果
１１  検査結果
【図１】
2007011605.tif 000003
【図２】
2007011605.tif 000004
【図３】
2007011605.tif 000005
【図４】
2007011605.tif 000006
【図５】
2007011605.tif 000007
【図６】
2007011605.tif 000008
【図７】
2007011605.tif 000009
【図８】
2007011605.tif 000010
【図９】
2007011605.tif 000011
【図１０】
2007011605.tif 000012
【図１１】
2007011605.tif 000013
【図１２】
2007011605.tif 000014
【図１３】
2007011605.tif 000015
【図１４】
2007011605.tif 000016