JP2013206310A - モデル検査装置、モデル検査方法、およびプログラム - Google Patents

Abstract

【課題】システムやソフトウェアの設計を検証するモデル検査において、反例解析の効率を向上させる。
【解決手段】ソフトウェアまたはシステムを構成するモジュールの動作仕様と、入力条件・出力条件を定義した仕様・設計情報の入力を受ける仕様・設計情報入力部１１と、仕様・設計情報に基づいて、モジュール毎に不具合の有無を検証する検証コードを生成する検証コード生成部１２と、検証コードを用いてモデル検査を実行するモデル検査実行部１３と、モデル検査において不具合を発見した場合に得られる反例から、不具合の存在するモジュールが実行するものではないステップを排除する反例加工部１４と、モデル検査において発見された不具合の有無を出力し、不具合がある場合には、不具合のあるモジュールを提示すると共に、不具合のあるモジュールが実行するものではないステップを排除した反例を出力する検証結果出力部１５と、を備える。
【選択図】図１

Description

本発明は、モデル検査装置、モデル検査方法、およびプログラムに関する。

近年、複雑化・巨大化が進むシステムやソフトウェアの検証手法として、モデル検査による検証が行われている。モデル検査とは、検証対象を状態遷移系としてモデル化し、それを網羅的に探索することで、検証対象が仕様を満たしているかどうかを検証する技術である。モデル検査は設計段階から適用できるため、システムやソフトウェアの信頼性を向上させるための技術として注目されている。

モデル検査による検証手法でシステムやソフトウェアの不具合が発見された場合、その不具合に至るまでのシーケンスが、満たすべき仕様に対する反例として得られる。得られるのはあくまでシーケンスの一例であるため、不具合を修正するにあたりその原因を特定するには、得られた反例を解析する必要がある。その解析作業は一般に困難なものであるため、それを支援する技術が開発されている。例えば特許文献１には、反例と共に問題箇所候補を提示する技術が開示されている。

特許第４４７７０５４号公報

しかし、特許文献１に記載された方法では、反例そのものの可読性は向上しないという問題がある。反例のシーケンス内には、通常不具合と直接関係のあるステップだけでなく、無関係なステップも数多く含まれている。したがって、不具合の原因となっている箇所が判明しても、不具合が発生する理由や修正案の検討には反例の解析が不可欠である。その際に、不具合とは無関係のステップについても確認することは時間の浪費であり、検証の工数を増大させる原因となる。

そこで、本発明の目的は、システムやソフトウェアの設計が仕様を満たしているか否かを検証するモデル検査において、反例解析の効率を向上させることである。

本発明に係るモデル検査装置は、ソフトウェアまたはシステムを構成するモジュールの動作仕様と、入力条件・出力条件を定義した仕様・設計情報の入力を受ける仕様・設計情報入力部と、前記仕様・設計情報に基づいて、モジュール毎に不具合の有無を検証する検証コードを生成する検証コード生成部と、前記検証コードを用いてモデル検査を実行するモデル検査実行部と、前記モデル検査において不具合を発見した場合に得られる反例から、不具合の存在するモジュールが実行するものではないステップを排除する反例加工部と、前記モデル検査において発見された不具合の有無を出力し、不具合がある場合には、不具合のあるモジュールを提示すると共に、不具合のあるモジュールが実行するものではないステップを排除した反例を出力する検証結果出力部と、を備えたものである。

本発明に係るモデル検査方法は、ソフトウェアまたはシステムを構成するモジュールの動作仕様と、入力条件・出力条件を定義した仕様・設計情報の入力を受ける工程と、前記仕様・設計情報に基づいて、モジュール毎に不具合の有無を検証する検証コードを生成する工程と、前記検証コードを用いてモデル検査を実行する工程と、前記モデル検査において不具合を発見した場合に得られる反例から、不具合の存在するモジュールが実行するものではないステップを排除する工程と、前記モデル検査において発見された不具合の有無を出力し、不具合がある場合には、不具合のあるモジュールを提示すると共に、不具合のあるモジュールが実行するものではないステップを排除した反例を出力する工程と、を備えたものである。

本発明に係るプログラムは、コンピュータを、ソフトウェアまたはシステムを構成するモジュールの動作仕様と、入力条件・出力条件を定義した仕様・設計情報の入力を受ける仕様・設計情報入力部と、前記仕様・設計情報に基づいて、モジュール毎に不具合の有無を検証する検証コードを生成する検証コード生成部と、前記検証コードを用いてモデル検査を実行するモデル検査実行部と、前記モデル検査において不具合を発見した場合に得られる反例から、不具合の存在するモジュールが実行するものではないステップを排除する反例加工部と、前記モデル検査において発見された不具合の有無を出力し、不具合がある場合には、不具合のあるモジュールを提示すると共に、不具合のあるモジュールが実行するものではないステップを排除した反例を出力する検証結果出力部と、して機能させるためのものである。

本発明によれば、システムやソフトウェアの設計が仕様を満たしているか否かを検証するモデル検査において、反例解析の効率を向上させることができる。

