(57)【要約】【課題】モデル検査の効率の向上を図ること。【解決手段】プロセスの構造を表すクラスと、当該クラスの状態遷移を表すステートマシンと、によるシステムモデルを表すモデル情報を記憶するモデル情報記憶手段と、モデル情報記憶手段に記憶されているクラスに対応付け可能なステートマシンのうち特定のステートマシンの選択を受け付けて、当該選択された特定のステートマシンとクラスとを組み合わせた検査対象モデルを設定する検査対象モデル設定手段と、設定された検査対象モデルを表す検査対象モデル情報が、予め定められた検査式を満たすか否かの検査を実行する検査実行手段と、検査対象モデル情報と、当該検査対象モデルの検査実行手段による検査結果と、を出力する検査結果出力手段と、を備えた。【選択図】図１
2009223711.tif 000002
【特許請求の範囲】
【請求項１】
プロセスの構造を表すクラスと、当該クラスの状態遷移を表すステートマシンと、によるシステムモデルを表すモデル情報を記憶するモデル情報記憶手段と、
前記モデル情報記憶手段に記憶されている前記クラスに対応付け可能な前記ステートマシンのうち特定のステートマシンの選択を受け付けて、当該選択された特定のステートマシンと前記クラスとを組み合わせた検査対象モデルを設定する検査対象モデル設定手段と、
前記設定された検査対象モデルを表す検査対象モデル情報が、予め定められた検査式を満たすか否かの検査を実行する検査実行手段と、
前記検査対象モデル情報と、当該検査対象モデルの前記検査実行手段による検査結果と、を出力する検査結果出力手段と、
を備えたことを特徴とするモデル検査装置。
【請求項２】
前記検査対象モデル設定手段にて設定された検査対象モデルを表す検査対象モデル情報を記憶する検査対象モデル記憶手段を備え、
前記検査対象モデル設定手段は、前記検査対象モデル記憶手段に記憶されている前記検査対象モデル情報を読み出して、前記検査実行手段にて実行する検査対象モデルとして設定する、
ことを特徴とする請求項１記載のモデル検査装置。
【請求項３】
前記検査対象モデル記憶手段は、前記検査実行手段にて検査を実行した前記検査対象モデル情報と、その検査結果と、を関連付けて記憶し、
前記検査結果出力手段は、前記検査結果記憶手段に記憶されている前記検査対象モデル情報と、その前記検査結果と、を出力する、
ことを特徴とする請求項２記載のモデル検査装置。
【請求項４】
前記検査対象モデル設定手段は、前記検査対象モデル記憶手段から読み出して設定した前記検査対象モデルの前記クラスと前記特定のステートマシンとによる組み合わせを変更するよう他の特定のステートマシンの選択を受け付けて、当該選択された他の特定のステートマシンと前記クラスとを組み合わせた検査対象モデルを設定する、
ことを特徴とする請求項２又は３記載のモデル検査装置。
【請求項５】
前記検査実行手段は、実行した検査の実行時間を計測して前記検査結果に含める、
ことを特徴とする請求項１，２，３又は４記載のモデル検査装置。
【請求項６】
前記検査実行手段は、実行している検査の実行時間が、予め定められた時間を超えた場合に、当該検査の実行を停止する、
ことを特徴とする請求項５記載のモデル検査装置。
【請求項７】
前記検査結果記憶手段に記憶されている前記実行時間が、指定された時間以内である前記検査対象モデルを、前記検査結果記憶手段から検索する検査検索手段を備え、
前記検査結果出力手段は、前記検査検索手段にて検索された前記検査対象モデルの前記検査対象モデル情報と、当該検査対象モデルの前記検査実行手段による検査結果と、を出力する、
ことを特徴とする請求項５又は６記載のモデル検査装置。
【請求項８】
複数の前記検査対象モデルの検査順序を設定する検査順序設定手段を備え、
前記検査実行手段は、前記設定された検査順序に従って前記各検査対象モデルの検査をそれぞれ実行する、
ことを特徴とする請求項１，２，３，４，５，６又は７記載のモデル検査装置。
【請求項９】
前記モデル情報記憶手段は、前記クラスに対応付け可能であり、当該クラスの状態遷移の詳細度合いが異なる複数のステートマシンを記憶している、
ことを特徴とする請求項１，２，３，４，５，６，７又は８記載のモデル検査装置。
【請求項１０】
コンピュータに、
プロセスの構造を表すクラスと、当該クラスの状態遷移を表すステートマシンと、によるシステムモデルを表すモデル情報を記憶装置に記憶するモデル情報記憶処理手段と、
前記記憶装置に記憶されている前記クラスに対応付け可能な前記ステートマシンのうち特定のステートマシンの選択を受け付けて、当該選択された特定のステートマシンと前記クラスとを組み合わせた検査対象モデルを設定する検査対象モデル設定手段と、
前記設定された検査対象モデルを表す検査対象モデル情報が、予め定められた検査式を満たすか否かの検査を実行する検査実行手段と、
前記検査対象モデル情報と、当該検査対象モデルの前記検査実行手段による検査結果と、を出力する検査結果出力手段と、
を実現させるためのプログラム。
【請求項１１】
前記コンピュータに、
前記検査対象モデル設定手段にて設定された検査対象モデルを表す検査対象モデル情報を記憶装置に記憶する検査対象モデル記憶処理手段を実現すると共に、
前記検査対象モデル設定手段は、前記記憶装置に記憶されている前記検査対象モデル情報を読み出して、前記検査実行手段にて実行する検査対象モデルとして設定する、
ことを特徴とする請求項１０記載のプログラム。
【請求項１２】
プロセスの構造を表すクラスと、当該クラスの状態遷移を表すステートマシンと、によるシステムモデルを表すモデル情報を記憶装置に記憶するモデル情報記憶処理工程と、
前記記憶装置に記憶されている前記クラスに対応付け可能な前記ステートマシンのうち特定のステートマシンの選択を受け付けて、当該選択された特定のステートマシンと前記クラスとを組み合わせた検査対象モデルを設定する検査対象モデル設定工程と、
前記設定された検査対象モデルを表す検査対象モデル情報が、予め定められた検査式を満たすか否かの検査を実行する検査実行工程と、
前記検査対象モデル情報と、当該検査対象モデルの前記検査実行手段による検査結果と、を出力する検査結果出力工程と、
を有することを特徴とするモデル検査方法。
【請求項１３】
前記検査対象モデル設定工程にて設定された検査対象モデルを表す検査対象モデル情報を記憶装置に記憶する検査対象モデル記憶処理工程を有すると共に、
前記検査対象モデル設定工程は、前記記憶装置に記憶されている前記検査対象モデル情報を読み出して、前記検査実行工程にて実行する検査対象モデルとして設定する、
ことを特徴とする請求項１２記載のモデル検査方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検査装置にかかり、特に、検査対象システムを表すモデルの記述が、所定の性質を満たすか否かを検査するモデル検査装置に関する。
【背景技術】
【０００２】
モデル検査とは、検査対象システム（ハードウェアとソフトウェアとを含む）の形式的に記述された仕様に対して、それが検査式を満足するかどうかを網羅的に検証することをいう。ここで、検査式とは、検査内容を示す情報であって、仕様に要求される性質を論理式で記述したものである。
【０００３】
一方で、モデル検査の利用には、形式的な仕様の記述が必要となるため、一般の開発者が利用しにくいという問題がある。この問題を解消するため、形式的な記述の代わりに、モデリング言語ＵＭＬ（Unified Modeling Language）で仕様を記述して検査する方法が知られている。この場合には、まず、ＵＭＬで記述したモデル図を形式的な仕様記述に自動変換する。そして、モデル検査では、検査対象のプロセスの構造（保持する情報や操作）と、そのプロセスのふるまい（状態遷移）の情報と、を入力として与える必要があるが、ＵＭＬを使用したモデル検査では、プロセスの構造をＵＭＬのクラスで、ふるまいをＵＭＬのステートマシンで表現し、クラスとステートマシンを関連付けてプロセスの構造とふるまいを表す。
【０００４】
ここで、あるシステムの概要設計から詳細設計へと進む開発フローに沿ってモデル検査を適用する場合には、概要設計で満たされた性質が詳細設計でも満たされることが望ましく、プロセス間の情報のやり取りの整合性はある程度保たれると考えられる。つまり、プロセス間の情報のやり取りはあまり変わらず、ふるまいのロジックが追加され詳細化されていくことになる。このような環境下では、クラスに関連付けられるステートマシンを切り替えることで、検証に要する時間の削減と状態爆発の回避が可能となる。なお、一般的に、モデル検査システムでは、検査対象のモデルが大きくなり状態数が増大すると、コンピュータで扱える範囲を超えてしまい処理しきれなくなるという問題があり、それを「状態爆発」と呼ぶ。
【０００５】
そして、特許文献１には、ＣＡＤシステムのシミュレーションに関して、指定された切替時刻で、低速なシミュレーション方法と、高速であるが低精度のシミュレーション方法と、を切り替えることで、検証のレベルにあったシミュレーションを選択可能とし、検証時間を短縮する設計支援装置が記載されている。また、特許文献２には、性能評価用シミュレーションに関して、外部から入力されるイベントに従って、異なるモデル動作手段を選択するシミュレーションシステムが記載されている。さらに、特許文献３には、ハードウェアを、選択した抽象度に応じたステートマシンの記述と、そのステートマシンの各ステートで実行するオブジェクトと、の組み合わせにより作成している。これにより、ステートマシン間でオブジェクトの再利用を可能としている。
【０００６】
【特許文献１】特許第３４７２０６７号公報
【特許文献２】特開２００４−２１９０７号公報
【特許文献３】特開２００３−３３０９９１号公報
【発明の開示】
【発明が解決しようとする課題】
【０００７】
しかしながら、上述した技術では、クラスと、当該クラスに結びつくステートマシンとにより構成されるモデルにおいて、概要設計から詳細設計へと進む開発フローに沿ってモデル検査を適用する場合に、設計の詳細度を変更することが困難である。従って、検査精度を維持しつつ、検査の実行時の削減を図るといった、バランスのよい検査を実行することができない、という問題がある。具体的に、特許文献１では、シミュレーションの処理方法を切り替えているだけである。また、特許文献２では、入力イベントに従って、クロック毎の信号レベルでの動作を記述したクロックモデル、複数の信号により表される１つの処理（トランザクション）毎に動作をまとめて記述したトランザクションモデル、入力データのまとまりに対する動作を記述したデータフローモデルなど、種別の異なるモデル動作手段を切り替えるしくみを提供するものであり、詳細度が異なるステートマシンを変更するものではない。さらに、特許文献３では、各ステートで実行するオブジェクトの再利用が可能なだけであり、クラスに結びつくステートマシンを切り替えるものではない。
【０００８】
このため、本発明の目的は、上述した課題である、モデル検査の効率の向上を図ることにある。
【課題を解決するための手段】
【０００９】
そこで、本発明の一形態であるモデル検査装置は、
プロセスの構造を表すクラスと、当該クラスの状態遷移を表すステートマシンと、によるシステムモデルを表すモデル情報を記憶するモデル情報記憶手段と、
モデル情報記憶手段に記憶されているクラスに対応付け可能なステートマシンのうち特定のステートマシンの選択を受け付けて、当該選択された特定のステートマシンとクラスとを組み合わせた検査対象モデルを設定する検査対象モデル設定手段と、
設定された検査対象モデルを表す検査対象モデル情報が、予め定められた検査式を満たすか否かの検査を実行する検査実行手段と、
検査対象モデル情報と、当該検査対象モデルの検査実行手段による検査結果と、を出力する検査結果出力手段と、
を備えた、という構成を採る。
【００１０】
また、本発明の他の形態であるプログラムは、
コンピュータに、
プロセスの構造を表すクラスと、当該クラスの状態遷移を表すステートマシンと、によるシステムモデルを表すモデル情報を記憶装置に記憶するモデル情報記憶処理手段と、
記憶装置に記憶されているクラスに対応付け可能なステートマシンのうち特定のステートマシンの選択を受け付けて、当該選択された特定のステートマシンとクラスとを組み合わせた検査対象モデルを設定する検査対象モデル設定手段と、
設定された検査対象モデルを表す検査対象モデル情報が、予め定められた検査式を満たすか否かの検査を実行する検査実行手段と、
検査対象モデル情報と、当該検査対象モデルの検査実行手段による検査結果と、を出力する検査結果出力手段と、
を実現させる、という構成を採る。
【００１１】
さらに、本発明の他の形態であるモデル検査方法は、
プロセスの構造を表すクラスと、当該クラスの状態遷移を表すステートマシンと、によるシステムモデルを表すモデル情報を記憶装置に記憶するモデル情報記憶処理工程と、
記憶装置に記憶されているクラスに対応付け可能なステートマシンのうち特定のステートマシンの選択を受け付けて、当該選択された特定のステートマシンとクラスとを組み合わせた検査対象モデルを設定する検査対象モデル設定工程と、
設定された検査対象モデルを表す検査対象モデル情報が、予め定められた検査式を満たすか否かの検査を実行する検査実行工程と、
検査対象モデル情報と、当該検査対象モデルの検査実行手段による検査結果と、を出力する検査結果出力工程と、
を有する、という構成を採る。
【発明の効果】
【００１２】
本発明は、以上のように構成されることにより、モデル検査を、所定の検査精度を維持しつつ、短時間で実行することでき、モデル検査の効率の向上を図ることができる、という優れた効果を有する。
【発明を実施するための最良の形態】
【００１３】
本発明は、モデル検査において、容易に状態遷移を切り替えて適切なモデル検査を選び出すことを可能とし、効率的な検査を行うことができる構成を採っている。例えば、概要設計から詳細設計という開発のフローに沿って概要設計における整合性を保ちながら詳細設計を検査する場合においては、検査対象モデルに含まれるクラスに対して、詳細度の異なるステートマシンから所望のステートマシンを選択して設定する手段を備えたことを特徴とする。また、設定されたステートマシンの情報を記憶する手段を備え、その設定でモデル検査を所望のときに再実行できる構成を採ることを特徴とする。
【００１４】
そして、本発明の一形態であるモデル検査装置は、
プロセスの構造を表すクラスと、当該クラスの状態遷移を表すステートマシンと、によるシステムモデルを表すモデル情報を記憶するモデル情報記憶手段と、
モデル情報記憶手段に記憶されているクラスに対応付け可能なステートマシンのうち特定のステートマシンの選択を受け付けて、当該選択された特定のステートマシンとクラスとを組み合わせた検査対象モデルを設定する検査対象モデル設定手段と、
設定された検査対象モデルを表す検査対象モデル情報が、予め定められた検査式を満たすか否かの検査を実行する検査実行手段と、
検査対象モデル情報と、当該検査対象モデルの検査実行手段による検査結果と、を出力する検査結果出力手段と、
を備えた、という構成を採る。
【００１５】
上記発明によると、まず、モデル検査装置には、クラスと、当該クラスに対応付け可能なステートマシンと、が記憶されている。そして、利用者がモデル検査装置に対してクラスに対応付けするステートマシンを選択入力することで、モデル検査装置は、クラスと選択されたステートマシンとの組み合わせによる検査対象モデルを設定する。その後、モデル検査装置は、設定した検査対象モデルが、所定の検査式を満たすか否かの検査を実行し、検査結果を出力する。
【００１６】
このように、利用者は、クラスとステートマシンとからなる検査対象モデルを任意に設定することができるため、検査精度と実行時間のバランスを考慮した最適なモデル検査を実行することができる。従って、モデル検査を、所定の検査精度を維持しつつ、短時間で実行することでき、モデル検査の効率の向上を図ることができる。
【００１７】
また、上記モデル検査装置は、上記検査対象モデル設定手段にて設定された検査対象モデルを表す検査対象モデル情報を記憶する検査対象モデル記憶手段を備え、上記検査対象モデル設定手段は、検査対象モデル記憶手段に記憶されている検査対象モデル情報を読み出して、検査実行手段にて実行する検査対象モデルとして設定する、という構成を採る。また、上記検査対象モデル記憶手段は、検査実行手段にて検査を実行した検査対象モデル情報と、その検査結果と、を関連付けて記憶し、上記検査結果出力手段は、検査結果記憶手段に記憶されている検査対象モデル情報と、その検査結果と、を出力する、という構成を採る。さらに、上記検査対象モデル設定手段は、検査対象モデル記憶手段から読み出して設定した検査対象モデルのクラスと特定のステートマシンとによる組み合わせを変更するよう他の特定のステートマシンの選択を受け付けて、当該選択された他の特定のステートマシンとクラスとを組み合わせた検査対象モデルを設定する、という構成を採る。
【００１８】
これにより、過去にモデル検査を行ったクラスとステートマシンとの組み合わせの検査対象モデルを記憶しているため、当該検査対象モデルの組み合わせや検査結果情報の参照、さらには、検査の再実行が容易となる。そして、過去に検査を実行した検査対象モデルの組み合わせも変更設定できる。従って、さらなるモデル検査の効率化を図ることができる。
【００１９】
また、上記モデル検査装置では、上記検査実行手段は、実行した検査の実行時間を計測して検査結果に含める、という構成を採る。また、上記検査実行手段は、実行している検査の実行時間が、予め定められた時間を超えた場合に、当該検査の実行を停止する、という構成を採る。さらに、上記検査結果記憶手段に記憶されている実行時間が、指定された時間以内である検査対象モデルを検索する検査検索手段を備え、上記検査結果出力手段は、検査検索手段にて検索された検査対象モデルの検査対象モデル情報と、当該検査対象モデルの検査実行手段による検査結果と、を出力する、という構成を採る。
【００２０】
これにより、検査対象モデルの検査の実行時間を計測でき、利用者は実行時間に基づいて効率よく検査を実行することができる。また、指定時間以内の実行時間の検査対象モデルを抽出することもでき、さらなる検査の効率化を図ることができる。
【００２１】
また、上記モデル検査装置では、複数の検査対象モデルの検査順序を設定する検査順序設定手段を備え、上記検査実行手段は、設定された検査順序に従って各検査対象モデルの検査をそれぞれ実行する、という構成を採る。これにより、複数の検査対象モデルを、設定した順序でまとめて検査することができ、検査のさらなる効率化を図ることができる。
【００２２】
なお、上記モデル検査装置では、上記モデル情報記憶手段は、クラスに対応付け可能であり、当該クラスの状態遷移の詳細度合いが異なる複数のステートマシンを記憶している、という構成を採る。
【００２３】
また、本発明の他の形態であるプログラムは、
コンピュータに、
プロセスの構造を表すクラスと、当該クラスの状態遷移を表すステートマシンと、によるシステムモデルを表すモデル情報を記憶装置に記憶するモデル情報記憶処理手段と、
記憶装置に記憶されているクラスに対応付け可能なステートマシンのうち特定のステートマシンの選択を受け付けて、当該選択された特定のステートマシンとクラスとを組み合わせた検査対象モデルを設定する検査対象モデル設定手段と、
設定された検査対象モデルを表す検査対象モデル情報が、予め定められた検査式を満たすか否かの検査を実行する検査実行手段と、
検査対象モデル情報と、当該検査対象モデルの検査実行手段による検査結果と、を出力する検査結果出力手段と、
を実現させる、という構成を採る。
【００２４】
そして、上記プログラムは、上記コンピュータに、検査対象モデル設定手段にて設定された検査対象モデルを表す検査対象モデル情報を記憶装置に記憶する検査対象モデル記憶処理手段を実現すると共に、上記検査対象モデル設定手段は、記憶装置に記憶されている検査対象モデル情報を読み出して、検査実行手段にて実行する検査対象モデルとして設定する、という構成を採る。
【００２５】
また、本発明の他の形態であるモデル検査方法は、
プロセスの構造を表すクラスと、当該クラスの状態遷移を表すステートマシンと、によるシステムモデルを表すモデル情報を記憶装置に記憶するモデル情報記憶処理工程と、
記憶装置に記憶されているクラスに対応付け可能なステートマシンのうち特定のステートマシンの選択を受け付けて、当該選択された特定のステートマシンとクラスとを組み合わせた検査対象モデルを設定する検査対象モデル設定工程と、
設定された検査対象モデルを表す検査対象モデル情報が、予め定められた検査式を満たすか否かの検査を実行する検査実行工程と、
検査対象モデル情報と、当該検査対象モデルの検査実行手段による検査結果と、を出力する検査結果出力工程と、
を有する、という構成を採る。
【００２６】
そして、上記モデル検査工程は、さらに、上記検査対象モデル設定工程にて設定された検査対象モデルを表す検査対象モデル情報を記憶装置に記憶する検査対象モデル記憶処理工程を有すると共に、上記検査対象モデル設定工程は、記憶装置に記憶されている検査対象モデル情報を読み出して、検査実行工程にて実行する検査対象モデルとして設定する、という構成を採る。
【００２７】
上述した構成のプログラム、モデル検査方法の発明であっても、上記モデル検査装置と同様に作用するため、上述した本発明の目的を達成することができる。
【００２８】
＜実施形態１＞
本発明の第１の実施形態を、図１乃至図１１を参照して説明する。図１は、モデル検査装置の構成を示す機能ブロック図である。図２乃至図５は、モデル検査装置に記憶されるモデルの構成の一例を示す図である。図６は、モデル検査装置に記憶されるモデル検査結果の一例を示す図である。図７乃至図８は、モデル検査装置に表示される画面の一例を示す図である。図９乃至図１１は、モデル検査装置の動作を示すフローチャートである。
【００２９】
［構成］
本実施形態におけるモデル検査装置１は、図１に示すように、キーボードといった操作部１１と、ディスプレイといった表示部１２と、ＣＰＵといった演算装置（図示せず）と、フラッシュメモリやハードディスクと言った記憶装置（図示せず）と、を備えた一般的なコンピュータで構成されている。そして、モデル検査装置１は、演算装置に所定のプログラムが組み込まれることによって構築された、モデル作成部１３と、モデル設定部１４と、検査実行部１５と、検査情報検索部１６と、を備えている。また、モデル検査装置１は、記憶装置に形成されたモデル情報記憶部１７と、検査結果記憶部１８と、を備えている。以下、各構成について詳述する。
【００３０】
まず、上記モデル作成部１３（モデル情報記憶処理手段）は、利用者から操作部１１を介して入力された情報に基づいて、検証対象となるシステムモデルを表すモデル図（検査対象モデル）を作成する。本実施形態では、例えば、モデリング言語ＵＭＬ（Unified Modeling Language）で仕様を記述するＵＭＬエディタであり、プロセスの構造を表すクラスと、当該クラスに対応付け可能でありクラスのふるまい（状態遷移）を表すステートマシンと、によるシステムモデルを表すモデル情報を作成する。そして、モデル作成部１３は、作成したクラスとステートマシンとを含むモデル情報を、モデル情報記憶部１７（モデル情報記憶手段）に記憶する。
【００３１】
ここで、上述したようにモデル作成部１３にて作成し、モデル情報記憶部１７に記憶するモデル情報について、図２乃至図５を参照して説明する。まず、モデル情報は、図２に示すように、クラス（１）と、それに対応付けることが可能な全てのステートマシン（１，２，３）と、により構成されており、クラス１と全てのステートマシン１，２，３とが対応付け可能な状態（図２の点線矢印参照）で記憶されている。そして、クラス１に対応付け可能な各ステートマシン１，２，３は、クラス１のふるまいの詳細度合いが異なるものである。例えば、ステートマシンの１つは、クラス１のふるまいの概要を表す概要設計レベルであり、別のステートマシンは、概要設計レベルよりもクラス１のふるまいのロジックが追加されて詳細化されている詳細設計レベルである。
【００３２】
ここで、クラスとステートマシンの具体例について説明する。まず、図３は、クラスＡ，Ｂ，Ｃを関連付けたクラス図であり、図４乃至図５は、各クラスのふるまい（状態遷移）を表すステートマシンである。具体的に、図４（ａ）は、クラスＡの概要設計レベルのふるまいを表すステートマシン、図４（ｂ）は、クラスＢの概要設計レベルのふるまいを表すステートマシン、図４（ｃ）は、クラスＣの概要設計レベルのふるまいを表すステートマシンである。そして、図５（ａ）は、クラスＡの詳細設計レベルのふるまいを表すステートマシン、図５（ｂ）は、クラスＢの詳細設計レベルのふるまいを表すステートマシン、図５（ｃ）は、クラスＣの詳細設計レベルのふるまいを表すステートマシンである。この場合には、クラスＡには、図４（ａ）に示す概要設計レベルのステートマシンと、図５（ａ）に示す詳細設計レベルのステートマシンと、が対応付け可能なようモデル情報記憶部１７に記憶されている。なお、上述したクラス及びステートマシンは、利用者から任意のタイミングで入力されるモデル作成要求に応じて作成される。
【００３３】
次に、上記モデル設定部１４（検査対象モデル作成手段）について説明する。モデル設定部１４は、モデル情報記憶部１７に記憶されているモデル情報を読み出して、クラスと当該クラスに対応付け可能なステートマシンとを表示部１２に表示し、利用者１１から操作部１１を介して入力されるステートマシンの選択を受け付ける。そして、モデル設定部１４は、クラスと、選択された特定のステートマシンと、を対応付けた組み合わせを検査対象モデルとして、その情報（検査対象モデル情報）を検査実行部１５に渡す。
【００３４】
例えば、図２に示すように、クラス１に対応付け可能なステートマシン１，２，３のうち、特定のステートマシン２が選択されると、クラス１とステートマシン２とが対応付けられた検査対象モデルが設定される（図２の実線矢印参照）。なお、モデル設定部１４は、後述するように検査結果記憶部１８に記憶されているクラスと特定のステートマシンとの組み合わせが既に設定された検査対象モデルを読み出して、検査実行部１５による検査を実行する新たな検査対象モデルとして設定することができる。さらに、モデル設定部１４は、既にクラスとステートマシンとの組み合わせが設定されている検査対象モデルに対して、そのクラスに対応付け可能な他の特定のステートマシンの選択を受け付けて、その組み合わせを変更して新たな検査対象モデルを設定することができる。
【００３５】
なお、上記モデル設定部１４は、例えば、クラスに関連するステートマシンの一覧を表示し、この一覧の中から利用者にて選択された特定のステートマシンをクラスに対応付けて、検査対象モデルを設定する。また、モデル設定部１４では、後述する検査実行部１５にて検査を実行する際に用いる検査式を選択することもできる。
【００３６】
次に、検査実行部１５（検査実行手段）について説明する。検査実行部１５は、上記モデル設定部１４にてクラスとステートマシンとの組み合わせが設定された検査対象モデルの検査を実行する。例えば、検査実行部１５は、検査対象モデル情報を形式的な使用記述に自動的に変換し、かかる記述が、予め定められた検査式を満たしているかどうか検査する。なお、検査式は、検査内容を示す情報であって、仕様に要求される性質を論理式で記述したものであり、例えば、検査実行部１５に組み込まれて記憶されていたり、あるいは、モデル検査装置１の記憶装置内に記憶されている。
【００３７】
また、検査実行部１５は、検査対象モデルが検査式を満たすかどうかを検査すると共に、当該検査の実行時間を計測する。そして、検査対象モデルの構成つまりクラスとステートマシンとの組み合わせを示す検査対象モデル情報、検査式、検査により検査式を満たしたかどうかを表す結果、及び、計測した実行時間を含む検査結果、を関連付けて、検査結果記憶部１８（検査対象モデル記憶手段）に記憶する。また、検査実行部１５は、上記検査結果記憶部１８に記憶する検査対象モデル情報や検査結果の情報を、表示部１２に出力する機能も有する（検査結果出力手段）。
【００３８】
ここで、検査結果記憶部１８に記憶される情報の一例を図６に示す。この図に示すように、検査実行部１５は、検査の実行単位であるクラスとステートマシンとの組み合わせが設定された検査対象モデル毎に、検査名（検査１，２）を付けて、各クラスに対応付けた各ステートマシンと、検査式と、検査の実行時間と、を関連付けて記憶する。なお、実行時間は、過去に検査を実行している場合には、過去に計測した実行時間の平均値を記憶する。また、過去に実行していない検査については、実行時間は空欄である。
【００３９】
また、図７に、実行した検査の検査結果を表示部１２に表示したときの一例を示す。この図に示すように、表示例も、上記図６と同様に、検査の実行単位である検査対象モデルの検査名（検査１，２）毎に、各クラスに対応付けた各ステートマシンと、検査式と、検査の実行時間と、を関連付けて表示する。
【００４０】
なお、図７に示すように、各検査の組み合わせ、検査式、実行時間が表示された状態で、利用者が操作部１１を操作することで、クラスに対応付けるステートマシンの選択、検査式の選択、さらには、検査単位の削除、の指示を入力することができる。このとき、例えば、図８に示すように、クラスに対応付け可能なステートマシンの一覧をプルダウンメニューにて表示し、特定のステートマシンを選択可能とする。そして、特定のステートマシンの選択入力をモデル設定部１４が受け付けて、当該特定のステートマシンをクラスに対応付け、新たな検査つまり検査対象モデルとして設定する。かかる場合には、図８に示すように、各検査の実行時間が表示されるため、利用者は各組み合わせの実行時間を参照して、クラスとステートマシンとの組み合わせを変更設定することができる。
【００４１】
また、上記検査実行部１５は、予め検査の実行時間の上限値が記憶されており、実行している検査の実行時間が、上記実行時間の上限値を越えると、検査の実行を停止する機能を有する。なお、実行時間の上限値は、予め設定された値がモデル検査装置１内に記憶されていてもよく、あるいは、利用者から操作部１１を介して入力された上限値がモデル検査装置１内に記憶されてもよい。
【００４２】
次に、検査情報検索部１６（検査検索手段）について説明する。検査情報検索部１６は、検査結果記憶部１８に記憶されている検査から、所定の条件を満たす検査を検索して読み出し、モデル設定部１４に通知する。例えば、検査一覧の中から選択された所望の検査を検索したり、あるいは、所望の実行時間を指定して、当該指定された実行時間以内の実行時間が記憶された検査を検索する。そして、検索された検査の通知を受けたモデル設定部１４は、検索された検査を表示部１２に出力したり、検査実行部１５による検査対象として設定する。このように、モデル設定部１４は、検査結果出力手段としても機能する。なお、この場合も、モデル設定部１４は、上述同様に、検索された検査のクラスに対応付けされたステートマシンを変更するよう他のステートマシンの選択入力を利用者から受け付けると、この選択された他のステートマシンとクラスとを対応付けた組み合わせに変更する。
【００４３】
［動作］
次に、上記構成のモデル検査装置１の動作を、図９乃至図１１のフローチャートを参照して説明する。まず、利用者は、操作部１１から、クラスと当該クラスに対応付け可能なステートマシンとを作成する情報を入力してモデルを作成する（ステップＳ１）。これを受けたモデル検査装置１は、入力されたクラスとステートマシンとを、モデル情報記憶部１７に記憶する（モデル情報記憶処理工程）。なお、クラスとステートマシンとにより構成されているモデル情報は、必ずしも利用者によって作成されることに限定されない。例えば、既存のモデル情報をモデル検査装置１に記憶してもよい。
【００４４】
続いて、モデル検査装置１は、モデル情報記憶部１７内に記憶されているクラス及び当該クラスに対応付けられている全ての詳細度のステートマシンを取得し、表示部１２に表示する。つまり、１つのクラスに複数の詳細度の異なるステートマシンが関連付けられている場合には、全てのステートマシンを選択可能なよう表示する。かかる表示に対して、利用者は、各クラスに対応付ける特定のステートマシンをそれぞれ選択する（ステップＳ２）。このとき、例えば、図８に示すように、クラスに対応付け可能なステートマシンをプルダウンメニューにて表示することで、この中から利用者は選択することができる。
【００４５】
そして、モデル検査装置１は、選択されたステートマシンとクラスとの組み合わせからなる検査対象モデルを設定する（ステップＳ３、検査対象モデル設定工程）。なお、ここでは、詳細度の低い概要設計レベルのステートマシンが選択されたこととする。また、利用者は、検査に用いる検査式も選択する。
【００４６】
続いて、モデル検査装置１は、上記設定された検査対象モデルつまりクラスと選択されたステートとの組み合わせ、さらには、選択した検査式を記憶する（検査対象モデル記憶処理工程）。そして、かかる組み合わせによる検査対象モデルの検査を実行する（ステップＳ４、検査実行工程）。具体的には、検査対象モデルが検査式を満たすかどうかを検査する検査プログラムを作成し、当該検査プログラムを実行して検査を行う。このとき、検査の実行時間を計測する。そして、検査が終了すると、モデル検査装置１は、検査結果である実行時間を、かかる検査のクラスとステートマシンとの組み合わせ及び検査式と共に、記憶しておく（ステップＳ５）。なお、この実行時間を記憶するときにはじめて、検査対象モデルの構成であるクラスとステートマシンとの組み合わせ及び検査式を記憶してもよい（検査対象モデル記憶処理工程）。
【００４７】
続いて、モデル検査装置１は、図７に示すように、検査を行った検査対象モデルのクラスとステートマシンとの組み合わせ、検査式、実行時間、を表示部１２に表示出力する（ステップＳ６、検査結果出力工程）。これにより、利用者は、検査を行ったモデルの構成と検査結果とを確認することができる。なお、このとき、ステートマシンとして概要設計レベルのステートマシンを選択した場合であって、検査結果に問題が無いこととする。これを確認した利用者は、さらに詳細設計に進むこととする（ステップＳ７でイエス）。
【００４８】
続いて、利用者は、クラスに対応付けるステートマシンを詳細設計レベルのものにすべく、まず、詳細設計レベルのステートマシンを作成する（図１０のステップＳ１１でノー、Ｂに進む、図９のステップＳ１）。すると、モデル検査装置１は、詳細設定のステートマシンを記憶し、これを選択可能なよう表示部１２に表示する。例えば、図８に示すように、新たに作成した詳細設計レベルのステートマシンをプルダウンメニューに表示し、利用者がこれを選択することで（ステップＳ２）、モデル検査装置１は、当該選択されたステートマシンとクラスとの組み合わせからなる検査対象モデルを設定する（ステップＳ３）。また、利用者は、検査に用いる検査式も選択する。なお、詳細設計レベルのステートマシンが予め記憶されている場合には、上記ステップＳ１は省略される。
【００４９】
続いて、モデル検査装置１は、上述同様に、クラスに上記詳細設計レベルのステートマシンが対応付けられた検査対象モデル、及び、選択した検査式を記憶すると共に、かかる組み合わせによる検査対象モデルの検査を実行する（ステップＳ４）。そして、検査が終了すると、モデル検査装置１は、検査結果である実行時間を、かかる検査のクラスとステートマシンとの組み合わせ及び検査式と共に記憶し（ステップＳ５）、図７に示すように、検査を行った検査対象モデルのクラスとステートマシンとの組み合わせ、検査式、実行時間、を表示部１２に表示出力する（ステップＳ６）。
【００５０】
以上により、利用者は、検査対象モデルとして、クラスに対応付ける特定のステートマシンを選択することができるため、種々の組み合わせで検査を実行することができる。また、このとき検査の実行時間を確認しながら組み合わせを設定できるため、効率的な検査を実行することができる。
【００５１】
ここで、検査に非常に時間がかかるか、もしくは、途中で状態爆発が発生した場合には、図１０の処理に進む。まず、記憶されている実行した検査の検査対象モデルを読み出し、図７に示すように表示する（ステップＳ１２）。そして、あるクラスのステートマシンを、詳細設計レベルから概要設計レベルのものに変更するよう選択し（ステップＳ１３でイエス、ステップＳ１４）、クラスとステートマシンとの組み合わせを変更設定する。一例として、図３乃至図５に示したクラスＡ，Ｂ，Ｃ及び各ステートマシンの場合を考える。この例では、「Counter Up」でCounterを増やし、「Counter ＞ COND」でCounterが条件値CONDを超えているかを判定するカウンタ計算があり、状態数が増える原因となる。従って、上記のステートマシンを使用した場合に、検査の実行時間がかかる場合、クラスＡの検査の優先度が高ければ、当該クラスＡについては図５（ａ）に示す詳細設計レベルのステートマシンをそのまま使用し、クラスＢとＣについては、図４（ｂ），（ｃ）に示す概要設計レベルのステートマシンに切り替える。
【００５２】
そして、変更した検査対象モデルにて、再度モデル検査を実行する（ステップＳ１５でＣに進む、図９のステップＳ４）。検査が終了すると、上述したように、モデル検査装置１は、検査結果である実行時間を、かかる検査のクラスとステートマシンとの組み合わせ及び検査式と共に記憶し（ステップＳ５）、図７に示すように、組み合わせを変更設定した検査対象モデルのクラスとステートマシンとの組み合わせ、検査式、実行時間、を表示部１２に表示出力する（ステップＳ６）。
【００５３】
以上により、本実施形態では、利用者が検査の実行時間を参照して、詳細度の異なるステートマシンの切り替えを容易に行うことができるため、検査時間の軽減と状態爆発の回避を行うことができる。つまり、検査の精度と実行時間のバランスを考慮した最適なモデル検査を実行することができる。例えば、モデルを詳細化するうちに検査時間の増加が問題になった場合に、検査にあまり影響のない部分のステートマシンを概要設計時のものに戻すことで、検査の精度の落とさずに検査時間を削減することが可能である。また、検査の実施計画に応じて、検査したいことと実行時間のバランスを考えて、最適な検査を効率的に選択することができ、その結果を保存しておくことが可能であるため、モデル検査を回帰テストとして行うことが容易になる。
【００５４】
なお、利用者は、モデル検査装置１に検索条件を入力することで、過去に検査を行ったもののうち、条件を満たす検査を閲覧、あるいは、再検査行うことができる。例えば、「全ての検査」という検索条件を入力することで、検査一覧を表示することができる。そして、利用者は、一覧の中から所望の検査を選択することで、モデル検査装置１は、表示部１２に、図７に示すように、選択された検査の組み合わせ、検査式、実行時間を表示する。この検査に対して、上述したように利用者は、図８に示すよう、あるクラスに対応付けるステートマシンの変更も可能であり、種々の構成の検査を実行することができる。
【００５５】
また、図１１に示すように、利用者は、ある時間以内の検査を検索したとする。この場合に、利用者は、モデル検査装置１に対して、実行時間の上限値を指定して入力する（ステップＳ２１）。すると、モデル検査装置１は、入力された実行時間の上限値以内の実行時間を有する検査を、検査結果記憶部１８内から検索する（ステップＳ２２）。そして、モデル検査装置１は、検索された検査対象モデルの組み合わせ、検査式、実行時間、を図７のように表示する。これにより、利用者は実行時間に基づいて効率よく検査を実行することができる。
【００５６】
＜実施形態２＞
次に、本発明の第２の実施形態を、図１２を参照して説明する。図１２は、本実施形態におけるモデル検査装置１の構成を示す機能ブロック図である。
【００５７】
本実施形態におけるモデル検査装置１は、上記実施形態１におけるモデル検査装置に、さらに、演算装置に所定のプログラムが組み込まれることで構成された検査シナリオ設定部１９を備えている。また、記憶装置には、検査シナリオ記憶部２０が形成されている。
【００５８】
上記検査シナリオ設定部１９（検査順序設定手段）は、利用者が操作部１１から入力した検査の順序を設定する情報に基づいて、複数の検査を実行する順序を設定し、この一連の検査を１つの検査対象シナリオとする。例えば、「検査１」と「検査２」がある場合に、その順序を「検査２」、「検査１」と設定し、また、かかる順序の検査郡のシナリオ名を設定する。そして、設定したシナリオの名前と、各検査の名前を設定された検査順序で表したリストと、を検査シナリオ記憶部２０に記憶する。
【００５９】
その後、検査実行タイミングとなると、検査実行部１５は、検査対象シナリオの内容を読み出して、当該シナリオに含まれる各検査を、設定された検査順序で検査を実行する。そして、上述したように、順番に実行された各検査の結果を記憶したり、表示出力する。
【００６０】
なお、一部の検査の実行時間が非常に大きく、すべての検査が終わらないことを防止するため、上述同様に、実行時間についての上限値を設定するとよい。かかる場合には、検査の実行時間が、設定された実行時間の上限値を越えた場合、そこで検査を打ち切って次の検査に進むよう作動する。
【００６１】
これにより、複数の検査対象モデルを、設定した順序でまとめて検査することができ、検査のさらなる効率化を図ることができる。
【産業上の利用可能性】
【００６２】
本発明は、モデル検査において、検査の実行時間を確認しながら状態遷移を切り替えて、適切なモデル検査を選び出すという用途に好適である。また、検査という単位で状態遷移の組合せを保存し、複数の検査をシナリオに従って再実行する用途に好適である。
【図面の簡単な説明】
【００６３】
【図１】実施形態１におけるモデル検査装置の構成を示す機能ブロック図である。
【図２】モデル検査装置に記憶されるモデルの構成の一例を示す図である。
【図３】クラスの一例を示す図である。
【図４】概要設計レベルのステートマシンの一例を示す図である。
【図５】詳細設計レベルのステートマシンの一例を示す図である。
【図６】モデル検査装置に記憶されるモデル検査結果の一例を示す図である。
【図７】モデル検査装置に表示される画面の一例を示す図である。
【図８】モデル検査装置に表示される画面の一例を示す図である。
【図９】モデル検査装置の動作を示すフローチャートである。
【図１０】モデル検査装置の動作を示すフローチャートである。
【図１１】モデル検査装置の動作を示すフローチャートである。
【図１２】実施形態２におけるモデル検査装置の構成を示す機能ブロック図である。
【符号の説明】
【００６４】
１  モデル検査装置
１１  操作部
１２  表示部
１３  モデル作成部
１４  モデル設定部
１５  検査実行部
１６  検査情報検索部
１７  モデル情報記憶部
１８  検査結果記憶部
１９  検査シナリオ設定部
２０  検査シナリオ記憶部
【図１】
2009223711.tif 000003
【図２】
2009223711.tif 000004
【図３】
2009223711.tif 000005
【図４】
2009223711.tif 000006
【図５】
2009223711.tif 000007
【図６】
2009223711.tif 000008
【図７】
2009223711.tif 000009
【図８】
2009223711.tif 000010
【図９】
2009223711.tif 000011
【図１０】
2009223711.tif 000012
【図１１】
2009223711.tif 000013
【図１２】
2009223711.tif 000014