(57)【要約】【課題】複数の性質情報からなる性質情報群に対するシステムの動作主体の動作仕様の検査を効率良く実施可能とする。【解決手段】入力された動作主体の動作仕様情報１００は検査指示部７の検査制御部１３に供給され、入力された性質情報群の性質情報１０１は、性質上記録部６で記録された後、検査制御部１３に読み取られる。検査制御部１３は、この性質情報１０１を基に、モデル検査部３ａ，３ｂ，……での動作仕様情報１００の検査計画情報１０６を作成し、この検査部計画情報１０６のもとに、性質情報１０１をモデル検査部３ａ，３ｂ，……に割り振って動作仕様情報１００が性質情報を満たしているか否かの検査を行なわせる。ここでは、一例として、モデル検査部３ａ，３ｂ，……毎に異なる性質情報１０１ａ，１０１ｂ，１０１ｃを割り振り、これらで同時に動作仕様情報１００の検査を行なう。【選択図】図５
2010277533.tif 000002
【特許請求の範囲】
【請求項１】
システムの動作主体の動作仕様情報を性質情報群の夫々の性質情報毎に該性質情報を満たすか否かを検査する仕様検査装置であって、
該動作仕様情報と該性質情報群とを入力し、かつ得られた検査情報を出力する入出力部と、
該入出力部から入力された該性質情報群の各性質情報を性質情報記録テーブルに記録する性質情報記録部と、
複数のモデル検査部と、
該複数のモデル検査部での該性質情報による該動作仕様情報の検査を指示する検査指示部と
を備えたことを特徴とする仕様検査装置。
【請求項２】
請求項１において、
１以上の前記モデル検査部に前記性質情報を夫々割り振り、前記性質情報が割り振られた前記モデル検査部で前記動作仕様情報の検査を行なうことを特徴とする仕様検査装置。
【請求項３】
請求項２において、
検査が終了した前記モデル検査部に、前記モデル検査部に割り振られていない前記性質情報と前記動作仕様情報とを割り振って当該動作仕様情報の検査を行なうことを特徴とする仕様検査装置。
【請求項４】
請求項１において、
同じ前記性質情報を２以上の前記モデル検査部に、前記動作仕様情報とともに、割り振り、これらモデル検査部のいずれか１つで当該動作仕様情報の検査が終了すると、当該性質情報を用いた検査中の他の前記モデル検査部の検査を途中で停止させることを特徴とする仕様検査装置。
【請求項５】
請求項４において、
前記モデル検査部毎にモデル検査プログラムの検査方式が異なることを特徴とする仕様検査装置。
【請求項６】
請求項１に記載の仕様検査装置において、
前記モデル検査部にモデル検査プログラムのオプションが設定可能であって、
同じ前記性質情報を２以上の前記モデル検査部に、前記動作仕様情報とともに、割り振り、
前記モデル検査部で設定されたオプションに応じた検査結果が得られたときには、当該性質情報を用いた検査中の他の前記モデル検査部の検査を途中で停止させ、
前記モデル検査部で設定されたオプションに応じない検査結果が得られたときには、当該性質情報を用いた検査中の他の前記モデル検査部の検査を継続させる
ことを特徴とする仕様検査装置。
【請求項７】
請求項６において、
前記モデル検査部としては、モデル検査プログラムに応じて、前記動作仕様情報が当該性質情報を満たさないとの検査結果は確実であるが、前記動作仕様情報が当該性質情報を満たすとの検査結果は保証されない第１のモデル検査部と、前記動作仕様情報が当該性質情報を満たすとの検査結果と前記動作仕様情報が当該性質情報を満たさないとの検査結果とが確実である第２のモデル検査部とがあり、
前記検査指示部は、
該第１のモデル検査部からの検査結果が前記動作仕様情報が当該性質情報を満たさないとの検査結果であるとき、該検査結果を有効として、その他のモデル検査部の検査実行を停止させ、
該第１のモデル検査部からの検査結果が前記動作仕様情報が当該性質情報を満たす検査結果であるとき、該第２のモデル検査部の検査を継続させ、その検査結果を有効とする
ことを特徴とする仕様検査装置。
【請求項８】
請求項４，５または６において、
前記検査指示部は、検査実行中の前記モデル検査部からの検査経過情報と検査を商量した前記モデル検査部からの検査結果情報とをもとに、検査実行中の前記モデル検査部の検査を途中停止させることを特徴とする仕様検査装置。
【請求項９】
請求項１〜６のいずれか１つにおいて、
前記モデル検査部での前記性質情報による前記動作仕様情報の検査結果を、前記性質情報記録テーブルにおいて、該当する前記性質情報と関連付けて記録する
ことを特徴とする仕様検査装置。
【請求項１０】
請求項１〜９のいずれか１つにおいて、
前記検査指示部は、前記入出力部から入力された前記性質情報群の性質情報元に、前記性質情報の検査計画情報を作成し、
該検査計画情報を基に、前記性質情報の前記モデル検査部への割り振りを行ない、前記モデル検査部からの検査結果を取得する毎に該検査計画情報を更新して、次の前記性質情報の前記モデル検査部への割り振りを行なう
ことを特徴とする仕様検査装置。
【請求項１１】
請求項１〜１０のいずれか１つに記載の仕様検査装置において、
前記入出力部で入力された前記性質情報群の夫々の性質情報を変換処理し、新たな変換性質情報を作成する性質変換部を設け、
該性質変換部で作成された該変換性質情報を前記性質情報記録部の前記性質情報記録テーブルに記録し、前記性質情報群に該変換性質情報を追加する
ことを特徴とする仕様検査装置。
【請求項１２】
請求項１１において、
前記性質変換部は、予め変換ルールが設定されており、前記入出力部で入力されて前記性質情報記録部で前記性質情報記録部に記録されている前記性質情報を該変換ルールを基に変換することにより、前記変換性質情報を作成することを特徴とする仕様検査装置。
【請求項１３】
請求項１１または１２において、
前記性質変換部は、前記性質情報を、これと論理的に等価な論理式で変換して前記変換性質情報を形成することを特徴とする仕様検査装置。
【請求項１４】
請求項１１または１２において、
前記性質変換部は、前記性質情報の論理的帰結により、前記変換性質情報を形成することを特徴とする仕様検査装置。
【請求項１５】
請求項１１または１２において、
前記性質変換部は、前記性質情報をそれを構成する要素に分割し、分割した外装素価らなる前記変換性質情報を形成することを特徴とする仕様検査装置。
【請求項１６】
請求項１１〜１５のいずれか１つにおいて、
前記性質変換部は、前記変換性質情報に対して再帰的に変換処理を行なうことを特徴とする仕様検査装置。
【請求項１７】
請求項１〜１６において、
前記複数のモデル検査部は計算能力が異なり、
前記性質情報の構造が複雑なほど、計算能力が高い前記モデル計算部に優先的に割り付ける
ことを特徴とする仕様検査装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、システムなどの動作主体の動作仕様を検査する仕様検査装置に関する。
【背景技術】
【０００２】
システムの振舞い（動作）、特に、システムを構成する複数の動作主体（例えば、複数の動作を実行する複数の機構からなる装置において、１つの動作を実行する機構の組み合わせが１つの動作主体であり、このように、複数の動作を実行する場合には、複数の動作主体がある）が事象のやり取りを介して連携しつつ、並行、並列に動作することによるシステムの振舞いは複雑である。このような分野の典型的なシステムとしては、ネットワークを介して通信プロトコルシステムや並行動作するハードウェア（装置など）をソフトウェアが制御する組込みシステムがある。このようなシステムでの各動作主体は、事象の同期的なやり取りのほかは独立して動作する。そのため、複数の動作主体間の事象のやり取りの内容によってシステムの振舞いが決定するだけでなく、やり取りの順序やタイミングにより、システムの振舞いが変化し得る。
【０００３】
このようなシステムを開発する場合には、各動作主体の動作を定義した動作仕様書を作成し、これを検査することが一般に行なわれる。各動作主体の動作の定義には、状態遷移モデルやシーケンス図，ＵＭＬなどが用いられる。システムの動作時における、事象のやり取りの内容、各動作主体間のやり取りの順序やタイミングの組み合わせが膨大となり、可能なシステムの振舞いが多数存在する。
【０００４】
システムの可能な振舞いを網羅的かつ自動的に分析する技術として、モデル検査技術が知られている。かかるモデル検査技術とは、予めシステムを構成する動作主体の動作仕様情報を専用言語で記述し、これとは別に、システムプログラムが満たすべき性質情報を数学的な記法を用いて記述し、この動作仕様情報がこの性質情報を満たしているか否かを数学的に検査する技術である。モデル検査を実行するプログラムをモデル検査プログラムということにする。かかるモデル検査技術を実装した代表的なモデル検査プログラムとしては、ＳＰＩＮ（Simple Promela Interpreter）（例えば、非特許文献１及び非特許文献２参照）やＳＭＶ（Symbolic Model Checher）（例えば、非特許文献３参照），ＵＰＰＡＡＬ（例えば、非特許文献４参照）などが知られている。
【０００５】
モデル検査プログラムは、動作主体の動作仕様情報が性質情報を満たさない状態に至ることがある場合、その性質情報を満たさない状態に至るプログラムの動作過程を出力する。このように、モデル検査プログラムが出力する性質情報を満たさない状態に至るプログラムの動作過程を反例という。
【０００６】
モデル検査プログラムは、並行、並列に動作する複数の動作主体からなるシステムの可能な振舞いを網羅的に探索するものであることから、大規模なシステムの振舞いを検査する場合には、時間と計算機の記憶領域を大量に必要とするという問題がある。
【０００７】
かかる問題を解決するために、各モデル検査プログラムでは、探索を効率的に行なう技術が開発されている。その一例として、モデル検査プログラムの１つであるＳＰＩＮでは、計算機のＣＰＵのマルチコアに対応し、探索を分割して処理することで探索効率を向上させる技術が知られている（例えば、非特許文献２参照）。他の例としては、ＳＭＶでＢＤＤ（Binary Decision Diagram）とＳＡＴ（SATisfiability Probrem）ソルバと呼ばれる技術を用いて探索効率の向上をはかるようにした技術も知られている（例えば、非特許文献３参照）。さらにその他の例としては、ＳＡＴソルバを用いたモデル検査方法（例えば、特許文献１）やＢＤＤを用いたモデル検査方法（例えば、特許文献２参照），状態集合の分割を用いたモデル検査方法（例えば、特許文献３参照）なども知られている。
【０００８】
これらのモデル検査技術は、単独の性質情報に対するモデル検査を時間もしくは計算機の記憶領域に関して効率的に実現するものである。
【先行技術文献】
【特許文献】
【０００９】
【特許文献１】特開２００４−５６７４号公報
【特許文献２】特開平１１−３２８２３６号公報
【特許文献３】特開平１０−３０１９６３号公報
【非特許文献１】G.J.Halzmann著 「The SPIN model checker：Primer and reference manual」Addison Wesiey, 2000年
【非特許文献２】中島 震著  「ＳＰＩＮモデル  検証モデリング技法」２００８年
【非特許文献３】A.Cimatti, E.Giunchiglia, M.Roveri, M.Pistore,R.Sebastiani and A.Tacchella. 「Integrating BDD-based and SAT-Based Symbolic Model Checking」 Proceedings of 4th International Workshop on Frontiers of Combining Systems, 2002年
【非特許文献４】G.Behrmann et.al 「A Tutorial on UPPAAL」 In proceeding of the 4th International School on Formal Methods for the Design of Computer,Communication,and Software Systems(SFM-RT'04). LNCS 3185 2004年
【非特許文献５】G.J.Halzmann,D.Bosnacki著 「The Design of Multicore Extenstion of the SPIN MODEL CHECKER」 IEEE TRANSACTIONS OF SOFTWARE ENGINNERING VOL.33 No.10 pp.659-674,2007年
【発明の概要】
【発明が解決しようとする課題】
【００１０】
システムが満たすべき性質は、一般に複数存在する。また、システムへの要求は複数である。例えば、モデル検査において、検査される一般的な性質である到達可能性（ある状態から他の状態に必ず到達することを意味する性質）は、システムが有する状態の組み合わせだけ性質が存在し得る。そのほか、一般にシステムは複数の要求を実現するものであり、これら複数の要求がモデル検査で検査する性質となり得る。しかし、多数の性質をモデル検査技術を用いて検査することは、検査に時間を要することになる。
【００１１】
上記の各特許文献や非特許文献で示されるモデル検査技法は、単一の性質に対するモデル検査に関するものであり、複数の性質の集合である性質群に対するモデル検査のかかる課題を解決するものではない。
【００１２】
本発明は、かかる点に鑑みてなされたものであって、その目的は、複数の性質からなる性質群に対するシステムの動作主体の動作仕様の検査をを効率良く実施可能とした仕様検査装置を提供することにある。
【課題を解決するための手段】
【００１３】
上記目的を達成するために、本発明は、システムの動作主体の動作仕様情報を性質情報群の夫々の性質情報毎に性質情報を満たすか否かを検査する仕様検査装置であって、動作仕様情報と性質情報群とを入力し、かつ得られた検査情報を出力する入出力部と、入出力部から入力された性質情報群の各性質情報を性質情報記録テーブルに記録する性質情報記録部と、複数のモデル検査部と、複数のモデル検査部での性質情報による動作仕様情報の検査を指示する検査指示部とを備えたことを特徴とする。
【００１４】
また、本発明は、１以上のモデル検査部に性質情報を夫々割り振り、性質情報が割り振られたモデル検査部で動作仕様情報の検査を行なうことを特徴とする。
【００１５】
また、本発明は、検査が終了したモデル検査部に、モデル検査部に割り振られていない性質情報と動作仕様情報とを割り振って当該動作仕様情報の検査を行なうことを特徴とする。
【００１６】
また、本発明は、同じ性質情報を２以上のモデル検査部に、動作仕様情報とともに、割り振り、これらモデル検査部のいずれか１つで当該動作仕様情報の検査が終了すると、当該性質情報を用いた検査中の他のモデル検査部の検査を途中で停止させることを特徴とする。
【００１７】
また、本発明は、モデル検査部毎にモデル検査プログラムの検査方式が異なることを特徴とする。
【００１８】
また、本発明は、モデル検査部にモデル検査プログラムのオプションが設定可能であって、同じ性質情報を２以上のモデル検査部に、動作仕様情報とともに、割り振り、モデル検査部で設定されたオプションに応じた検査結果が得られたときには、当該性質情報を用いた検査中の他のモデル検査部の検査を途中で停止させ、モデル検査部で設定されたオプションに応じない検査結果が得られたときには、当該性質情報を用いた検査中の他のモデル検査部の検査を継続させることを特徴とする。
【００１９】
また、本発明は、モデル検査部としては、モデル検査プログラムに応じて、動作仕様情報が当該性質情報を満たさないとの検査結果は確実であるが、動作仕様情報が当該性質情報を満たすとの検査結果は保証されない第１のモデル検査部と、動作仕様情報が当該性質情報を満たすとの検査結果と動作仕様情報が当該性質情報を満たさないとの検査結果とが確実である第２のモデル検査部とがあり、検査指示部は、第１のモデル検査部からの検査結果が動作仕様情報が当該性質情報を満たさないとの検査結果であるとき、検査結果を有効として、その他のモデル検査部の検査実行を停止させ、第１のモデル検査部からの検査結果が動作仕様情報が当該性質情報を満たす検査結果であるとき、第２のモデル検査部の検査を継続させ、その検査結果を有効とすることを特徴とする。
【００２０】
また、本発明は、検査指示部が、検査実行中のモデル検査部からの検査経過情報と検査を商量したモデル検査部からの検査結果情報とをもとに、検査実行中のモデル検査部の検査を途中停止させることを特徴とする。
【００２１】
また、本発明は、モデル検査部での性質情報による動作仕様情報の検査結果を、性質情報記録テーブルにおいて、該当する性質情報と関連付けて記録することを特徴とする。
【００２２】
また、本発明は、検査指示部が、入出力部から入力された性質情報群の性質情報元に、性質情報の検査計画情報を作成し、検査計画情報を基に、性質情報のモデル検査部への割り振りを行ない、モデル検査部からの検査結果を取得する毎に検査計画情報を更新して、次の性質情報のモデル検査部への割り振りを行なうことを特徴とする。
【００２３】
また、本発明は、入出力部で入力された性質情報群の夫々の性質情報を変換処理し、新たな変換性質情報を作成する性質変換部を設け、性質変換部で作成された変換性質情報を性質情報記録部の性質情報記録テーブルに記録し、性質情報群に変換性質情報を追加することを特徴とする。
【００２４】
また、本発明は、性質変換部が、予め変換ルールが設定されており、入出力部で入力されて性質情報記録部で性質情報記録部に記録されている性質情報を変換ルールを基に変換することにより、変換性質情報を作成することを特徴とする。
【００２５】
また、本発明は、性質変換部が、性質情報を、これと論理的に等価な論理式で変換して変換性質情報を形成することを特徴とする。
【００２６】
また、本発明は、性質変換部が、性質情報の論理的帰結により、変換性質情報を形成することを特徴とする。
【００２７】
また、本発明は、性質変換部が、性質情報をそれを構成する要素に分割し、分割した外装素価らなる変換性質情報を形成することを特徴とする。
【００２８】
また、本発明は、性質変換部が、変換性質情報に対して再帰的に変換処理を行なうことを特徴とする。
【００２９】
また、本発明は、複数のモデル検査部が計算能力が異なり、性質情報の構造が複雑なほど、計算能力が高いモデル計算部に優先的に割り付けることを特徴とする。
【発明の効果】
【００３０】
本発明によれば、システムの動作主体の動作仕様情報が性質情報を満たすか否かの検査を、複数のモデル検査部を用いて並行，並列に行なわれるものであるから、かかる検査に要する時間を大幅に短縮することができる。
【図面の簡単な説明】
【００３１】
【図１】本発明による仕様検査装置の第１の実施形態の全体構成を示すブロック構成図である。
【図２】図１における入出力部の一具体例を示すブロック構成図である。
【図３】図２における性質情報記録部での性質情報の記録状態を示す図である。
【図４】図１におけるモデル検査部の一具体例を示すブロック構成図である。
【図５】図２における検査指示部の一具体例を示すブロック構成図である。
【図６】図５における検査計画情報の一具体例を示す図である。
【図７】図５における検査部情報の一具体例を示す図である。
【図８】図５における検査制御部の処理の流れの一具体例を示すフローチャートである。
【図９】図８におけるステップＳ１０８の一具体例を示すフローチャートである。
【図１０】本発明による仕様検査装置の第２の実施形態での検査計画情報の一具体例を示す図である。
【図１１】本発明による仕様検査装置の第２の実施形態における検査制御部の処理の流れの一具体例を示すフローチャートである。
【図１２】図１１におけるステップ２０２の一具体例を示すフローチャートである。
【図１３】本発明による仕様検査装置の第３の実施形態での検査部情報の一具体例を示す図である。
【図１４】本発明による仕様検査装置の第４の実施形態における検査指示部の一具体例を示すブロック構成図である。
【図１５】図１４における性質変換部の一具体例を示すブロック構成図である。
【図１６】図１５における性質変換ルール部の一具体例を示す図である。
【図１７】図１４及び図１５における性質変換部で得られた変換性質情報が追加されて拡張された性質情報記録部の性質情報記録テーブル一具体例を示す図である。
【図１８】図１５に示す性質変換部の処理の流れの一具体例を示すフローチャートである。
【図１９】図１４における検査制御情報の一具体例を示す図である。
【図２０】図１４及び図１９に示す検査制御情報を用いた図１４における検査制御部の処理の流れを示すフローチャートである。
【発明を実施するための形態】
【００３２】
以下、本発明の実施形態を図面を用いて説明する。
【００３３】
なお、以下では、検査の対象となるシステムを構成する動作主体の動作を定義した情報を動作仕様情報といい、この動作仕様情報は夫々、１つの動作主体の動作を定義するものであるが、複数の動作主体の互いに関連しあった動作を定義したものも含む。また、検査の対象となるシステムが満たすべき性質を定義した情報を性質情報といい、性質情報は１つの性質を定義したものであって、かかる性質情報の集合を性質情報群という。
【００３４】
〔第１の実施形態〕
図１は本発明による仕様検査装置の第１の実施形態の全体構成を示すブロック構成図であって、１は仕様検査装置、２は入出力部、３ａ，３ｂ，３ｃはモデル検査部、４は情報伝達路、１００は動作仕様情報、１０１は性質情報、１０２は性質情報群、１０３は検査情報である。
【００３５】
同図において、この実施形態の仕様検査装置１は、入出力部２とモデル検査部３ａ〜３ｃとを有しており、入出力部２とモデル検査部３ａ〜３ｃとが情報伝達路４によって接続されている。ここでは、モデル検査部３（モデル検査部の総称）としては、３個のモデル検査部３ａ〜３ｃを有するものとするが、１個でもよいし、２以上の任意の複数個であってもよい。
【００３６】
入出力部２には、検査の対象となる１つの動作仕様情報１００と、この動作仕様情報１００を検査するための１〜複数の性質情報１０１の集合の性質群１０２とが入力され、また、モデル検査部３ａ〜３ｃの検査結果が検査情報１０３として出力される。
【００３７】
モデル検査部３ａ〜３ｃには、入出力部２に入力された動作仕様情報１００と性質情報群１０２の性質情報１０１とが情報伝達路４を介して供給され、モデル検査部３ａ〜３ｃ毎にこの動作仕様情報１００が性質情報１０１を満たすか否かの検査を行なう。これらモデル検査部３ａ〜３ｃによる検査は、入出力部２から情報伝達路４を介した指示により実行される。この第１の実施形態では、性質情報群１０２の各性質情報がモデル検査部３ａ〜３ｃに夫々分配され、また、同じ動作仕様情報１００がこれらモデル検査部３ａ〜３ｃに供給される。これにより、モデル検査部３ａ〜３ｃの夫々では、異なる性質情報毎に、動作仕様情報１００がこのときのモデル検査部３に割り当てられた性質情報を満たしているか否か検査が行なわれる。
【００３８】
モデル検査部３からは、検査の途中（検査中）であることを示す検査の途中経過情報や検査結果を示す検査結果情報を、情報伝達路４を介して、入出力部２に供給する。入出力部２は、モデル検査部３ａ〜３ｃからの検査の途中経過情報や検査結果情報を、検査情報１０３として、出力する。
【００３９】
モデル検査部３ａ〜３ｃには、モデル検査プログラムを用いることができる。代表的なモデル検査プログラムとして、ＳＰＩＮがある。この第１の実施形態では、モデル検査部３ａ〜３ｃにＳＰＩＮを用いるものとするが、これに限定するものではなく、ＳＭＶやＵＰＰＡＡＬ、もしくは、他のモデル検査プログラムを用いてもよい。また、ＳＰＩＮを用いたモデル検査では、動作仕様情報１００をPromelaと称する専用言語を用いて記述し、性質情報１０１をＬＴＬ（Linear Temporal Logic）と称する時相論理に基づく論理式で記述する。
【００４０】
モデル検査部３ａ〜３ｃは、動作仕様情報１００の全ての実行状態を網羅的に探索し、入力された性質情報群１０２の性質情報１０１を満たすかどうかを検査する。なお、この第１の実施形態における動作仕様情報１００は、上記非特許文献５では「振舞い仕様」と呼ばれている。本実施形態における性質情報は、非特許文献４で「性質」と呼ばれているものである。
【００４１】
図２は図１における入出力部２の一具体例を示すブロック構成図であって、５は入力部、６は性質情報記録部、７は検査指示部、８は検査結果取得部、９は検査結果出力部であり、図１に対応する部分には同一符号をつけて重複する説明を省略する。
【００４２】
同図において、入出力部２は、入力部５と性質情報記録部６と検査指示部７と検査結果取得部８と検査結果出力部９を有してなる。
【００４３】
入力部５は、動作仕様情報１００と性質情報群１０２が入力され、動作仕様情報１００ａとして検査指示部７に伝達し、性質情報群１０２の内容を性質情報記録部６に記録する。
【００４４】
検査指示部７は供給された動作仕様情報１００と性質情報記録部６から読み出される性質情報１０１とを参照して検査計画を算出し、この検査計画に従ってモデル検査部３ａ〜３ｃに検査を指示する。指示には、検査の開始または停止の指示と、検査の開始を指示する場合には、動作仕様情報１００と性質情報１０１とを含んでいる。
【００４５】
ここで、検査指示部７からは、動作仕様情報１００が全てのモデル検査部３ａ〜３ｃに供給され、また、モデル検査部３ａ〜３ｃ毎に異なる性質情報１０１が供給される。従って、モデル検査部３ａ〜３ｃでは夫々、互いに異なる性質情報１０１でこの動作仕様情報１００の検査（即ち、動作仕様情報１００が性質情報１０１を満たすか否かを検出する検査）が行なわれる。
【００４６】
検査結果取得部８は各モデル検査部３ａ〜３ｃからその検査結果を表わす検査結果情報を受け取り、この検査結果情報に従って性質情報記録部６の性格情報を更新し、また、検査結果情報を検査指示部７に伝達する。検査指示部７は、受け取った検査結果情報を基に、新たな検査手順を算出してモデル検査部３ａ〜３ｃに指示する。
【００４７】
検査結果出力部９は、性質情報記録部６の性質情報を参照して、検査情報１０３を出力する。この参照は、定められた時間間隔で定期的に行なうか、あるいは、検査結果取得部８による性質情報記録部６での性質情報の更新を認識した時点で行なってもよい。検査情報１０３の出力は、ユーザが認識できる形式であれば、電子ファイルや印刷，ディスプレイなどのユーザインタフェースへの表示など、形式は問わない。
【００４８】
図３は図２における性質情報記録部６で記録された性質情報１０１の性質情報テーブルを示す図であって、６Ｔは性質情報記録テーブル、６ａは性質ＩＤ、６ｂは性質情報内容、６ｃは検査結果である。
【００４９】
同図において、性質情報記録部６では、入力された性質情報１０１が、性質情報記録テーブル６Ｔで示すように、性質ＩＤ６ａ，性質情報内容６ｂ及び検査結果６ｃの要素でもって表わされて記録される。性質情報記録部６には、性質ＩＤ６ａとして、予め性質ＩＤが「Ｐ１」，「Ｐ２」，「Ｐ３」，……と設定されており、入力される順に性質情報１０１が「Ｐ１」，「Ｐ２」，「Ｐ３」，……の順で性質ＩＤが割り当てられる。この性質ＩＤ６ａは、性質情報１０１を識別する記号を含むものであるが、性質情報１０１の識別ができれば、任意の形式であってよい。ここで、性質情報群１０２の持つべき情報の例を示すものであり、他のデータ形式で実施されてもよい。
【００５０】
性質情報内容６ｂは、入力された性質情報１０１の内容（論理式）を表わすものであって、例えば、ＬＴＬ式で記載される。これは、モデル検査部３ａ〜３ｃにモデル検査プログラムとしてＳＰＩＮを用いる場合であるが、性質情報１０１の表現形式としてＬＴＬ式に限定する必要はない。例えば、モデル検査部３ａ〜３ｃにモデル検査プログラムとしてＳＭＶを用いる場合には、性質情報１０１の性質情報内容６ｂはＣＴＬ（Computation Tree Logic）式であってよい。
【００５１】
検査結果６ｃには、動作仕様情報１００が該当する性質情報１０１を満たすか否かというモデル検査の結果を表わすものであり、ここでは、「ｖａｌｉｄ」は満たすこと、「ｉｎｖａｌｉｄ」は満たさないことを示す。
【００５２】
モデル検査部３ａ〜３ｃ（図２）のいずれかで検査結果が得られると、これが検査結果取得部８（図２）で取得されて性質情報記録部６に供給されるが、この性質情報記録部６では、該当する性質情報１０１の検査結果６ｃが「ｖａｌｉｄ」または「ｉｎｖａｌｉｄ」に更新される。即ち、性質情報記録部６では、検査結果取得部８から検査結果情報１０８が供給されると、この性質情報記録部６に記録されている該当する性質情報１０１が更新される（具体的には、検査結果６ｃがこの検査結果情報１０８に応じて更新される）ことになる。
【００５３】
ここで、性質情報内容６ｂでの「[]」と「<>」は時相演算子であり、「->」，「&&」，「->」は命題論理演算子である。それらにより構成される論理式を時相論理式という。これらの意味論については、例えば、先の非特許文献４に示されている。以下、論理式ｐと論理式ｑが論理的に等価であることをｐ≡ｑと表わす。また、論理式集合Ｓから論理式ｐが帰結されることをＳ├ｑと表わす。例えば、[](s && t)≡[]s && []tであり、{[](p-> <>q), [](q-> <>r)}├[](s-> <>r)である。
【００５４】
図３では、性質情報記録部６での５個の性質情報１０１を夫々性質情報１０１ａ，１０１ｂ，１０１ｃ，１０１ｄ，１０１ｅで表わしており、一例として、性質情報１０１ａは性質ＩＤ６ａが「Ｐ１」であり、性質情報内容６ｂは「[](p-> <>q)」であって、既に検査結果情報１０８が得られていて、検査結果６ｃは「ｖａｌｉｄ」に更新されている。
【００５５】
なお、以下では、性質ＩＤ６ａが「Ｐ１」，「Ｐ２」，「Ｐ３」であることを夫々、性質ＩＤ「Ｐ１」，「Ｐ２」，「Ｐ３」ということにする。
【００５６】
この第１の実施形態においては、性質情報１０１は時相論理式で表わされ、性質情報群１０２はこれら性質情報１０１の集合である。
【００５７】
このようにして、入力部５（図１，図２）から入力された性質情報１０１が性質情報記録部６に供給されると、この性質情報１０１が性質情報内容６ｂとなり、これに性質ＩＤ６ａが割り当てられて記録される。そして、検査指示部７（図２）からの要求により、この性質情報１０１が性質情報記録部６から読み出されて検査指示部７（図２）に供給されるときには、かかる性質ＩＤ６ａが性質情報内容６ｂに付加されてなる性質情報１０１が性質情報記録部６から読み出されて検査指示部７に供給される。その後、この性質情報１０１に対して検査結果が検査結果取得部８（図２）で得られると、性質情報記録部６において、この性質情報１０１での検査結果６ｃがこの検査結果によって更新されることになる。
【００５８】
図４は図１におけるモデル検査部３ａ〜３ｃの一具体例を示すブロック構成図であって、３はモデル検査部（モデル検査部３ａ〜３ｃの総称）、１０は検査受付部、１１は検査部、１２は結果送信部、１０４は検査指示情報、１０５は検査結果情報であり、前出図面に対応する部分には同一符号をつけて重複する説明を省略する。
【００５９】
同図において、モデル検査部３ａ〜３ｃ、即ち、モデル検査部３は、検査受付部１０と検査部１１と結果送信部１２とから構成されている。ここで、検査部１１は、ＳＰＩＮ，ＳＭＶ，ＵＰＰＡＡＬあるいは他のモデル検査プログラムを利用してよい。
【００６０】
検査受付部１０は、入出力部２からの検査指示情報１０４と動作仕様情報１００と性質情報１０１を受け付け、入出力部２で作成された検査指示情報１０４に従って検査部１１の実行を制御する。検査部１１に検査を実行させる場合には、検査受付部１０は、動作仕様情報１００と性質情報１０１とを検査部１１に供給する。ここで、モデル検査部３に供給される動作仕様情報１００は仕様検査装置１に入力される動作仕様情報（以下では、これを入力動作仕様情報という）１００と同一の情報内容のものであるが、同一のデータ形式である必要はない。同様に、モデル検査部３に供給される性質情報１０１も、仕様検査装置１に入力される性質情報（以下では、これを入力性質情報という）１０１と同一の情報内容のものであるが、同一のデータ形式である必要はない。
【００６１】
検査部１１は、動作指示情報１０４による検査受付部１０の制御に伴い、モデル検査を実行し、または、停止し、実行時には、入力された動作仕様情報１００と性質情報１０１とに対するモデル検査を実行し、モデル検査実行後、その検査結果情報１０５を出力する。
【００６２】
結果送信部１２は、この検査結果情報１０５を取得して、入出力部２に伝達する。ここで、結果送信部１２からの検査結果情報１０５は検査部１１からの検査結果情報１０５と同一の情報内容のものであるが、同一のデータ形式である必要はない。
【００６３】
図５は図２における検査指示部７の一具体例を示すブロック構成図であって、１３は検査制御部、１３ａは記憶部、１０６は検査計画情報、１０７は検査部情報、１０８は検査結果情報であり、前出図面に対応する部分には同一符号をつけて重複する説明を省略する。なお、ここでは、モデル検査部３ｃは、図面の都合上、図示を省略している。
【００６４】
同図において、検査指示部７は記憶部１３ａなどを有する検査制御部１３から構成されている。この検査制御部１３は、入力部５（図２）から動作仕様情報１００を取得とし、性質情報記録部６から性質情報１０１（性質ＩＤ６ａ（図３）が付加されている）の性質情報群１０２を取得して夫々記憶部１３ａに保持する。そして、これら動作仕様情報１００と性質情報１０１とを参照して検査計画を算出し、検査計画情報１０６を作成する。
【００６５】
また、検査制御部１３は、検査計画情報１０６に基づいて検査指示情報１０４を作成する。この検査指示情報１０４はモデル検査部３毎に作成され、ここでは、モデル検査部３ａに対する検査指示情報１０４を検査指示情報１０４ａとし、モデル検査部３ｂに対する検査指示情報１０４を検査指示情報１０４ｂとする。検査指示情報１０４ａは、記憶部１３ａに保持されている動作仕様情報１００と性質情報１０１とともに、モデル検査部３ａに供給され、検査指示情報１０４ｂは、この動作仕様情報１００と記憶部１３ａに保持されている他の性質情報１０１とともに、モデル検査部３ｂに供給される。ここで、このときにモデル検査部３ａに供給される性質情報１０１を図３の性質情報１０１ａとすると、モデル検査部３ｂに供給される性質情報１０１を図３の性質情報１０１ｂとなる。かかる検査指示情報１０４ａ，１０４ｂの指示のもとに、モデル検査部３ａで検査仕様情報１００が性質情報１０１ａを満たすか否かの検査が行なわれ、モデル検査部３ｂで検査仕様情報１００が性質情報１０１ｂを満たすか否かの検査が行なわれる。
【００６６】
このように、モデル検査部３ａに動作仕様情報１００と性質情報１０１ａとが供給され、検査指示情報１０４ａによってこのモデル検査部３ａでの性質情報１０１ａによる動作仕様情報１００の検査開始の指示が与えられると、検査制御部１３は検査計画情報１０６を、この性質情報１０１ａに関して、更新する。同様にして、モデル検査部３ｂに動作仕様情報１００と性質情報１０１ｂとが供給され、検査指示情報１０４ｂによってこのモデル検査部３ｂでの性質情報１０１ｂによる動作仕様情報１００の検査開始の指示が与えられると、検査制御部１３は検査計画情報１０６を、この性質情報１０１ｂに関して、更新する。
【００６７】
これらモデル検査部３ａ，３ｂの検査結果は検査結果取得部８で取得され、これらが検査結果情報１０８として検査制御部１３に供給される。なお、かかる検査結果情報１０８には、該当する性質情報１０１と関連付けるために、この検査結果を出力したモデル検査部３の検査部ＩＤが付加されている。
【００６８】
ここで、モデル検査部３ａ，３ｂのいずれかで検査が終了し、検査結果情報１０８が検査結果取得部８から得られると、検査制御部１３は、記憶部１３ａから新たな性質情報１０１（例えば、図３での性質ＩＤ「Ｐ３」の性質情報１０１ｃ）を取得するとともに、取得した検査結果情報１０８と検査計画情報１０６とをもとに検査計画を再算出して検査計画情報１０６を更新し、更新された検査計画情報１０６に基づいて新たに検査指示情報１０４を作成し、モデル検査部３ａ，３ｂのうちの検査が終了した方のモデル検査部３に動作仕様情報１００と記憶部１３ａから取得した性質ＩＤ「Ｐ３」の性質情報１０１ｃとをこのモデル検査部３に供給し、この検査指示情報１０４によってモデル検査の開始を指示する。
【００６９】
なお、検査部情報１０７は、各モデル検査部３に関する情報である。
【００７０】
図６は図５における検査計画情報１０６の一具体例を示す図であって、１０７ａは検査部ＩＤ、１０７ｂは検査状態である。
【００７１】
各モデル検査部３には、その識別子として、検査部ＩＤが割り当てられている。ここで、仕様検査装置１に、図１に示すように、３つのモデル検査部３ａ，３ｂ，３ｃが設けられているものとすると、夫々の検査部ＩＤを「Ｃ１」，「Ｃ２」，「Ｃ３」とする（なお、以下では、これら検査部ＩＤを夫々検査部ＩＤ「Ｃ１」，「Ｃ２」，「Ｃ３」という）。なお、検査部ＩＤとしては、モデル検査部３を識別できる適宜の形式のものを用いることができる
図６において、検査計画情報１０６は、性質情報１０１毎に検査に用いるモデル検査部３と検査状況を表わしたものであって、性質情報１０１を性質ＩＤ６ａと、検査に割り振られたモデル検査部３を表わす検査部ＩＤ１０６ａと、性質情報１０１の検査状況を表わす検査状況１０６ｂとで表わされる。
【００７２】
性質ＩＤ６ａは、性質情報記録部６で設定された性質情報１０１に対して割り当てられた図３に示す性質ＩＤ６ａであり、先に説明したように、検査制御部１３が性質情報記録部６から性質情報群１０２を読み取ったときに、夫々の性質情報１０１に性質ＩＤ６ａが付加されており、記憶部１３ａに保持され、検査計画情報１０６が作成されるときには、性質情報１０１毎に、その性質ＩＤ６ａが登録される。
【００７３】
検査部ＩＤ１０６ａは、性質ＩＤ６ａが登録されている性質情報１０１のうちで、モデル検査部３で検査が行なわれている、あるいは検査が行なわれた性質情報１０１に対して、登録されるものであって、また、検査に使用されている、あるいは使用されたモデル検査部３に割り当てられた検査部ＩＤが登録されるものである。図６に示す例では、性質ＩＤ「Ｐ１」の性質情報１０１ａ（図３）に対しては、検査部ＩＤ１０６ａが「Ｃ１」（即ち、検査部ＩＤ「Ｃ１」）のモデル検査部３が、性質ＩＤ「Ｐ２」の性質情報１０１ｂ（図３）に対しては、検査部ＩＤ１０６ａが「Ｃ２」（即ち、検査部ＩＤ「Ｃ２」）のモデル検査部３が、性質ＩＤ「Ｐ３」の性質情報１０１ｃ（図３）に対しては、検査部ＩＤ１０６ａが「Ｃ３」（即ち、検査部ＩＤ「Ｃ３」）のモデル検査部３が夫々使用されたこと、あるいは仕様されていることが示されている。なお、検査部ＩＤ１０６ａでマーク「―」が示される性質情報１０１、ここでは、性質ＩＤ「Ｐ４」，「Ｐ５」の性質情報１０１ｄ，１０１ｅ（図３）は、検査の待機中である。
【００７４】
検査状況１０６ｂは、性質情報１０１の検査状況を「Ｄｏｎｅ」，「Ｒｕｎｎｉｎｇ」で示すものであって、「Ｄｏｎｅ」は検査が終了したことを、「Ｒｕｎｎｉｎｇ」は検査中であることを夫々示している。マーク「−」が付された性質情報１０１は、まだ、モデル検査部３に割り振られていない待機状態にあること示すものである。図６においては、性質ＩＤ「Ｐ１」，「Ｐ２」の性質情報１０１は夫々、検査部ＩＤ「Ｃ１」，「Ｃ２」のモデル検査部３で検査が終了したものであり、性質ＩＤ「Ｐ３」の性質情報１０１は、検査部ＩＤ「Ｃ３」のモデル検査部３で検査中であることを示している。これら以外の性質情報１０１は、検査の待機状態にある。
【００７５】
このように、検査計画情報１０６において、検査の待機状態にある性質情報１０１は、モデル検査部３での検査が可能な状況となると、この検査計画情報１０６に基づいてこの性質情報１０１が検査可能なモデル検査部３に供給され、これとともに検査指示情報１０４が出力されて動作仕様情報１００の検査が行なわれる。これにより、図６に示す検査計画情報１０６では、この性質情報１０１に対して、その検査状況１０６ｂが「Ｒｕｎｎｉｎｇ」に更新され、検査が終了してその検査結果情報１０８が検査結果取得部８から供給されると、その検査状況１０６ｂが「Ｒｕｎｎｉｎｇ」から「Ｄｏｎｅ」に更新される。
【００７６】
なお、検査実行中のモデル検査部３から、それが所定の動作をする毎に、動作の変化を表わす検査経過情報が出力され、この検査経過情報が検査結果取得部８から検査制御部１３に供給されるようにしてもよい。この場合には、検査制御部１３は、この検査経過情報を取得する毎に、検査計画情報１０６における該当するモデル検査部３の検査部ＩＤ１０６ａでの検査状況１０６を「Ｒｕｎｎｉｎｇ」に更新するようにすることもできる。
【００７７】
ここで、図６に示すように、性質ＩＤ「Ｐ１」，「Ｐ２」の性質情報１０１ａ，１０１ｂの検査状況１０６ｂが「Ｄｏｎｅ」に更新されたとすると、性質情報記録部６では、検査結果情報１０８に基づいて、図３に示すこれらの検索結果６ｃが「Ｖａｌｉｄ」もしくは「ｉｎｖａｌｉｄ」に更新されることになる。
【００７８】
なお、これら「Ｄｏｎｅ」，「Ｒｕｎｎｉｎｇ」，「−」は夫々、検査状況を表わす表現の一例であって、同様に検査状態を意味する他の形式で表わすようにしてもよい。
【００７９】
検査制御部１３とモデル検査部３との間の通信は、モデル検査部３の種別に応じた通信方式によって行なわれる。従って、検査制御部１３からモデル検査部３への動作仕様情報１００や性質情報１０１の提供も、提供先のモデル検査部３の通信方式に基づいて行なわれる。そこで、検査制御部１３から該当するモデル検査部３への検査指示情報１０４による検査の開始や終了の指示も、このモデル検査部３の通信方式に応じた指示方式で行なわれる。モデル検査部３に対するかかる指示方式は、検査部情報１０７に設定されている。
【００８０】
図７はかかる検査部情報１０７の一具体例を示す図であって、１０７ａは通信方式であり、図６に対応する部分には同一符号を付けている。
【００８１】
同図において、モデル検査部３夫々の検査部情報１０７は検査部ＩＤ１０６ａと通信方式１０７ａからなり、仕様検査装置１（図１）に用いられるモデル検査部３夫々に割り当てられた検査部ＩＤ１０６ａが登録され、モデル検査部３の指示方式などの通信方式に関する情報が通信方式１０７ａとして設定されている。ここで、登録された検査部ＩＤ１０６ａは、図６に示す検査計画情報１０６での検査部ＩＤ１０６ａと同じである。
【００８２】
通信方式１０７ａには、例えば、該当するモデル検査部３が入出力部２（図１）とネットワークで接続された計算機で実行するプログラムである場合には、この計算機との通信方式や計算機の識別子，検査指示情報１０４と動作仕様情報１００と性質情報１０１とのこのモデル検査部３への伝達方法，このモデル検査部３に検査の実施もしくは停止を指示する方法（指示方式）などが設定される。
【００８３】
検査制御部１３が動作仕様情報１００や性質情報１０１を所定のモデル検査部３に送出する場合には、これらのこのモデル検査部３への通信方式を検査部情報１０７として設定されている通信方式に決定し、また、検査指示情報１０４も、この通信方式１０７ａの指示方式を基に、このモデル検査部３に送る。
【００８４】
なお、検査部情報１０７では、図７に図示しないが、「動作状況」欄を設け、夫々のモデル検査部３の動作状況（動作中，待機中など）を登録するようにしてもよい。
【００８５】
図８は図５における検査制御部１３の処理の流れの一具体例を示すフローチャートである。
【００８６】
同図において、検査制御部１３は、動作を開始すると（ステップＳ１００）、まず、動作仕様情報１００を読み込み、記憶部１３ａに保持する（ステップＳ１０１）。次いで、性質情報記録部６（図３）から性質情報群１０２の全ての性質情報１０１を読み込み、記憶部１３ａに保持する（ステップＳ１０２）。そして、これら性質情報１０１を基に、検査計画情報１０６（図６）を作成する（ステップＳ１０３）。但し、この検査計画情報１０６では、この時点では、性質情報１０１の性質ＩＤ「Ｐ１」，「Ｐ２」，……，「Ｐ５」が性質ＩＤ６ａとして登録されるだけであり、検査部ＩＤ１０６ａ，検査状況１０６ｂには、全ての性質ＩＤ６ａに対し、マーク「−」が付される。
【００８７】
次に、この仕様検査装置１に設けられたモデル検査部３ａ〜３ｃに関する情報を取得し、上記の検査部情報１０７（図７）を作成する（ステップＳ１０４）。
【００８８】
次に、検査計画情報１０６を基に、検査部ＩＤ１０６ａが割り振られていない性質情報１０１（以下、割り振り済みでない性質情報１０１という）があるか否かを判断する（ステップＳ１０５）。これは、検査計画情報１０６において、検査部ＩＤ１０６ａ、または、検査状況１０６ｂでマーク「−」が付された性質情報１０１の性質ＩＤ６ａを探索するものであり、この時点では、全ての性質情報１０１の性質ＩＤ６ａがこれに該当するので、割り振られていない性質情報１０１があるとして（ステップＳ１０５の“Ｙｅｓ”）、性質ＩＤ「Ｐ１」を選択する。
【００８９】
そして、検査計画情報１０６（図６）を基に、検査に使用されていないモデル検査部３（以下では、検査中でないモデル検査部３という）があるか否かを判断し（即ち、検査状況１０６ｂが「Ｒｕｎｎｉｎｇ」である検査部ＩＤ１０６ａがあるか否かの判断：ステップＳ１０６）、検査中でないモデル検査部３がなければ（即ち、全ての検査部ＩＤ１０６ａの検査状況１０６ｂが「Ｒｕｎｎｉｎｇ」または「Ｄｏｎｅ」である：ステップＳ１０６の“Ｎｏ”）、ステップＳ１０８に進むが、検査中でないモデル検査部３があれば（即ち、検査部ＩＤ１０６ａで登録されていない検査部ＩＤ１０６ａのモデル検査部３があるか、全てのモデル検査部３の検査部ＩＤ１０６ａが検査部ＩＤ１０６ａに登録されていても、その検査状況１０６ｂが「Ｄｏｎｅ」であるとき：ステップＳ１０６の“Ｙｅｓ”）、この検査中でないモデル検査部３の検査部ＩＤ１０６ａを取得する。あるいは、検査部情報１０７（図７）に上記の「動作状況」欄が設けられている場合、この「動作状況」欄での登録内容から検査中でないモデル検査部３の有無を判断するようにしてもよいし、あるいはまた、各モデル検査部３に対して動作状況を問合せて判断するようにしてもよい。最初の時点では、どのモデル検査部３も検査中ではないので、任意のモデル検査部３を選択してよいが、ここでは、検査部ＩＤ１０６ａ（図７：図６での検査部ＩＤ１０６ａと同じ）が「Ｃ１」（以下では、これを検査部ＩＤ「Ｃ１」という。他の検査部ＩＤ１０６ａについても、同様）のモデル検査部３を選択するものとする。
【００９０】
次に、ステップＳ１０５で選択した性質ＩＤ「Ｐ１」とステップＳ１０６で選択した検査部ＩＤ「Ｃ１」とを関連付けて、この性質ＩＤ「Ｐ１」の性質情報１０１ａを検査部ＩＤ「Ｃ１」のモデル検査部３ａに割り当て、検査計画情報１０６の性質ＩＤ「Ｐ１」に対応する検査部ＩＤ１０６ａを「Ｃ１」に更新する。そして、検査部情報１０７（図７）での検査部ＩＤ「Ｃ１」に対応する通信方式１０７ａでの指示方式に従って、検査部ＩＤ「Ｃ１」のモデル検査部３ａに対して、検査指示情報１０４ａと性質ＩＤ「Ｐ１」の性質情報１０１ａと動作仕様情報１００とを伝達する。この伝達が完了すると、検査計画情報１０６（図６）の性質ＩＤ「Ｐ１」の性質情報１０１ａに対応する検査状況１０６ｂを「Ｒｕｎｎｉｎｇ」に更新する（段落〔００１０７〕）。
【００９１】
これにより、このモデル検査部３ａで動作仕様情報１００が性質情報１０１ａを満たすか否かの検査が行なわれ、その検査結果を、検査結果情報１０８として、検査結果取得部８（図５）を介して取得する。そして、これとともに、検査計画情報１０６で性質ＩＤ「Ｐ１」の検査状況１０６ｂを「Ｄｏｎｅ」に更新する（ステップＳ１０８）。
【００９２】
次いで、ステップ１０５に戻って、割り振り済みでない性質情報１０１があると、その性質情報１０１に対してステップＳ１０６からの処理を行なう。
【００９３】
このようにして、性質情報群１０２の性質情報１０１ａ，１０１ｂ，……が順に検査され、これとともに、性質情報記録部６（図２）では、図３に示すように、検査が完了した性質情報１０１（図３では、性質ＩＤ「Ｐ１」，「Ｐ２」の性質情報１０１ａ，１０１ｂ）に対し、検査結果６ｃが「ｖａｌｉｄ」あるいは「ｉｎｖａｌｉｄ」に更新される。
【００９４】
割り振り済みでない性質情報１０１がない場合には（ステップＳ１０５の“Ｎｏ”）、検査済みでない性質情報１０１があるか否かを判定する（ステップＳ１０９）。これは、性質情報群１０２の全ての性質情報１０１が検査終了したか否かを判定するものであって、ない場合には（ステップＳ１０９の“Ｎｏ”）、処理を終了するが（ステップＳ１１１）、ある場合には（ステップＳ１０９の“Ｙｅｓ”）、その性質情報１０１の検査結果を待って（ステップＳ１１０）、処理を終了する（ステップＳ１０９，Ｓ１１１）。
【００９５】
図９は検査制御部１３による図８におけるステップＳ１０８の一具体例を示すフローチャートである。
【００９６】
同図において、ステップＳ１０８の検査状況処理がスタートすると（ステップＳ１０８ａ）、まず、検査結果取得部８（図５）からの検査結果情報１０８の有無をチェックする（ステップＳ１０８ｂ）。検査結果情報１０８がなければ（ステップＳ１０８ｂの“Ｎｏ”）、この検査状況処理の処理を終了し（ステップＳ１０８ｆ）、図８でのステップＳ１０５に戻る。
【００９７】
検査結果情報１０８があれば（ステップＳ１０８ｂの“Ｙｅｓ”）、この検査結果情報１０８を取得する（ステップＳ１０８ｃ）。この検査結果情報１０８には、これを発生したモデル検査部３の検査部ＩＤ１０６ａが付加されていてこの検査結果情報１０８の発生元を明確にしており、この検査結果情報１０８を、この検査部ＩＤ１０６ａとともに、記憶部１３ａに保持する。この検査結果情報１０８には、動作仕様情報１００が性質情報１０１を満たすか否かというモデル検査部３の検査結果と、動作仕様情報１００が性質情報１０１を満たさない場合には、満たさない状況に至る動作系列（非特許文献５における「不具合シナリオ」に相当）を含んでいる。
【００９８】
次に、記憶部１３ａに記憶した検査結果情報１０８に従って図３に示す性質情報記録部６の該当する性質情報１０１を更新する（ステップＳ１０８ｄ）。即ち、検査結果情報１０８が、動作仕様情報１００が性質情報１０１を満たすことを示す検査結果を表わすものである場合には、性質情報記録部６での性質情報記録テーブル６Ｔ（図３）の該当するモデル検査部３の検査部ＩＤによる検査結果６ｃとして、「ｖａｌｉｄ」を登録する。また、検査結果情報１０８が、動作仕様情報１００が性質情報１０１を満さないことを示す検査結果を表わすものである場合には、性質情報記録部６での該当するモデル検査部３の検査部ＩＤによる検査結果６ｃとして、「ｉｎｖａｌｉｄ」を記録する。図３では、性質ＩＤ「Ｐ１」の性質情報１０１ａに対しては、その検査結果６ｃが「ｖａｌｉｄ」に更新され、性質ＩＤ「Ｐ２」の性質情報１０１ｂに対しては、その検査結果６ｃが「ｉｎｖａｌｉｄ」に更新されたものとしている。
【００９９】
続いて、検査結果情報１０８に従って図６に示す検査計画情報１０６を更新する（ステップＳ１０８ｅ）。即ち、この検査計画情報１０６の該当するモデル検査部３の検査部ＩＤに対応する検査状況１０６ｂを「Ｄｏｎｅ」に更新する。図６では、検査部ＩＤ「Ｃ１」，「Ｃ２」のモデル検査部３ａ，３ｂに対し、それらの検査状況１０６ｂが「Ｄｏｎｅ」に更新されたものとしている。
【０１００】
以上の処理が終了すると、図８でのステップＳ１０８の処理が終了し、ステップＳ１０５に戻る。
【０１０１】
なお、ステップＳ１０８ｃからステップＳ１０８ｅまでの処理では、検査部ＩＤをキーとして検査計画情報１０６と性質情報記録部６とを更新するようにしたが、モデル検査部３で検査に用いた性質情報１０１の性質ＩＤをキーとして、同様の更新を実行するようにしてもよい。この場合には、図５において、各モデル検査部３から出力される検査結果に、この検査に用いた性質情報１０１に付加されていた性質ＩＤを関連付け、検査結果取得部８から出力される検査結果情報１０８にかかる性質ＩＤを付加するようにすればよい。
【０１０２】
以上のようにして、この第１の実施形態では、入力された性質情報群１０２について、この性質情報群１０２に含まれる性質情報１０１を、複数のモデル検査部３のうちのいずれかに割り当てて、複数のモデル検査部３が並行して動作仕様情報１００の検査を実施することを繰り返すことで、全ての性質情報１０１に対して動作仕様の検査を達成できる。そして、このように、複数のモデル検査部３で並行して動作仕様情報１００の検査を実行することにより、単一のモデル検査プログラムで複数の性質情報１０１に対する検査を順次行なうのに比べ、短時間で動作仕様情報１００の検査を行なうことが可能となる。
【０１０３】
〔第２の実施形態〕
次に、本発明による仕様検査装置の第２の実施形態について説明する。
【０１０４】
先の第１の実施例では、入力された性質情報群１０２の各性質情報１０１に対しては夫々、１つのモデル検査部３が動作仕様情報１００の検査に使用されるものであったが、この第２の実施例では、１つ１つの性質情報１０１に対し、複数のモデル検査部３が動作仕様情報１００の検査に用いられるものである。この第２の実施形態では、図１〜図５，図７は先の第１の実施形態と同様である。
【０１０５】
ここで、第２の実施例では、図５での検査制御部１３で作成される検査計画情報１０６が、先の第１の実施形態での図６に示す検査計画情報１０６と異なる。なお、この第２の実施形態においても、３台のモデル検査部３ａ〜３ｃに対しては、図７に示す検査部情報１０７が作成されており、夫々のモデル検査部３ａ〜３ｃは、通信方式１０７ａが異なるものとする。そして、モデル検査部３の通信方式が異なると、そこで処理される情報のデータ形式が異なることになり、また、また、モデル検査部３の処理速度も異なることから、同じ情報を検査処理するにしても、モデル検査部３毎に処理時間が異なることになる。
【０１０６】
この第２の実施形態は、このことを利用して動作仕様情報１００が性質情報１０１を満たしているか否かの検査処理に要する時間を短縮するものである。
【０１０７】
図１０は本発明による仕様検査装置の第２の実施形態での図５における検査計画情報１０６の一具体例を示す図であって、図６に対応する部分には同一符号を付けている。
【０１０８】
同図において、この第２の実施形態では、上記のように、モデル検査部３ａ〜３ｃの通信方式１０７ａが異なる場合、同じ性質情報１０１に対し、２以上のモデル検査部３を同時に検査に用いることができるものであり、図示する例では、性質ＩＤ「Ｐ１」，「Ｐ２」の性質情報１０１ａ，１０１ｂでは、検査部ＩＤ「Ｃ１」，「Ｃ２」の２台のモデル検査部３ａ，３ｂを使用するものとして、検査部ＩＤ１０６ａとして検査部ＩＤ「Ｃ１」，「Ｃ２」を設定している。また、性質ＩＤ「Ｐ３」の性質情報１０１ｃでは、検査部ＩＤ「Ｃ３」のモデル検査部３ｃのみを使用するものであり、その検査部ＩＤ１０６ａとして検査部ＩＤ「Ｃ３」を設定している。
【０１０９】
ここでは、性質ＩＤ「Ｐ１」の性質情報１０１ａでは、検査状況１０６ｂが「Ｄｏｎｅ」となって検査は終了している。また、性質ＩＤ「Ｐ２」，「Ｐ３」の性質情報１０１ｂ，１０１ｃは、検査状況１０６ｂが「Ｒｕｎｎｉｇ」となって検査中である。これら以外の性質ＩＤ「Ｐ４」，「Ｐ５」の性質情報１０１ｄ，１０１ｅは、検査状況１０６ｂが「―」となって待機状態にある。
【０１１０】
図１１は第２の実施形態における図５における検査制御部１３の処理の流れの一具体例を示すフローチャートであって、図８におけるステップと同一ステップには同一符号をつけて重複する説明は省略する。
【０１１１】
同図において、ステップＳ１００からステップＳ１０４までの処理は、図８におけるステップＳ１００からステップＳ１０４までの処理と同じであり、図８でのステップＳ１０５，Ｓ１０７，Ｓ１０８の代わりに、ステップＳ２００，Ｓ２０１，Ｓ２０２の処理が行なわれる。
【０１１２】
検査計画情報１０６（図５）が作成され（ステップＳ１０３）、検査部情報１０７（図５）が作成されると（ステップＳ１０４）、次に、検査済みでない性質情報１０１があるか否かを判断し（ステップＳ２００）、ある場合には（ステップＳ２００の“Ｙｅｓ”）、該当する性質情報１０１の性質ＩＤ６ａを選択し、ステップＳ１０６に移る。
【０１１３】
ここで、検査済みでない性質情報１０１とは、検査計画情報１０６で検査部ＩＤ１０６ａが対応づけられていない性質ＩＤ６ａの性質情報１０１、即ち、モデル検査部３に割り振られていない性質情報１０１であるか、あるいは、検査状況１０６ｂが「Ｒｕｎｎｉｎｇ」となっている性質ＩＤ６ａの性質情報１０１、即ち、モデル検査部３で検査中の性質情報１０１である。
【０１１４】
ステップＳ２００が“Ｙｅｓ”であるときには、かかる検査済みでない性質情報１０１のうちの任意の性質情報１０１を選択する。なお、モデル検査部３に割り振られていない性質情報１０１か、モデル検査部３で検査中の性質情報１０１かいずれかを優先的に選択してもよい。
【０１１５】
このようなモデル検査部３に割り振られていない性質情報１０１がなく、モデル検査部３で検査中の性質情報１０１のみがある場合には、検査済みでない性質情報１０１はないとして（ステップＳ２００の“Ｎｏ”）、ステップＳ１０９に進み、図８と同様、ステップＳ１１０，Ｓ１１１の処理が行なわれる。
【０１１６】
検査済みでない性質情報１０１がある場合には（ステップＳ２００の“Ｙｅｓ”）、第１の実施形態と同様、検査中でないモデル検査部３があるかどうかを検出し、ない場合には（ステップＳ１０６の“Ｎｏ”）、後述するステップＳ２０２に進むが、ある場合には（ステップＳ１０６の“Ｙｅｓ”）、ステップＳ２０１に進む。
【０１１７】
ステップＳ２０１では、ステップＳ２００で検査計画情報１０６（図１０）から選択した性質ＩＤ６ａとステップＳ１０６で選択した検査部ＩＤ１０６ａを対応付けることにより、この性質ＩＤ６ａの性質情報１０１に１以上のモデル検査部３が割り当てられる。これにより、検査計画情報１０６において、この選択した性質ＩＤ６ａに対して対応付けられた１つ以上の検査ＩＤ１０７ｂがこの検査ＩＤ６ａに対する検査部ＩＤ１０６ａに設定されて更新される。そして、検査部情報１０７（図７）の検査部ＩＤ１０６ａに対応する通信方式１０６での指示方式を基に、該当するモデル検査部３に対して、検査指示情報１０４とこの性質ＩＤ６ａに該当する性質情報１０１と動作仕様情報１００を伝達する。検査計画情報１０６でこの性質ＩＤ６ａに対応する検査状況１０６ｂが「−」のときには、「Ｒｕｎｎｉｎｇ」に更新する。しかる後、かかるモデル検査部３で検査が行なわれ、ステップＳ２０２に進む。
【０１１８】
図１０に示す検査計画情報１０６によると、性質ＩＤ「Ｐ１」の性質情報１０１ａは、検査部ＩＤ「Ｃ１」，「Ｃ２」のモデル検査部３ａ，３ｂで検査が行なわれて、その検査が終了したものである。性質ＩＤ「Ｐ２」の性質情報１０１ｂは、検査部ＩＤ「Ｃ１」，「Ｃ２」のモデル検査部３ａ，３ｂで検査が行なわれているところであり、性質ＩＤ「Ｐ３」の性質情報１０１ｃは、検査部ＩＤ「Ｃ３」のモデル検査部３ｃで検査が行なわれているところである。これら以外の性質ＩＤ「Ｐ４」，「Ｐ５」の性質情報１０１ｄ，１０１ｅは待機状態にある。
【０１１９】
図１２は図１１におけるステップ２０２の一具体例を示すフローチャートであり、図９と同様の処理には同一符号を付けて重複する説明を省略する。
【０１２０】
同図において、ステップＳ１０８ａからステップＳ１０８ｃまでの処理は、第１の実施形態での図９の処理と同様である。
【０１２１】
ここで、いま、同じ性質ＩＤ６ａの性質情報１０１が複数のモデル検査部３に割り当てられ、これらモデル検査部３でこの性質情報１０１の検査が同時に指示され、検査が行なわれているとする。
【０１２２】
その後、これらモデル検査部３のうちの１つで検査が終了し、その検査結果情報１０８が検査結果取得部８（図５）からあると（ステップＳ１０８ｂの“Ｙｅｓ”）、検査結果取得部８は、先の第１の実施形態と同様、この検査結果情報１０８を取得し（ステップＳ１０８ｃ）、性質情報記録部６でこの性質情報１０１について更新する（ステップＳ１０８ｄ）。
【０１２３】
しかる後、検査制御部１３は、この性質情報１０１を用いて検査を行なっている他のモデル検査部３に停止指令の検査指示情報１０４を送り、これらモデル検査部３の検査処理を途中で停止させる（ステップＳ２０２ａ）。例えば、図１０に示すように、性質ＩＤ「Ｐ２」の性質情報１０１ｂを用いて検査部ＩＤ「Ｃ１」，「Ｃ２」のモデル検査部３ａ，３ｂが動作仕様情報１００の検査を行なっているときに、例えば、検査部ＩＤ「Ｃ１」のモデル検査部３ａが終了してその検査結果情報１０８が得られると、検査制御部１３は、この検査結果情報１０８を取得するとともに、検査動作中の検査部ＩＤ「Ｃ２」のモデル検査部３ｂをその検査の途中で停止させるものである。
【０１２４】
以上の動作が終わると、ステップＳ２０２の処理が終了し（ステップＳ１０８ｆ）、図１１のステップＳ２００に進む。
【０１２５】
以上のように、この第２の実施形態では、１つの性質情報１０１について複数のモデル検査部３で並行して同時に検査を実施し、これら複数のモデル検査部３のうちの１つが、同じ性質情報について検査を実施している他のモデル検査部３よりも早く検査が完了した場合には、これら検査実施中のモデル検査部３の検査を全て途中停止させる。
【０１２６】
ここで、同じ性質情報１０１についての検査を同時に複数のモデル検査部３で実行する例を示す。
【０１２７】
モデル検査プログラムでは、モデル検査の方法をユーザが指定できる。例えば、モデル検査ツールがＳＰＩＮである場合、ＳＰＩＮを実行するコマンドラインオプションにより、探索方法を変更することができる。上記の非特許文献１によれば、モデル検査プログラムの実体であるＰＡＮプログラムのコンパイル時オプションと実行時オプションなどに、探索方法や利用するメモリ最大量などを指定することができる。これらのオプション指定により、モデル検査に要する時間が異なる。しかし、どのオプションを指定すれば、最も短時間で検査が完了するかは、モデル検査プログラムを実行する計算機の性能や動作仕様情報の内容に依存し、一意に決定しない。
【０１２８】
以上のように、この第２の実施形態によれば、各モデル検査部３でモデル検査プログラムに対するオプションを変更することにより、１つの性質情報１０１に対して異なるモデル検査方法を用いることにより、同時にモデル検査を実行することができ、最も短時間で検査を完了したモデル検査の結果を採用することができ、モデル検査にかかる時間を短縮できる。
【０１２９】
〔第３の実施形態〕
次に、本発明による仕様検査装置の第３の実施形態について説明する。  
上記第２の実施形態では、オプション設定の異なる複数のモデル検査部３で同一の性質情報１０１を用いた動作仕様情報１００の検査を行ない、これらモデル検査部３のうちで最も短時間で検査が完了したモデル検査部３の検査結果を採用し、他のモデル検査部３による検査を途中停止した。
【０１３０】
しかし、オプション設定によっては、検査結果が確実でないものがある。例えば、ＳＰＩＮで用いられているPartial Order Reduction法と呼ばれる高速化技法があるが、上記非特許文献４によれば、このPartial Order Reduction法を用いた場合、動作仕様情報１００が性質情報１０１を満たさないという結果となった場合には、その結果は確実であるが、そうでない場合の結果は保証されない。
【０１３１】
この第３の実施形態では、仕様検査装置１が、各モデル検査部３で実行されるモデル検査プログラムのオプション設定を管理するものである。例えば、検査部情報１０７（図５，図７）を、図１３に示すように、オプション１０７ｂを追加して拡張し、そこにオプションを設定できるようにする。
【０１３２】
ここで、いま、検査計画情報１０６が図１０の状況であったとすると、性質ＩＤ「Ｐ２」の性質情報１０１ｂが検査部ＩＤ「Ｃ１」，「Ｃ２」の２つのモデル検査部３ａ，３ｂで検査中であるが、ここで、検査部ＩＤ「Ｃ１」のモデル検査部３ａで検査が先に完了し、動作仕様情報１００が性質情報１０１ｂを満たすという結果であった場合、この検査ＩＤ「Ｃ１」のモデル検査部３ｂがPartial Order Reduction法が用いられているものとすると、「満たさない」という検査結果は保証されるが、この「満たす」という検査結果が保証されない。
【０１３３】
そこで、同時に使用するモデル検査部３のいずれかにおいて、例えば、図１３において、検査部ＩＤ「Ｃ２」のモデル検査部３ｂに、オプション１０７ｂとして、Partial Order Reduction法を否定するオプション「-DNOREDUCE」を設定し、Partial Order Reduction法を用いてモデル検査部３（例えば、図１３での検査部ＩＤ「Ｃ１」のモデル検査部３ａ）とオプション「-DNOREDUCE」が設定された（即ち、検査に要する時間は長くなるが、「満たさない」という検査結果も、また、「満たす」という検査結果も保証される）モデル検査部３ｂとにより、性質情報１０１を用いた検査を同時に行なう。そして、Partial Order Reduction法を用いてモデル検査部３ａの方が先に検査を終了し、その検査結果が上記の「満たさない」というものであるときには、その検査結果は保証されるので、他方のモデル検査部３ｂの検査を途中で停止し、このモデル検査部３ａの検査結果が先の実施形態のように用いられるが、先に検査が終了したモデル検査部３ａの検査結果が上記の「満たす」というものであれば、これは保証されないので、さらにモデル検査部３ｂの検査を継続し、このモデル検査部３ｂの検査結果を最終的な結果とするものである。
【０１３４】
〔第４の実施形態〕
次に、本発明による仕様検査装置の第５の実施形態について説明する。
【０１３５】
上記第１〜第３の実施形態では、入力された性質情報１０１を用いた検査を複数のモデル検査部３で実行するようにしたが、この第４の実施形態では、入力された性質情報群１０２に、かかる性質情報群１０２から得られる新たな性質情報群１０２’を作成して加え、これら性質情報群１０２，１０２’を用いて動作仕様情報１００の検査を行なうものである。
【０１３６】
この第４の実施形態は、図１，図２，図４に示す構成をなすものであるが、検査指示部７が、性質情報群１０２’を形成する点で、先の実施形態１〜３のものとことなる。
【０１３７】
図１４はこの第４の実施形態における検査指示部７の一具体例を示すブロック構成図であって、１４は性質変換部、１０９は検査制御情報であり、図５に対応する部分には同一符号を付けて重複する説明を省略する。
【０１３８】
同図において、性質変換部１４は、性質情報１０１を演算処理して変換し、新たな性質情報（以下、これを変換性質情報１０１’という）を生成するものであり、性質情報記録部６に記録された性質情報群１０２の適宜の性質情報１０１を読み取って変換性質情報１０１’を生成し、これを性質情報記録部６に記録して性質情報群１０２に追加する。
【０１３９】
検査制御部１３は、性質情報記録部６からかかる変換性質情報１０１’を含めた性質情報群１０２を読み取って記憶部１３ａに保存し、かかる性質情報群１０２を基に、先の実施形態と同様、検査計画情報１０６を作成し、変換性質情報１０１’についても、モデル検査部３で動作仕様情報１００の検査が行なわれる。
【０１４０】
また、検査制御情報１０９は、モデル検査部３での検査の実行もしくは途中停止に関する情報である。
【０１４１】
図１５は図１４における性質変換部１４の一具体例を示すブロック構成図であって、１５は性質変換処理部、１６は性質変換ルール部である。
【０１４２】
同図において、性質変換部１４は性質変換変換部１５と各種の変換ルールが登録されている性質変換ルール部１６とから構成されており、性質情報記録部６から読み取った性質情報群１０２の性質情報１０１を、性質変換処理部１５により、性質変換ルール部１６での変換ルールに従って演算処理して新たな性質情報１０１’に変換し、これを性質情報記録部６に記録して更新する。
【０１４３】
図１６は図１５における性質変換ルール部１６の性質変換ルールテーブルの一具体例を示す図であって、１６Ｔは性質変換ルールテーブル、１６ａ〜１６ｈは性質変換ルール、１７ａは変換前集合、１７ｂは変換後集合、１７ｃは変換種別である。
【０１４４】
同図において、性質変換ルール１６ａ〜１６ｈは、変換前集合１７ａと変換後集合１７ｂとの関係を示すものであり、変換種別１７ｃはその関係を示す識別子である。変換前集合１７ａは性質情報１０１の集合を表わすものであり、集合の要素は１以上であるとする。変換後集合１７ｂは、対応する変換前集合１７ａから得る性質情報１０１の集合である。
【０１４５】
ここで、この性質変換ルールテーブル１６Ｔは一例を示すものであり、同様の意味を表わすならば、同一のデータ形式である必要はない。
【０１４６】
例えば、変換種別１７ｃが「等価」とは、変換前集合１７ａの要素である論理式Ｐと変換後集合の要素である論理式Ｑが、Ｐ≡Ｑの関係であることを意図する。変換種別１７ｃが「帰結」とは、変換前集合Ｓについて変換後集合の要素である論理式Ｑが、Ｓ├Ｑの関係であることを意図する。変換種別１７ｃが「Ａ分割」とは、「＆＆」演算子で結合された論理式「Ａ＆＆Ｂ」を「Ａ」と「Ｂ」とに分割し、その各々を選択することを意図するものである。また、変換種別１７ｃが「Ｏ分割」とは、「｜｜」演算子で結合された論理式「Ａ｜｜Ｂ」を「Ａ」と「Ｂ」に分割し、その各々を選択することを意図するものである。これらは性質変換ルールテーブル１６Ｔを定義したユーザの意図であり、仕様検査装置は単なる識別子として処理する。
【０１４７】
図１７は図１４及び図１５における性質変換部１４で得られた変換性質情報１０１’が追加されて拡張された性質情報記録部６の性質情報記録テーブル６Ｔの一具体例を示す図であって、６ｄが変換元、６ｅが変換種別であり、図３に対応する部分には同一符号を付けて重複する説明を省略する。
【０１４８】
同図において、性質情報１０１ａ〜１０１ｅは、入力された性質情報群１０２の性質情報１０１であり、図３における性質情報１０１ａ〜１０１ｅである。
【０１４９】
性質情報１０１’ａ〜１０１’ｃが性質変換部１４で得られて追加された変換性質情報１０１’である。ここで、これら変換性質情報１０１’ａ〜１０１’ｃでの変換元６ｄは、これら変換性質情報１０１’ａ〜１０１’ｃを得るために用いられた性質情報１０１の性質ＩＤ６ａを表わすものであり、図１６での変換前集合１７ａに相当する。変換種別６ｅは図１６での変換種別１７ｃに相当し、性質情報内容６ｂが図１６での変換後集合１７ｂに相当する。
【０１５０】
変換性質情報１０１’ａは、変換元６ｄを性質ＩＤ「Ｐ１」，「Ｐ２」の性質情報１０１ａ，１０１ｂとして、変換種別６ｅを「帰結」で変換したものであり（図１６でのルール１６ｆ）、変換情報６ｂが性質情報１０１ａの「［]ｐ‐＞ｑ」と性質情報１０１ｂの「［］ｑ−＞＜＞ｒ」とからなるものである。変換性質情報１０１’ｂ，１０１’ｃは、変換元６ｄを性質ＩＤ「Ｐ３」の性質情報１０１ｃとして、夫々変換種別６ｅを「Ｏ分割」で変換したものであり（図１６でのルール１６ｇ）、変換情報６ｂが性質情報１０１ｃの「［](ｓ＆＆ｔ）」を「ｓ」と「ｔ」とに分割して、夫々「［]ｓ」，「［]ｔ」とするものである。
【０１５１】
図１８は図１５に示す性質変換部１４の処理の流れの一具体例を示すフローチャートである。
【０１５２】
同図において、性質変換処理部１５は、まず、性質情報記録部６から性質情報群１０２を取得し（ステップＳ３００）、性質変換ルール部１６から性質変換ルールテーブル１６Ｔの性質変換ルールを取得する（ステップＳ３０１）。そして、取得した性質情報群１０２のサブセットのうち、取得したせいしつ変換ルールでの変換前集合１７ａのいずれかに該当する集合を検索し（ステップＳ３０２）、該当する集合が存在しない場合には（ステップＳ３０２の“Ｎｏ”）、性質変換処理を終了するが（ステップＳ３０４）。該当する集合が存在する場合には（ステップＳ３０２の“Ｙｅｓ”）、該当する変換前集合を演算して変換後集合１７ｂを算出し、図１７に示すように、これを性質情報記録部６の性質情報記録テーブル６Ｔに記録して性質情報群１０２に追加する（ステップＳ３０３）。
【０１５３】
ここで、例えば、図３に示す性質情報記録部６の性質情報記録テーブル６Ｔの性質情報群１０２と、性質変換ルール部１６の図１６に示す性質変換ルールテーブル１６Ｔを例にとると、性質情報記録テーブル１６Ｔでの性質情報１０１からなる集合のうち集合｛[](p-> <>q)，[](q-> <>r)｝は、図１６に示す性質変換ルールテーブル１６Ｔでの性質変換ルール１６ｆに該当する。ここで、この性質変換ルール１６ｆでのＡがｐ、Ｂがｑ、Ｃがｒに相当するため、変換後集合は｛[](p-> <>r)｝となる。
【０１５４】
さらに、ステップＳ３０３では、性質情報記録テーブル１６Ｔの変換元６ｄを変換に用いた元の性質情報１０１の性質ＩＤ６ａに更新し、得られた変換後集合１７ｂで図１７での性質情報記録テーブル１６Ｔの性質情報内容６ｂを更新し、使用した性質変換ルールの変換種別１７ｃで変換種別６ｅを更新する。上記の例は、図１７に示す性質情報記録テーブル１６Ｔの変換性質情報１０１’ａに対するものであり、変換元６ａは性質ＩＤ「Ｐ１」，「Ｐ２」であり、変換種別６ｅは「帰結」ということになる。
【０１５５】
図１９は図１４における検査制御情報１０９の一具体例を示す図であって、１０８ａ，１０８ｂは検査結果情報１０８の内容、１０９ａ，１０９ｂは他のモデル検査部３の動作制御（他検査部）、１１０ａ，１１０ｂは変換元６ｄの検査結果の判定（変換元）であり、前出図面に対応する部分には同一符号を付けている。
【０１５６】
同図において、検査制御情報１０９は、変換種別６ｅ毎に、検査結果情報１０８ａ，１０８ｂの検査結果内容に応じて、他のモデル検査部３の動作の制御１０９ａ，１０９ｂと変換元６ｄの検査結果の判定１１０ａ，１１０ｂとを規定するものである。
【０１５７】
ここで、変換種別６ｅが「等価」である場合を一例として説明すると、モデル検査部３から得られた検査結果情報１０８のそのとき使用した性質情報１０１に対し、「性質情報を満たす場合」との検査結果内容１０８ａであるときには、「変換元」１１０ａにより、そのモデル検査部３に対して、動作仕様情報１００がそのときの性質情報１０１を満たすものとし、「他検査部」１０９ａにより、他のモデル検査部３は検査を途中停止させる。また、「性質情報を満たさない場合」との検査結果内容１０８ｂであるときには、「変換元」１１０ｂにより、そのモデル検査部３に対して、動作仕様情報１００がそのときの性質情報１０１を満たすものとし、「他検査部」１０９ｂにより、他のモデル検査部３は検査を途中停止させる。
【０１５８】
変換種別６ｅが「帰結」である場合を他の例として説明すると、モデル検査部３から得られた検査結果情報１０８のそのとき使用した性質情報１０１に対し、「性質情報を満たす場合」との検査結果内容１０８ａであるときには、「変換元」１１０ａにより、そのモデル検査部３に対して、動作仕様情報１００がそのときの性質情報１０１を満たす可能性があるとし、「他検査部」１０９ａにより、他のモデル検査部３は検査を継続させる。また、「性質情報を満たさない場合」との検査結果内容１０８ｂであるときには、「変換元」１１０ｂにより、そのモデル検査部３に対して、動作仕様情報１００がそのときの性質情報１０１を一部満たさないものとし、「他検査部」１０９ｂにより、他のモデル検査部３は検査を継続させる。
【０１５９】
図２０は図１４，図１９に示す検査制御情報１０９を用いた図１４における検査制御部１３の処理の流れを示すフローチャートであり、前出図面に対応する部分には同一符号を付けて重複する説明を省略する。
【０１６０】
この第４の実施形態も、その全体的な動作は図８に示すフローチャートと同様であるが、検査制御部１３で行なわれるそのステップＳ１０８の処理が、図９に示すフローチャートに対し、図２０に示すように、ステップＳ１０８ｄとステップＳ１０８ｅとの間に、ステップＳ４００，Ｓ４０１の処理が付加されたものとなる。
【０１６１】
図２０において、図１４での検査制御部１３は、検査結果情報１０８を取得して（ステップＳ１０８ｃ）、性質情報記録部６の性質情報記録テーブル６Ｔ（図１７）の更新を行なうと（ステップＳ１０８ｄ）、検査制御情報１０９（図１９）を読み込んだ記憶部１３ａに保持する（ステップＳ４００）。
【０１６２】
次いで、記憶部１３ａに保持されている性質情報記録テーブル６Ｔ（図１７）からこのときの性質情報１０１または１０１’に対する変換種別６ｅを取得し、この変換種別６ｅに該当する他のモデル検査部３の検査を継続させるか、途中停止させるかの判定を検査制御情報１０９（図１９）の「他検査部」１０９ａ，１０９ｂのいずれかから取得する。この判定が他のモデル検査部３を途中停止するとのことである場合には、検査制御部１３は、このときの性質情報１０１または１０１’の変換元６ｄである性質情報１０１及び変換元６ｄから変換された他の性質情報１０１に該当するモデル検査部３に検査の途中停止を指示する（ステップＳ４０１）。そして、さらに、性質情報記録テーブル６Ｔ（図１７）での検査結果６ｃに、このときの性質情報１０１または１０１’，その変換元６ｄである性質情報１０１及び変換元６ｄから変換された他の性質情報１０１’の検査結果６ｃを更新する（ステップＳ４０１）。
【０１６３】
しかる後、検査計画情報１０６を更新し、このときの性質情報１０１または１０１’に対する検査を終了する（ステップＳ１０８ｆ）。
【０１６４】
以上により、入力された性質情報１０１に、それを変換して得られる新たな性質情報１０１’を加えた性質情報群１０２について並行動作するモデル検査部３により検査を実行し、一部の性質情報１０１または１０１’に対する検査の結果に従って、他の性質情報に対する検査の実行または停止を制御できる。
【０１６５】
これにより、入力された性質情報群１０２に新たに加えられた性質情報１０１’が、元々の性質情報群１０２に含まれていた性質情報１０１よりも早く検査が完了した場合に、仕様検査に要する時間を短縮することができる。
【０１６６】
なお、この第４の実施形態では、変換性質情報を前記性質変換部１４で再帰的に変換処理し、変換元６ｄの性質情報１０１を復帰させることもできる。
【０１６７】
〔第５の実施形態〕
上記第１〜第４の実施形態では、図８におけるステップＳ１０７もしくは図１１におけるステップＳ２０１において、性質情報１０１に対するモデル検査部３の割り当ては任意であった。
【０１６８】
この第５の実施形態では、さらに、モデル検査部３を構成する計算機の処理能力、即ち、ＣＰＵの能力や搭載メモリ量などが異なる場合には、モデル検査に時間がかかると想定される複雑構造をした性質情報１０１を優先的に処理能力の高い計算機で構成されたモデル検査部３に割り当てるものであり、これにより、モデル検査に要する時間を短縮するものである。
【符号の説明】
【０１６９】
１  仕様検査装置
２  入出力部
３，３ａ，３ｂ，３ｃ  モデル検査部
４  情報伝達路
５  入力部
６  性質情報記録部
６Ｔ  性質情報記録テーブル
６ａ  性質ＩＤ
６ｂ  性質情報内容
６ｃ  検査結果
６ｄが変換元
６ｅが変換種別
７  検査指示部
８  検査結果取得部
９  検査結果出力部
１０  検査受付部
１１  検査部
１２  結果送信部
１３  検査制御部
１４  性質変換部
１５  性質変換処理部
１６  性質変換ルール部
１６Ｔ  性質変換ルールテーブル
１６ａ〜１６ｈ  性質変換ルール
１７ａ  変換前集合
１７ｂ  変換後集合
１７ｃ  変換種別
１００  動作仕様情報
１０１  性質情報
１０１ａ〜１０１ｅ，１０１’ａ〜１０１’ｃ  性質情報
１０２  性質情報群
１０３  検査情報
１０４  検査指示情報
１０５  検査結果情報
１０６  検査計画情報
１０６ａ  検査部ＩＤ欄
１０６ｂ  検査状況
１０７  検査部情報
１０７ａ  通信方式
１０７ｂ  オプション
１０８  検査結果情報
１０８ａ，１０８ｂ  検査結果情報１０８の内容
１０９  検査制御情報
１０９ａ，１０９ｂ  他のモデル検査部３の動作制御（他検査部）
１１０ａ，１１０ｂ  変換元６ｄの検査結果の判定（変換元）
【図１】
2010277533.tif 000003
【図２】
2010277533.tif 000004
【図３】
2010277533.tif 000005
【図４】
2010277533.tif 000006
【図５】
2010277533.tif 000007
【図６】
2010277533.tif 000008
【図７】
2010277533.tif 000009
【図８】
2010277533.tif 000010
【図９】
2010277533.tif 000011
【図１０】
2010277533.tif 000012
【図１１】
2010277533.tif 000013
【図１２】
2010277533.tif 000014
【図１３】
2010277533.tif 000015
【図１４】
2010277533.tif 000016
【図１５】
2010277533.tif 000017
【図１６】
2010277533.tif 000018
【図１７】
2010277533.tif 000019
【図１８】
2010277533.tif 000020
【図１９】
2010277533.tif 000021
【図２０】
2010277533.tif 000022