本発明の実施の形態１による、モデル検査装置の構成を示すブロック図。 本発明の実施の形態１による、仕様・設計情報の構成を示す図。 本発明の実施の形態１による、モデル検査装置の動作のフローチャート。 本発明の実施の形態１による、検証コード生成部の動作のフローチャート。 本発明の実施の形態１による、検証コード生成部の出力違反検証コード生成の動作のフローチャート。 本発明の実施の形態１による、検証コード生成部の呼出違反検証コード生成の動作のフローチャート。 本発明の実施の形態１による、反例加工部の動作の例フローチャート。 本発明の実施の形態２による、仕様・設計情報の構成を示す図。 本発明の実施の形態２による、仕様・設計情報に含まれるクラス図の例を示す図。 本発明の実施の形態２による、仕様・設計情報に含まれるアクティビティ図の例を示す図。 本発明の実施の形態３による、検証結果出力部で出力されるアクティビティ図の例を示す図。 本発明の実施の形態４による、検証コード生成部で生成されるＰｒｏｍｅｌａで記述された検証コードの例を示す図。

実施の形態１．
次に、本発明を実施するための形態について、図面を参照して詳細に説明する。
図１は、本発明の実施の形態１によるモデル検査装置１の構成を示すブロック図である。
図１に示すように、モデル検査装置１は、仕様・設計情報入力部１１、検証コード生成部１２、モデル検査実行部１３、反例加工部１４、および検証結果出力部１５を備えている。

モデル検査装置１は、ＣＰＵ、ＲＯＭやＲＡＭ等のメモリ、各種の情報を格納する外部記憶装置、入力装置、出力装置、通信インタフェース及びこれらを結ぶバスを備える専用又は汎用のコンピュータを適用することができる。なお、モデル検査装置１は、単一のコンピュータにより構成されるものであっても、通信回線を介して互いに接続された複数のコンピュータにより構成されるものであってもよい。

仕様・設計情報入力部１１、検証コード生成部１２、モデル検査実行部１３、反例加工部１４、および検証結果出力部１５は、ＣＰＵがＲＯＭ等に格納された所定のプログラムを実行することにより実現される機能の単位に相当する。

仕様・設計情報入力部１１は、入力装置を介して、システムあるいはソフトウェアを構成するモジュールの内容と、モジュールの入力条件・出力条件と、を定義した仕様・設計情報の入力を受ける。

図２に示すように、仕様・設計情報Ｄ１１は、各モジュールについてのモジュールの識別子Ｄ１１１１、モジュールが参照する変数名Ｄ１１１２、モジュールの入力条件・出力条件Ｄ１１１３、およびモジュールの動作仕様Ｄ１１１４の情報を含むモジュール情報Ｄ１１１を有している。

検証コード生成部１２は、仕様・設計情報入力部１１から仕様・設計情報Ｄ１１を受信し、モデル検査実行部１３が実行可能な検証コードを生成する。検証コードは、システムあるいはソフトウェアを構成するモジュールの内容とその検証内容を定義している。

ここでは、検証内容は、モジュールが入力条件を満たす入力を受け取った場合に、出力条件を満たさない出力を行なう不具合を意味する出力違反の有無の検証、またはモジュールがその他のモジュールを呼び出す場合に、モジュールがその他のモジュールの入力条件を満たさない入力を行なう不具合を意味する呼出違反の有無の検証、のいずれかであるものとして説明する。ただし、適切な検証コードが生成できるものであれば、検証内容は出力違反の有無または呼出違反の有無に限定されない。

検証コードは、システムあるいはソフトウェアを構成するモジュール毎に、出力違反検証を行なう検証コードと呼出違反検証を行なう検証コードのそれぞれを生成する。すなわち、モジュール１つにつき検証コードが２つ生成されることになるので、モジュールの数がｎ（ｎは自然数）であった場合、検証コードは２ｎ生成される。

モデル検査実行部１３は、検証コード生成部１２で生成された各々の検証コードについてモデル検査を実行し、検証内容の成否である検証結果と、さらに検証内容が満たされない場合にはその反例とを生成する。検証コード１つにつきモデル検査が１回実行され、検証結果が１つと、さらに検証内容が満たされない場合には反例が１つ生成されることになる。したがって、検証コードの数が２ｎであった場合、モデル検査が２ｎ回実行され、検証結果は２ｎ生成され、反例は最大で２ｎ生成される。

反例加工部１４は、モデル検査実行部１３が実行したモデル検査の結果として生成された各々の反例から、出力違反検証あるいは呼出違反検証の対象であるモジュール以外のモジュールのステップを排除し、新たな反例を生成する。反例１つにつき新たな反例が１つ生成されることになるので、反例の数が２ｎであった場合、新たな反例は２ｎ生成される。

検証結果出力部１５は、モデル検査実行部１３が実行したモデル検査の結果である検証結果と、反例加工部１４が生成した新たな反例とをそれぞれ個別に出力する。仕様・設計情報Ｄ１１に含まれるモジュール１つにつき、出力違反検証の結果が１つ、呼出違反検証の結果が１つ生成されることになるので、モジュールの数がｎであった場合、検証結果は２ｎ出力される。また、モジュール１つにつき新たな反例が最大２つ生成されることになるので、モジュールの数がｎであった場合、新たな反例は最大２ｎ出力される。

次に、図３のフローチャートを用いてモデル検査装置１の動作について説明する。
まず、ユーザーは、仕様・設計情報Ｄ１１を作成し、入力装置を介してモデル検査装置１に入力する（ステップＳ１１）。モデル検査装置１は仕様・設計情報入力部１１において仕様・設計情報Ｄ１１を受信する。

次に、検証コード生成部１２において、仕様・設計情報Ｄ１１を検証コードＤ１２に変換する（ステップＳ１２）。

図４を用いて、検証コード生成部１２の詳細な動作について説明する。
まず、検証コード生成部１２は仕様・設計情報Ｄ１１に含まれる全てのモジュールの動作仕様を検証コード化した、ベースとなる検証コードＤ１２１を生成する（ステップＳ１２１）。次に、ベースとなる検証コードＤ１２１のコピーＤ１２１’を１つ生成し、仕様・設計情報Ｄ１１からモジュールＭを１つ抽出する（ステップＳ１２３）。

次に、ベースとなる検証コードＤ１２１を用いて、モジュールＭの出力違反検証コードＤ１２２を生成する（ステップＳ１２４）。さらに、同じくベースとなる検証コードＤ１２１を用いて、呼出違反検証コードＤ１２３を生成する（ステップＳ１２５）。これを、仕様・設計情報Ｄ１１から抽出していないモジュールがなくなるまで繰り返す（ステップＳ１２２）。

モジュール１つにつき検証コードが２つ生成されることになるので、モジュールの数がｎであった場合、検証コードは２ｎ生成される。

図５を用いて、出力違反検証コードＤ１２２の生成について詳細に説明する。
まず、ベースとなる検証コードＤ１２１のコピーＤ１２１’を生成する（ステップＳ１２４１）。次に、抽出したモジュールＭの入力条件の成否を判定する検証コードＤ１２２１を生成し（ステップＳ１２４２）、ベースとなる検証コードＤ１２１のコピーＤ１２１’内の、モジュールＭの動作仕様を表す部分の入力動作の直後に挿入する（ステップＳ１２４３）。

さらに、モジュールＭがその他のモジュールを呼び出す場合には（ステップＳ１２４４：Ｙｅｓ）、呼び出すモジュールのそれぞれについてその出力条件の成否を判定する検証コードＤ１２２２を生成し（ステップＳ１２４５）、ベースとなる検証コードＤ１２１のコピーＤ１２１’内の、各呼出動作の直後にそれぞれ対応する検証コードＤ１２２２を挿入する（ステップＳ１２４６）。

最後に、モジュールＭの出力条件の成否を判定する検証コードＤ１２２３を生成し（ステップＳ１２４７）、ベースとなる検証コードＤ１２１のコピーＤ１２１’内の、モジュールＭの動作仕様を表す部分の出力動作の直前に挿入する（ステップＳ１２４８）。

これらの手順により生成された検証コードを、モジュールＭの出力違反検証コードＤ１２２とする。モジュール１つにつき出力違反検証コードが１つ生成されることになるので、モジュールの数がｎであった場合、出力違反検証コードはｎ生成される。

図６を用いて、呼出違反検証コードＤ１２３の生成について詳細に説明する。
まず、ベースとなる検証コードＤ１２１のコピーＤ１２１’を生成する（ステップＳ１２５１）。

次に、抽出したモジュールＭの入力条件の成否を判定する検証コードＤ１２３１を生成し（ステップＳ１２５２）、ベースとなる検証コードＤ１２１のコピーＤ１２１’内の、モジュールＭの動作仕様を表す部分の入力動作の直後に挿入する（ステップＳ１２５３）。

さらに、モジュールＭがその他のモジュールＭ’を呼び出す場合には（ステップＳ１２５４：Ｙｅｓ）、呼び出すモジュールＭ’のそれぞれについてその入力条件の成否を判定する検証コードＤ１２３２を生成し（ステップＳ１２５５）、ベースとなる検証コードＤ１２１のコピーＤ１２１’内の、各呼出動作の直前にそれぞれ対応する検証コードＤ１２３２を挿入する（ステップＳ１２５６）。

これらの手順により生成された検証コードを、モジュールＭの呼出違反検証コードＤ１２３とする。モジュール１個につき呼出違反検証コードが１つ生成されることになるので、モジュールの数がｎであった場合、呼出違反検証コードはｎ生成される。

モデル検査実行部１３は、検証コード生成部１２で生成された検証コードＤ１２のそれぞれに対して個別にモデル検査を実行し、検証結果Ｄ１３と、さらに検証内容が満たされない場合には反例Ｄ１４とを生成する（図３、ステップＳ１３）。

検証コード１つにつきモデル検査が１回実行され、検証結果が１つと、検証内容が満たされない場合には反例が１つと、が生成されることになるので、検証コードの数が２ｎであった場合、モデル検査が２ｎ回実行され、検証結果は２ｎ個生成され、反例は最大で２ｎ個生成される。

反例加工部１４は、反例Ｄ１４をそれぞれ解析し、出力違反検証あるいは呼出違反検証の対象だったモジュールを特定する。さらに、検証の対象だったモジュールのものではないステップを反例Ｄ１４から排除し、新たな反例Ｄ１５を生成する（ステップＳ１４）。

図７を用いて反例加工部１４の動作の一例について説明する。
まず、反例加工部１４は、反例Ｄ１４内のステップを先頭から順に抽出し（ステップＳ１４１）、出力違反検証コード生成や呼出違反検証コード生成により挿入された検証コードであるか否か判断してゆく（ステップＳ１４２）。

当該ステップが出力違反検証コード生成や呼出違反検証コード生成によって挿入された検証コードであった場合（Ｙｅｓ）、ステップを行なったモジュールを検証の対象だったモジュールと特定する（ステップＳ１４３）。さらに、反例Ｄ１４に他のステップが残っている場合には、ステップＳ１４５に進む。

ステップＳ１４２で、当該ステップが出力違反検証コード生成や呼出違反検証コード生成によって挿入された検証コードではない場合には、ステップＳ１４１に戻り次のステップを抽出する。

検証の対象だったモジュールの特定が完了したら、改めて反例Ｄ１４内の次のステップＤ１４２を先頭から順に抽出し（ステップＳ１４５）、検証の対象だったモジュールのものではないステップを削除してゆく（ステップＳ１４６，Ｓ１４７）。

以上の手順により生成された反例を、新たな反例Ｄ１５とする。この動作は一例であり、検証の対象だったモジュールが特定でき、かつ、検証の対象だったモジュールのものではないステップが適切に削除できるのであれば、これ以外の動作により新たな反例Ｄ１５を生成してもよい。反例１つにつき新たな反例が１つ生成されることになるので、反例の数が２ｎ個であった場合、新たな反例は２ｎ個生成される。

検証結果出力部１５は、検証結果Ｄ１３と、新たな反例Ｄ１５とを参照し、仕様・設計情報Ｄ１１に含まれる各モジュールに出力違反あるいは呼出違反があるかどうかの検証結果Ｄ１３と、違反の可能性がある場合にその一例であるシーケンスとして新たな反例Ｄ１５とをそれぞれ個別に出力する（図３、ステップＳ１５）。

仕様・設計情報Ｄ１１に含まれるモジュール１つにつき、出力違反検証の結果が１つ、呼出違反検証の結果が１つ生成されることになるので、モジュールの数がｎ個であった場合、検証結果は２ｎ回出力される。また、モジュール１つにつき新たな反例が最大２個生成されることになるので、モジュールの数がｎであった場合、新たな反例は最大２ｎ回出力される。
ユーザーは、ステップＳ１５で出力された結果を確認する（ステップＳ１６）。

以上のように、本実施形態によれば、検証コード生成部１２でソフトウェアあるいはシステムを構成するモジュールの不具合（出力違反あるいは呼出違反）の有無を検証する検証コードをモジュール毎に生成し、モデル検査実行部１３で検証コードのそれぞれに対してモデル検査を実行して不具合が発見された場合にはその反例を生成し、反例加工部１４で反例から不具合の存在するモジュールのものではないステップを排除する。これにより、不具合の存在するモジュールを特定すると共に不具合とは無関係なステップを解析する手間が削減されるため、反例解析の効率を向上させることができる。

なお、本実施形態では、検証内容として出力違反の有無及び呼出違反の有無の検証を例に挙げているが、適切な検証コードが生成できるのであれば、検証内容は出力違反及び呼出違反の有無に限定されるものではない。

実施の形態２．
実施の形態２では、仕様・設計情報入力部１１に入力される仕様・設計情報Ｄ１１は、図８に示すように、システムあるいはソフトウェアを構成するモジュールを定義したクラス図及びアクティビティ図を含む。

仕様・設計情報Ｄ１１のモデル検査装置１への入力は、キーボードやマウス等の入力装置を介して行なわれる。図８に示すように、クラス図Ｄ１１２１では、各モジュールについて、クラスが持つメソッド名として各モジュールの識別子Ｄ１１１１（図２のモジュールの識別子Ｄ１１１１に対応）を定義している。

また、クラスが持つ属性名として各モジュールが参照する変数名Ｄ１１１２（図２のモジュールが参照する変数名Ｄ１１１２に対応）を定義している。さらに、各モジュールの入力条件・出力条件（図２のモジュールの入力条件・出力条件Ｄ１１１４に対応）を定義している。図９にクラス図Ｄ１１２１の例を示す。

また、アクティビティ図Ｄ１１２２では、各モジュールに関して、モジュールの動作仕様Ｄ１１２２１（図２のモジュールの動作仕様Ｄ１１１４に対応）を定義している。図１０にアクティビティ図Ｄ１１２２の例を示す。

ユーザーは、システムあるいはソフトウェアを構成するモジュールを定義したクラス図Ｄ１１２１及びアクティビティ図Ｄ１１２２を含む仕様・設計情報Ｄ１１を作成し、入力装置を介してモデル検査装置１に入力する。モデル検査装置１は入力された仕様・設計情報Ｄ１１に基づいて実施の形態１と同様に動作し、検証結果および反例を生成して出力する。

実施の形態３．
実施の形態３では、検証結果出力部１５は、モデル検査を実行したＳｐｉｎ（モデル検査ツール）の出力を参照し、検証内容を満たさないモジュールがあれば、どの部分が満たさないのかをアクティビティ図上で示す形式でディスプレイ（出力装置）に表示する。

また、反例加工部１４が生成した新たな反例をファイルとして出力する。仕様・設計情報Ｄ１１に含まれるモジュール１つにつき、検証結果は最大２つ生成されることになるので、モジュールの数がｎ個であった場合、検証内容を満たさない部分は最大２ｎ箇所出力される。また、モジュール１つにつき新たな反例が最大２回生成されることになるので、モジュールの数がｎ個であった場合、新たな反例は最大２ｎ個のファイルに出力される。

実施の形態３によるモデル検査装置１の動作について図３を用いて説明する。
検証結果出力部１５は、検証結果Ｄ１３を参照し、ステップＳ１４で実行したモデル検査の結果をディスプレイに表示する（ステップＳ１５）。検証内容を満たさないモジュールがあれば、どの部分が満たさないのかをアクティビティ図上で示す形式でディスプレイに表示する。

また、反例加工部１４が生成した新たな反例Ｄ１５をファイルとして出力する。仕様・設計情報Ｄ１１に含まれるモジュール１つにつき、検証結果は最大２ｎ個生成されることになるので、モジュールの数がｎ個であった場合、検証結果を満たさない部分は最大２ｎ箇所ディスプレイに出力される。また、モジュール１個につき新たな反例が最大２回生成されることになるのでモジュールの数がｎ個であった場合、新たな反例は最大２ｎ個のファイルに出力される。

ステップＳ１１で仕様・設計情報入力部１１に図９のクラス図及び図１０のアクティビティ図を入力した場合に、ステップＳ１５で出力されるアクティビティ図の例を図１１に示す。図１１に示したアクティビティ図は、ｍａｉｎモジュールで呼出違反が起こることを表している。

実施の形態４．
実施の形態４では、検証コード生成部１２は、仕様・設計情報Ｄ１１から、モデル検査ツールＳｐｉｎの入力言語Ｐｒｏｍｅｌａで記述された検証コードを生成する。生成する検証コードは、実施の形態１と同様の特徴を持つ。

また、モデル検査実行部１３は、モデル検査ツールＳｐｉｎである。検証結果は、モデル検査を実行したＳｐｉｎの出力である。本実施形態のＳｐｉｎのバージョンは６．１．０とするが、その他のバージョンを用いてもよい。また、Ｓｐｉｎ以外のモデル検査ツールを用いてもよい。

反例加工部１４は、Ｓｐｉｎが実行したモデル検査の結果として生成された反例のそれぞれから、出力違反検証あるいは呼出違反検証の対象となったモジュール以外のステップを排除し新たな反例を生成する。

実施の形態４によるモデル検査装置１の動作について図３〜６を用いて説明する。
検証コード生成部１２では、仕様・設計情報Ｄ１１を検証コードに変換する（ステップＳ１２）。具体的には、クラス図Ｄ１１２１で定義されている各モジュールをそれぞれＰｒｏｍｅｌａプロセスとして宣言し、各モジュールの動作仕様Ｄ１１２２１を各Ｐｒｏｍｅｌａプロセスの動作として定義する。

さらに、各モジュールの入力条件・出力条件の成否を格納するｂｏｏｌ型の変数（以下、成否格納変数）を対応する各Ｐｒｏｍｅｌａプロセス内で宣言し、各モジュールが参照する変数名Ｄ１１２１２を変換しＰｒｏｍｅｌａのグローバル変数として宣言する。

ここまでの手順で生成された検証コードを、ベースとなる検証コードＤ１２１とする（ステップＳ１２１）。次に、ベースとなる検証コードＤ１２１のコピーＤ１２１’を１つ生成し、仕様・設計情報Ｄ１１からモジュールＭを１つ抽出する（ステップＳ１２３）。

ベースとなる検証コードＤ１２１を用いて、モジュールＭの出力違反検証コードＤ１２２を生成する（ステップＳ１２４）。さらに、同じくベースとなる検証コードＤ１２１を用いて、呼出違反検証コードＤ１２３を生成する（ステップＳ１２５）。これを、仕様・設計情報Ｄ１１から抽出していないモジュールがなくなるまで繰り返す（ステップＳ１２２）。

モジュール１つにつき検証コードが２つ生成されることになるので、モジュールの数がｎ個であった場合、検証コードは２ｎ個生成される。

出力違反検証コードＤ１２２生成のより詳細な動作に関して、図５を参照して説明する。まず、ベースとなる検証コードＤ１２１のコピーＤ１２１’を生成する（ステップＳ１２４１）。

次に、抽出したモジュールＭの入力条件が満たされる場合はｔｒｕｅ、満たされない場合はｆａｌｓｅを入力条件の成否格納変数に代入する検証コードＤ１２２１を生成し（ステップＳ１２４２）、ベースとなる検証コードＤ１２１のコピーＤ１２１’内の、モジュールＭに対応するＰｒｏｍｅｌａプロセス内の入力動作の直後に挿入する（ステップＳ１２４３）。

さらに、モジュールＭがその他のモジュールＭ’を呼び出す場合には（ステップＳ１２４４）、呼び出すモジュールＭ’のそれぞれについて、その出力条件が満たされる場合にはｔｒｕｅ、満たされない場合にはｆａｌｓｅを、呼び出すモジュールの出力条件の成否格納変数に代入する検証コードＤ１２２２を生成する（ステップＳ１２４５）。

さらに、ベースとなる検証コードＤ１２１のコピーＤ１２１’内の、各呼出動作の直後にそれぞれ対応する検証コードＤ１２２２を挿入する（ステップＳ１２４６）。

最後に、これまでの手順で挿入した検証コードで使用している成否格納変数が全てｔｒｕｅである場合にモジュールＭの出力条件の成否を判定する検証コードＤ１２２３（例えばａｓｓｅｒｔ文）を生成し（ステップＳ１２４７）、ベースとなる検証コードＤ１２１のコピーＤ１２１’内の、モジュールＭに対応するＰｒｏｍｅｌａプロセス内の出力動作の直前に挿入する（ステップＳ１２４８）。

以上の手順により生成された検証コードを、モジュールＭの出力違反検証コードＤ１２２とする。モジュール１つにつき出力違反検証コードが１個生成されることになるので、モジュールの数がｎ個であった場合、出力違反検証コードはｎ個生成される。

呼出違反検証コードＤ１２３生成のより詳細な動作に関して、図６を参照して説明する。まず、ベースとなる検証コードＤ１２１のコピーＤ１２１’を生成する（ステップＳ１２５１）。

次に、抽出したモジュールＭの入力条件が満たされる場合はｔｒｕｅ、満たされない場合はｆａｌｓｅを入力条件の成否格納変数に代入する検証コードＤ１２３１を生成する（ステップＳ１２５２）。

さらに、ベースとなる検証コードＤ１２１のコピーＤ１２１’内の、モジュールＭに対応するＰｒｏｍｅｌａプロセス内の入力動作の直後に挿入する（ステップＳ１２５３）。

さらに、モジュールＭがその他のモジュールＭ’を呼び出す場合には（ステップＳ１２５４）、呼び出すモジュールＭ’のそれぞれについて、これまでの手順で挿入した検証コードで使用している成否格納変数が全てｔｒｕｅである場合にモジュールＭ’の入力条件が満たされる場合はｔｒｕｅ、満たされない場合はｆａｌｓｅを、呼び出すモジュールＭ’の入力条件の成否格納変数に代入し、さらにその成否を判定する検証コードＤ１２３２を生成する（ステップＳ１２５５）。

さらに、ベースとなる検証コードＤ１２１のコピーＤ１２１’内の、各呼出動作の直前にそれぞれ対応する検証コードＤ１２３２を挿入する（ステップＳ１２５６）。ここで、検証コードＤ１２３２の生成手順における「これまでの手順で挿入した検証コード」とは、呼び出すモジュールＭ’が複数ある場合、その２つ目以降においては、その前までに呼び出されるモジュールＭ’の入力条件の成否格納変数への代入を行なう検証コードを含む。

以上の手順により生成された検証コードを、モジュールＭの呼出違反検証コードＤ１２３とする。モジュール１つにつき呼出違反検証コードが１つ生成されることになるので、モジュールの数がｎ個であった場合、呼出違反検証コードはｎ個生成される。

検証コード生成部１２が生成する検証コードの例として、図９に示すクラス図及び図１０に示すアクティビティ図を変換した例を図１２に示す。図１２に示す検証コードは、各モジュールの出力違反検証・呼出違反検証の全てについて、それらを行なう検証コードを挿入し生成したものである。実際には前述のように、ステップＳ１２において、各モジュールの出力違反検証・呼出違反検証を行なう検証コードは、それぞれ個別に生成される。

例えば図９のクラス図及び図１０のアクティビティ図を入力とした場合、ｍａｉｎモジュールの出力違反検証を行なう検証コードと、ｍａｉｎモジュールの呼出違反検証を行なう検証コードと、ｍｅｔｈｏｄＡモジュールの出力違反検証を行なう検証コードと、ｍｅｔｈｏｄＡモジュールの呼出違反検証を行なう検証コード、の４つの検証コードが生成される。

ただしこの場合、ｍａｉｎモジュールは出力条件が定義されておらず、また、ｍｅｔｈｏｄＡモジュールはその他のモジュールを呼び出さないため、ｍａｉｎモジュールの出力違反検証を行なう検証コード及びｍｅｔｈｏｄＡモジュールの呼出違反検証を行なう検証コードは用を成さない検証コードとなる。

この例に限らず、モジュールに出力条件が定義されていない場合の出力違反検証コードと、モジュールがその他のモジュールを呼び出さない場合の呼出違反検証コードは用を成さないため、その場合は検証コードを生成しないことにしてもよい。

また、生成する検証コードは、出力違反と呼出違反の適切な検証が可能であれば図１２に示す形式のものに限らず、その他の変換方式により生成してもよい。

モデル検査実行部１３（Ｓｐｉｎ）は、検証コード生成部１２で生成された検証コードＤ１２のそれぞれに対してモデル検査を実行し、検証結果Ｄ１３と、検証内容が満たされない場合には反例Ｄ１４と、を生成する（ステップＳ１３）。

検証コード１つにつきモデル検査が１回実行され、検証結果が１個と、検証内容が満たされない場合には反例が１個とが生成されることになるので、検証コードの数が２ｎ個であった場合、モデル検査が２ｎ回実行され、検証結果は２ｎ個生成され、反例は最大で２ｎ個生成される。

反例加工部１４は、反例Ｄ１４をそれぞれ解析し、出力違反検証あるいは呼出違反検証の対象だったモジュールを特定する。さらに、前記検証の対象だったモジュール以外のモジュールのステップを反例から排除し、新たな反例Ｄ１５を生成する（ステップＳ１４）。

反例加工部１４の動作の一例を、図７を参照して説明する。反例Ｄ１４内のステップを先頭から順に抽出し（ステップＳ１４１）、出力違反検証コード生成（ステップＳ１２４）や呼出違反検証コード生成（ステップＳ１２５）により挿入された検証コード（例えばａｓｓｅｒｔ文）であるか否かを判断してゆく。

当該ステップが挿入された検証コードであった場合、そのステップを行なったプロセスに対応するモジュールを検証の対象だったモジュールと特定する（ステップＳ１４３）。当該ステップが挿入された検証コードでない場合には、次のステップを抽出する。検証の対象だったモジュールの特定が完了したら、改めて反例Ｄ１４内のステップを先頭から順に抽出し（ステップＳ１４５）、検証の対象だったモジュールに対応するプロセスのものではないステップを削除してゆく（ステップＳ１４７）。

これらの手順により生成された反例を、新たな反例Ｄ１５とする。なお、この動作は一例であり、検証の対象だったモジュールが特定でき、かつ、検証の対象だったモジュールのものではないステップが適切に削除できるのであれば、これ以外の動作により新たな反例Ｄ１５を生成してもよい。

上記の実施の形態の一部または全部は、以下の付記のようにも記載されうるが、以下には限られない。
（付記１）ソフトウェアまたはシステムを構成するモジュールの動作仕様と、入力条件・出力条件を定義した仕様・設計情報の入力を受ける仕様・設計情報入力部と、
前記仕様・設計情報に基づいて、モジュール毎に不具合の有無を検証する検証コードを生成する検証コード生成部と、
前記検証コードを用いてモデル検査を実行するモデル検査実行部と、
前記モデル検査において不具合を発見した場合に得られる反例から、不具合の存在するモジュールが実行するものではないステップを排除する反例加工部と、
前記モデル検査において発見された不具合の有無を出力し、不具合がある場合には、不具合のあるモジュールを提示すると共に、不具合のあるモジュールが実行するものではないステップを排除した反例を出力する検証結果出力部と、を備えたモデル検査装置。

（付記２）前記検証コード生成部は、
前記モジュールが入力条件を満たす入力を受信した際に、前記モジュールが出力条件を満たさない出力を行なう不具合である出力違反の検証を行なう出力違反検証コードと、
前記モジュールがその他のモジュールを呼び出す際に、前記モジュールが前記その他のモジュールの入力条件を満たさない入力を行なう不具合である呼出違反の検証を行なう呼出違反検証コードと、をモジュール毎に生成する、付記１に記載のモデル検査装置。

（付記３）前記検証コード生成部は、
前記モジュールに出力条件が定義されていない場合、前記モジュールの前記出力違反検証コードを生成せず、前記モジュールがその他のモジュールを呼び出さない場合、前記モジュールの前記呼出違反検証コードを生成しない、付記２に記載のモデル検査装置。

（付記４）前記仕様・設計情報は、
各モジュールの識別子と、各モジュールが参照する変数名と、各モジュールの入力条件・出力条件と、を定義したクラス図と、
各モジュールの動作仕様を定義したアクティビティ図と、を含む、付記１から３のいずれか１項に記載のモデル検査装置。

（付記５）前記検証結果出力部は、不具合のあるモジュールを示すにあたり、前記仕様・設計情報に含まれるアクティビティ図における不具合の発生箇所を示す、付記４に記載のモデル検査装置。

（付記６）ソフトウェアまたはシステムを構成するモジュールの動作仕様と、入力条件・出力条件を定義した仕様・設計情報の入力を受ける工程と、
前記仕様・設計情報に基づいて、モジュール毎に不具合の有無を検証する検証コードを生成する工程と、
前記検証コードを用いてモデル検査を実行する工程と、
前記モデル検査において不具合を発見した場合に得られる反例から、不具合の存在するモジュールが実行するものではないステップを排除する工程と、
前記モデル検査において発見された不具合の有無を出力し、不具合がある場合には、不具合のあるモジュールを提示すると共に、不具合のあるモジュールが実行するものではないステップを排除した反例を出力する工程と、を備えたモデル検査方法。

（付記７）コンピュータを、
ソフトウェアまたはシステムを構成するモジュールの動作仕様と、入力条件・出力条件を定義した仕様・設計情報の入力を受ける仕様・設計情報入力部と、
前記仕様・設計情報に基づいて、モジュール毎に不具合の有無を検証する検証コードを生成する検証コード生成部と、
前記検証コードを用いてモデル検査を実行するモデル検査実行部と、
前記モデル検査において不具合を発見した場合に得られる反例から、不具合の存在するモジュールが実行するものではないステップを排除する反例加工部と、
前記モデル検査において発見された不具合の有無を出力し、不具合がある場合には、不具合のあるモジュールを提示すると共に、不具合のあるモジュールが実行するものではないステップを排除した反例を出力する検証結果出力部と、して機能させるためのプログラム。

本発明は、システム開発やソフトウェア開発における設計の妥当性を検証するツールに適用できる。

１ モデル検査装置、１１ 仕様・設計情報入力部、１２ 検証コード生成部、１３ モデル検査実行部、１４ 反例加工部、１５ 検証結果出力部、Ｄ１１ 仕様・設計情報、Ｄ１２ 検証コード、Ｄ１３ 検証結果、Ｄ１４ 反例、Ｄ１５ 新たな反例

Claims (7)

1. ソフトウェアまたはシステムを構成するモジュールの動作仕様と、入力条件・出力条件を定義した仕様・設計情報の入力を受ける仕様・設計情報入力部と、
   前記仕様・設計情報に基づいて、モジュール毎に不具合の有無を検証する検証コードを生成する検証コード生成部と、
   前記検証コードを用いてモデル検査を実行するモデル検査実行部と、
   前記モデル検査において不具合を発見した場合に得られる反例から、不具合の存在するモジュールが実行するものではないステップを排除する反例加工部と、
   前記モデル検査において発見された不具合の有無を出力し、不具合がある場合には、不具合のあるモジュールを提示すると共に、不具合のあるモジュールが実行するものではないステップを排除した反例を出力する検証結果出力部と、を備えたモデル検査装置。
2. 前記検証コード生成部は、
   前記モジュールが入力条件を満たす入力を受信した際に、前記モジュールが出力条件を満たさない出力を行なう不具合である出力違反の検証を行なう出力違反検証コードと、
   前記モジュールがその他のモジュールを呼び出す際に、前記モジュールが前記その他のモジュールの入力条件を満たさない入力を行なう不具合である呼出違反の検証を行なう呼出違反検証コードと、をモジュール毎に生成する、請求項１に記載のモデル検査装置。
3. 前記検証コード生成部は、
   前記モジュールに出力条件が定義されていない場合、前記モジュールの前記出力違反検証コードを生成せず、前記モジュールがその他のモジュールを呼び出さない場合、前記モジュールの前記呼出違反検証コードを生成しない、請求項２に記載のモデル検査装置。
4. 前記仕様・設計情報は、
   各モジュールの識別子と、各モジュールが参照する変数名と、各モジュールの入力条件・出力条件と、を定義したクラス図と、
   各モジュールの動作仕様を定義したアクティビティ図と、を含む、請求項１から３のいずれか１項に記載のモデル検査装置。
5. 前記検証結果出力部は、不具合のあるモジュールを示すにあたり、前記仕様・設計情報に含まれるアクティビティ図における不具合の発生箇所を示す、請求項４に記載のモデル検査装置。
6. ソフトウェアまたはシステムを構成するモジュールの動作仕様と、入力条件・出力条件を定義した仕様・設計情報の入力を受ける工程と、
   前記仕様・設計情報に基づいて、モジュール毎に不具合の有無を検証する検証コードを生成する工程と、
   前記検証コードを用いてモデル検査を実行する工程と、
   前記モデル検査において不具合を発見した場合に得られる反例から、不具合の存在するモジュールが実行するものではないステップを排除する工程と、
   前記モデル検査において発見された不具合の有無を出力し、不具合がある場合には、不具合のあるモジュールを提示すると共に、不具合のあるモジュールが実行するものではないステップを排除した反例を出力する工程と、を備えたモデル検査方法。
7. コンピュータを、
   ソフトウェアまたはシステムを構成するモジュールの動作仕様と、入力条件・出力条件を定義した仕様・設計情報の入力を受ける仕様・設計情報入力部と、
   前記仕様・設計情報に基づいて、モジュール毎に不具合の有無を検証する検証コードを生成する検証コード生成部と、
   前記検証コードを用いてモデル検査を実行するモデル検査実行部と、
   前記モデル検査において不具合を発見した場合に得られる反例から、不具合の存在するモジュールが実行するものではないステップを排除する反例加工部と、
   前記モデル検査において発見された不具合の有無を出力し、不具合がある場合には、不具合のあるモジュールを提示すると共に、不具合のあるモジュールが実行するものではないステップを排除した反例を出力する検証結果出力部と、して機能させるためのプログラム。