(57)【要約】【課題】部分検証範囲の特定や、呼び出し関係があるモジュール間で満たすべき条件の設定を行うことなくソフトウェアの検証を行うことができるようにする。【解決手段】中央処理装置１１１は、起点モジュールｍｓから、前条件無しで性質ｐが守られるか否かを判定する。判定不能の場合、性質ｐを含むモジュールを呼び出す可能性がある下位モジュールを起点モジュールｍｓとして、前条件無しで性質ｐが守られるか否かを判定する。性質ｐが守られないと判定した場合、性質ｐが守られないための条件Ｃｆを求め、最上位のモジュールから検証対象のモジュールの開始時までの処理結果において、条件Ｃｆが成り立つか否かを判定する。条件Ｃｆが成り立たないと判定した場合、検証対象のモジュールの検証結果を「性質ｐは守られる」とする。全ての下位モジュールに対して性質ｐが守られると判定した場合、ｍｓの検証結果Ｒｓを「性質ｐは守られる」とする。【選択図】図１
2008203977.tif 000002
【特許請求の範囲】
【請求項１】
複数のモジュールに分割可能なソフトウェアを検証するソフトウェア検証装置であって、
ソフトウェアを構成するモジュールを検証対象として、検証対象のモジュールについて前条件なしで所定の検証事項が成り立つか否かを判定する判定手段と、
前記判定手段が検証事項が成り立たない場合があると判定した場合に、前記検証対象のモジュールの開始時における検証事項が成り立たないための条件を算出する条件算出手段と、
モジュール間の呼び出し関係における最上位のモジュールから前記検証対象のモジュールの開始時までの処理結果において、前記条件算出手段が算出した条件が成り立つか否かを判定する条件判定手段と、
前記条件判定手段の判定に基づいて、前記検証対象のモジュールについて検証事項が成り立つか否かを判定し、前記条件判定手段が条件が成り立たないと判定した場合に、前記検証対象のモジュールについて検証事項が成り立つと判定するモジュール判定手段と、
前記モジュール判定手段の判定に基づいて、前記ソフトウェアについて所定の検証事項が成り立つか否かを判定するソフトウェア判定手段と
を備えたことを特徴とするソフトウェア検証装置。
【請求項２】
判定手段は、検証対象のモジュールについて、検証事項が成り立つか否かを判定不能である場合に、検証事項を含むモジュールを呼び出す可能性のある下位モジュールを順次検証対象として、前条件なしで検証事項が成り立つか否かを判定し、
モジュール判定手段は、前記判定手段または前記モジュール判定手段がすべての下位モジュールについて検証事項が成り立つと判定した場合に、上位の検証対象のモジュールについて検証事項が成り立つと再帰的に判定する
請求項１記載のソフトウェア検証装置。
【請求項３】
判定手段は、モジュール間の呼び出し関係における最上位のモジュールを検証対象として検証事項が成り立つか否かを判定し、
ソフトウェア判定手段は、前記判定手段またはモジュール判定手段がすべての下位モジュールについて検証事項が成り立つと判定した場合に、ソフトウェア全体について検証事項が成り立つと判定する
請求項１または請求項２記載のソフトウェア検証装置。
【請求項４】
ソフトウェア検証装置は、検証結果を出力する出力装置または検証結果を記憶する記憶装置を備え、
ソフトウェア判定手段は、判定した結果を前記出力装置または前記記憶装置に出力する
請求項１から請求項３のうちのいずれか１項に記載のソフトウェア検証装置。
【請求項５】
複数のモジュールに分割可能なソフトウェアを検証するソフトウェア検証方法であって、
ソフトウェアを構成するモジュールを検証対象として、検証対象のモジュールについて前条件なしで所定の検証事項が成り立つか否かを判定する判定ステップと、
前記判定ステップで検証事項が成り立たない場合があると判定した場合に、前記検証対象のモジュールの開始時における検証事項が成り立たないための条件を算出する条件算出ステップと、
モジュール間の呼び出し関係における最上位のモジュールから前記検証対象のモジュールの開始時までの処理結果において、前記条件算出ステップで算出した条件が成り立つか否かを判定する条件判定ステップと、
前記条件判定ステップでの判定に基づいて、前記検証対象のモジュールについて検証事項が成り立つか否かを判定し、前記条件判定ステップで条件が成り立たないと判定した場合に、前記検証対象のモジュールについて検証事項が成り立つと判定するモジュール判定ステップと、
前記モジュール判定ステップでの判定に基づいて、前記ソフトウェアについて所定の検証事項が成り立つか否かを判定するソフトウェア判定ステップと
を含むことを特徴とするソフトウェア検証方法。
【請求項６】
複数のモジュールに分割可能なソフトウェアを検証するためのソフトウェア検証プログラムであって、
コンピュータに、
ソフトウェアを構成するモジュールを検証対象として、検証対象のモジュールについて前条件なしで所定の検証事項が成り立つか否かを判定する判定処理と、
前記判定処理で検証事項が成り立たない場合があると判定した場合に、前記検証対象のモジュールの開始時における検証事項が成り立たないための条件を算出する条件算出処理と、
モジュール間の呼び出し関係における最上位のモジュールから前記検証対象のモジュールの開始時までの処理結果において、前記条件算出処理で算出した条件が成り立つか否かを判定する条件判定処理と、
前記条件判定処理での判定に基づいて、前記検証対象のモジュールについて検証事項が成り立つか否かを判定し、前記条件判定処理で条件が成り立たないと判定した場合に、前記検証対象のモジュールについて検証事項が成り立つと判定するモジュール判定処理と、
前記モジュール判定処理での判定に基づいて、前記ソフトウェアについて所定の検証事項が成り立つか否かを判定するソフトウェア判定処理と
を実行させるためのソフトウェア検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、複数のモジュールに分割可能なソフトウェアを検証するソフトウェア検証装置、ソフトウェア検証方法およびソフトウェア検証プログラムに関する。
【背景技術】
【０００２】
大規模なソフトウェアを対象にその動作の正しさを検証する際、部分的な検証から全体を検証する方法として、ホーアの提唱した理論（ホーア理論）（非特許文献１参照。）や、メイヤーにより提唱された契約によるプログラミング（非特許文献２参照。）が知られている。
【０００３】
ホーア理論での複合文の規則によれば、プログラムを複数の部分プログラムに分割し、分割した部分プログラム間で満たすべき条件（前に処理される部分プログラムの後条件であり、かつ、次に処理される部分プログラムの前条件）を与えると、それらの条件を元に部分プログラムを検証することにより元のプログラムの検証ができる。また、契約によるプログラミングによれば、プログラムを構成するルーチンの前条件・後条件を表明として与えることにより、プログラム全体が適切に動作することを検証できる。いずれの場合もプログラムを適切な部分に分割し、分割した部分に対して処理前および処理後の条件を適切に与えることにより、プログラム全体を検証することができる。
【０００４】
【非特許文献１】林晋著、「プログラム検証論」、共立出版、１９９５年９月１日、ｐｐ．２８
【非特許文献２】Bertrand Meyer著、二木厚吉監訳、「オブジェクト指向入門」、アスキー出版、１９９０年１１月２１日、ｐｐ．１５３−１６８
【発明の開示】
【発明が解決しようとする課題】
【０００５】
非特許文献１，２に記載された方式では、検証作業者が対象ソフトウェアを複数のモジュールに分割し、呼び出し関係のあるモジュール間で満たすべき条件（呼び出す側の後条件であり、かつ、呼び出される側の前条件）を設定する。そして、その条件の下で、分割した個々のモジュールを次々と個別に検証し、すべてのモジュールの検証結果を得ることで、対象ソフトウェア全体を検証する。この場合、検証作業者は、あらかじめ、検証の際にメモリ使用量がシステムのメモリ容量を超えず、許容可能な時間内で検証が完了するよう、いくつかのモジュールに適切に分割して検証する範囲を定め、かつ、呼び出し関係のあるモジュール間で満たすべき条件を適切に設定しなければならない。
【０００６】
そこで、本発明は、部分検証範囲の特定や、呼び出し関係があるモジュール間で満たすべき条件の設定を行うことなくソフトウェアの検証を行うことができるソフトウェア検証装置、ソフトウェア検証方法およびソフトウェア検証プログラムを提供することを目的とする。
【課題を解決するための手段】
【０００７】
本発明によるソフトウェア検証装置は、複数のモジュールに分割可能なソフトウェアを検証するソフトウェア検証装置であって、ソフトウェアを構成するモジュールを検証対象として、検証対象のモジュールについて前条件なしで所定の検証事項が成り立つか否かを判定する判定手段（例えば、中央処理装置１１１）と、判定手段が検証事項が成り立たない場合があると判定した場合に、検証対象のモジュールの開始時における検証事項が成り立たないための条件を算出する条件算出手段（例えば、中央処理装置１１１）と、モジュール間の呼び出し関係における最上位のモジュールから検証対象のモジュールの開始時までの処理結果において、条件算出手段が算出した条件が成り立つか否かを判定する条件判定手段（例えば、中央処理装置１１１）と、条件判定手段の判定に基づいて、検証対象のモジュールについて検証事項が成り立つか否かを判定し、条件判定手段が条件が成り立たないと判定した場合に、検証対象のモジュールについて検証事項が成り立つと判定するモジュール判定手段（例えば、中央処理装置１１１）と、モジュール判定手段の判定に基づいて、ソフトウェアについて所定の検証事項が成り立つか否かを判定するソフトウェア判定手段（例えば、中央処理装置１１１）とを備えたことを特徴とする。
【０００８】
判定手段は、検証対象のモジュールについて、検証事項が成り立つか否かを判定不能である場合に、検証事項を含むモジュールを呼び出す可能性のある下位モジュールを順次検証対象として、前条件なしで検証事項が成り立つか否かを判定し、モジュール判定手段は、判定手段またはモジュール判定手段がすべての下位モジュールについて検証事項が成り立つと判定した場合に、上位の検証対象のモジュールについて検証事項が成り立つと再帰的に判定することが望ましい。そのような構成によれば、正確かつ効率的に検証を行うことができる。
【０００９】
判定手段は、モジュール間の呼び出し関係における最上位のモジュールを検証対象として検証事項が成り立つか否かを判定し、ソフトウェア判定手段は、判定手段またはモジュール判定手段がすべての下位モジュールについて検証事項が成り立つと判定した場合に、ソフトウェア全体について検証事項が成り立つと判定することが望ましい。そのような構成によれば、ソフトウェア全体について検証を行うことができる。
【００１０】
ソフトウェア検証装置は、検証結果を出力する出力装置（例えば、出力装置１１２）または検証結果を記憶する記憶装置（例えば、二次記憶装置１１４）を備え、ソフトウェア判定手段は、判定した結果を出力装置または記憶装置に出力してもよい。そのような構成によれば、検証結果を出力または記憶することができる。
【００１１】
本発明によるソフトウェア検証方法は、複数のモジュールに分割可能なソフトウェアを検証するソフトウェア検証方法であって、ソフトウェアを構成するモジュールを検証対象として、検証対象のモジュールについて前条件なしで所定の検証事項が成り立つか否かを判定する判定ステップと、判定ステップで検証事項が成り立たない場合があると判定した場合に、検証対象のモジュールの開始時における検証事項が成り立たないための条件を算出する条件算出ステップと、モジュール間の呼び出し関係における最上位のモジュールから検証対象のモジュールの開始時までの処理結果において、条件算出ステップで算出した条件が成り立つか否かを判定する条件判定ステップと、条件判定ステップでの判定に基づいて、検証対象のモジュールについて検証事項が成り立つか否かを判定し、条件判定ステップで条件が成り立たないと判定した場合に、検証対象のモジュールについて検証事項が成り立つと判定するモジュール判定ステップと、モジュール判定ステップでの判定に基づいて、ソフトウェアについて所定の検証事項が成り立つか否かを判定するソフトウェア判定ステップとを含むことを特徴とする。
【００１２】
本発明によるソフトウェア検証プログラムは、複数のモジュールに分割可能なソフトウェアを検証するためのソフトウェア検証プログラムであって、コンピュータに、ソフトウェアを構成するモジュールを検証対象として、検証対象のモジュールについて前条件なしで所定の検証事項が成り立つか否かを判定する判定処理と、判定処理で検証事項が成り立たない場合があると判定した場合に、検証対象のモジュールの開始時における検証事項が成り立たないための条件を算出する条件算出処理と、モジュール間の呼び出し関係における最上位のモジュールから検証対象のモジュールの開始時までの処理結果において、条件算出処理で算出した条件が成り立つか否かを判定する条件判定処理と、条件判定処理での判定に基づいて、検証対象のモジュールについて検証事項が成り立つか否かを判定し、条件判定処理で条件が成り立たないと判定した場合に、検証対象のモジュールについて検証事項が成り立つと判定するモジュール判定処理と、モジュール判定処理での判定に基づいて、ソフトウェアについて所定の検証事項が成り立つか否かを判定するソフトウェア判定処理とを実行させることを特徴とする。
【発明の効果】
【００１３】
本発明によれば、検証事項が成り立たない場合の前条件を求め、最上位モジュールからその前条件が成立するかどうか確認するため、分割して検証する際の前条件を作業者が設定することなく、容易にソフトウェアの検証を行うことができるという効果がある。また、最上位モジュールから再帰的に検証をおこない、検証事項が成り立たないと判定した場合にのみ、検証事項が成り立たないための条件を求めるため、不適切な条件設定を回避でき、正確にソフトウェアの検証を行うことができるいう効果がある。
【発明を実施するための最良の形態】
【００１４】
以下、本発明の実施の形態を図面を参照して説明する。図１は、本発明によるソフトウェア検証装置の構成例を示すブロック図である。図１に示すソフトウェア検証装置は、中央処理装置１１１と、出力装置１１２と、一次記憶装置１１３と、二次記憶装置１１４とを備える。
【００１５】
中央処理装置１１１は、二次記憶装置１１４が記憶する検証対象ソフトウェアのソースコードを読み取って検証処理を行い、検証結果を出力装置１１２に出力する。
【００１６】
出力装置１１２は、ディスプレイ装置や印刷装置等である。一次記憶装置１１３は、ソフトウェア検証装置が検証を行うための検証用プログラムや、中央処理装置１１１がプログラムを実行する上で一時的に必要とされるデータなどの各種データを記憶する。二次記憶装置１１４は、検証対象ソフトウェアのソースコードを記憶する。
【００１７】
以下に説明する検証機能は、図１に示された中央処理装置１１１の一部として実装される。また、ソフトウェア検証装置がコンピュータで実現される場合には、中央処理装置１１１が、以下に説明する検証機能を実現するためのプログラムを実行することによって実現される。
【００１８】
図２は、検証対象ソフトウェアのモジュール構造の例を示す説明図である。ｍ１〜ｍ７は、モジュールである。矢印はモジュール間の呼び出し関係を示す。また、ｐは、検証すべき性質（検証事項）を示す。検証すべき性質とは、図２に示す例では、モジュールｍ７のある箇所で守られるべき条件である。破線で囲まれた部分は、モジュールｍｉ（ｉ＝１，２，３，６）を起点とした検証範囲Ｍｉである。
【００１９】
図２を参照して、本実施の形態による検証方法を説明する。ソフトウェア全体で性質ｐが守られるか否かを検証するには、最初に最上位モジュールｍ１から検証を行う。検証を行ったモジュールにおいて、性質ｐが守られるか否かを判定できない場合には、ｐを含むモジュールｍ７を呼び出す可能性がある下位モジュールｍ２，ｍ３に対して、性質ｐが守られるか否かの判定結果が出るまで前条件なしで検証することにより、再帰的にモジュールｍ１の検証を行う。
【００２０】
下位モジュールのいずれかについて、性質ｐが守られないとの判定結果が出た場合には、当該下位モジュールでの検証開始時の前条件として、性質が守られないための条件を求める。そして、最上位モジュールから当該下位モジュールまで順に、前条件なしで性質ｐについて検証し、当該下位モジュールの検証開始時において、性質が守られないための条件が成り立つか否かを判定する。性質が守られないための条件が成り立つ場合、ソフトウェア全体でも性質が守られないとする。また、下位モジュールのすべてについて、性質ｐが守られるとの判定結果が出た場合には、ソフトウェア全体でも性質が守られるとする。
【００２１】
次に、図面を参照して本実施の形態の動作について説明する。図３は、本実施の形態における検証処理を示すフローチャートである。以下、中央処理装置１１１が性質ｐの検証処理を行う場合について説明する。
【００２２】
中央処理装置１１１は、まず、最上位モジュールを検証の起点モジュールｍｓとする（ステップＳ１）。中央処理装置１１１は、起点モジュールｍｓから、前条件無しで性質ｐが守られるか否かを検証する（ステップＳ２）。
【００２３】
ステップＳ３において、中央処理装置１１１は、性質ｐが守られるか否かを判定する。ステップＳ３において、性質ｐが守られるか否か判定不能の場合、中央処理装置１１１は、起点モジュールｍｓから直接呼び出されるモジュールのうち、ｐを含むモジュールを呼び出す可能性があるモジュール（ｐを含むモジュールそのものも含む）の集合Ｍｃを生成する（ステップＳ９）。中央処理装置１１１は、ステップＳ１０において、Ｍｃが空集合か否かを判定し、Ｍｃが空集合である場合は（ＹＥＳ）、ｍｓの検証結果Ｒｓを「判定不能」とする（ステップＳ１１）。Ｍｃが空集合でない場合は（ＮＯ）、集合Ｍｃに含まれる各モジュールを起点モジュールｍｓとして、ステップＳ２からの処理を再帰的に繰り返し（ステップＳ１２）、続く判定を行う。
【００２４】
中央処理装置１１１は、ステップＳ３において、起点モジュールｍｓで性質ｐが守られると判定した場合（ＹＥＳ）、ｍｓの検証結果Ｒｓを「性質ｐは守られる」とし（ステップＳ４）、ステップＳ１８に移行する。
【００２５】
中央処理装置１１１は、ステップＳ３において、性質ｐが守られないと判定した場合（ＮＯ）、起点モジュールｍｓでの検証開始時の条件Ｃｆとして、性質ｐが守られないための条件を求める（ステップＳ５）。
【００２６】
中央処理装置１１１は、モジュールｍｓから最上位モジュールまで呼び出し関係を逆向きに辿る経路上にあるモジュール群を検証範囲Ｍｕとする。中央処理装置１１１は、検証範囲Ｍｕにおいて、最上位モジュールを起点に、前条件なしで性質ｐについて検証し、ｍｓが呼び出される時点において、条件Ｃｆが成り立つか検証する（ステップＳ６）。すなわち、中央処理装置１１１は、モジュール間の呼び出し関係における最上位のモジュールから検証対象のモジュールの開始時までの処理結果において、条件Ｃｆが成り立つか否かを検証する。
【００２７】
ステップＳ７において、中央処理装置１１１は、ｍｓが呼び出される時点において条件Ｃｆが成り立つか否かを判定し、成り立つと判定した場合（ＹＥＳ）、ｍｓの検証結果Ｒｓを「性質ｐは守られない」とし（ステップＳ８）、ステップＳ１８に移行する。
【００２８】
ステップＳ７において、条件Ｃｆが成り立たないと判定した場合（ＮＯ）、中央処理装置１１１は、ｍｓの検証結果Ｒｓを「性質ｐは守られる」とし（ステップＳ４）、ステップＳ１８に移行する。判定不能の場合、中央処理装置１１１は、ｍｓの検証結果Ｒｓを「判定不能」とし（ステップＳ１１）、ステップＳ１８に移行する。ステップＳ１８において、ｍｓが最上位モジュールか否かを判定し、ｍｓが最上位モジュールでない場合は（ＮＯ）、ステップＳ１２に復帰する（ステップＳ１９）。
【００２９】
中央処理装置１１１は、集合Ｍｃの全てのモジュールについて検証結果を算出した場合、ステップＳ１３に移行する。ステップＳ１３において、中央処理装置１１１は、Ｍｃ中の全てのモジュールに対して性質ｐが守られるか否かを判定する。Ｍｃ中の全てのモジュールに対して性質ｐが守られると判定した場合（ＹＥＳ）、中央処理装置１１１は、ｍｓの検証結果Ｒｓを「性質ｐは守られる」とし（ステップＳ１４）、ステップＳ１８に移行する。
【００３０】
ステップＳ１３において、Ｍｃ中の全てのモジュールに対して性質ｐが守られるのではないと判定した場合（ＮＯ）、中央処理装置１１１は、ステップＳ１５において、Ｍｃ中に性質ｐが守られないモジュールがあるか否かを判定する。中央処理装置１１１は、Ｍｃ中に性質ｐが守られないモジュールがあると判定した場合は（ＹＥＳ）、ｍｓの検証結果Ｒｓを「性質ｐは守られない」とし（ステップＳ１６）、ステップＳ１８に移行する。そのいずれでもない場合、すなわち、Ｍｃ中に性質ｐが守られないモジュールがなく、いずれかのモジュールが判定不能の場合は（ＮＯ）、ｍｓの検証結果Ｒｓを「判定不能」とし（ステップＳ１７）、ステップＳ１８に移行する。
【００３１】
中央処理装置１１１は、ステップＳ１８において、ｍｓが最上位モジュールか否かを判定し、ｍｓが最上位モジュールでない場合は（ＮＯ）、ステップＳ１２に復帰する（ステップＳ１９）。一方、ｍｓが最上位モジュールの場合（ＹＥＳ）、ｍｓの検証結果Ｒｓをソフトウェア全体の性質ｐの検証結果Ｒとし（ステップＳ２０）、一連の処理を終了する。
【００３２】
また、中央処理装置１１１は、例えば、各モジュールの検証結果や、ソフトウェア全体の検証結果を、出力装置１１２に出力する。
【００３３】
次に、図２〜図９を参照して、本実施の形態の動作の具体例について説明する。以下、図２に示す検証対象ソフトウェアのモジュール構造を例にして説明する。図４は、検証対象ソフトウェアの処理内容の例を示す説明図である。図４には、処理内容をＣ言語風に記述し、かつ、図２に示す各モジュールが、図４に示す同名の関数に対応するとする。また、検証する性質ｐは、「モジュールｍ７におけるａ［ｉｄｘ］＝−１；の処理で、配列上限を超えたメモリアクセスをしないこと」とする。また、リソースの制約から、モジュールｍ１、ｍ２およびｍ３での性質ｐの検証はできない（判定不能になる）とする。
【００３４】
ｍ１を検証の起点モジュールｍｓとし（ステップＳ１）、起点モジュールｍｓから、前条件なしで性質ｐが守られるか検証する（ステップＳ２）。ステップＳ３において、検証結果は判定不能となるので、ｍｓ（＝ｍ１）から直接呼び出されるモジュールのうちｐを含むｍ７を呼び出す可能性があるモジュールの集合としてＭｃ＝｛ｍ２，ｍ３｝を生成する（ステップＳ９）。図５は、ｍｓ＝ｍ１の場合の検証範囲Ｍ１と、ｍ１から呼び出され、ｐを含むモジュールを呼び出すモジュールの集合Ｍｃ＝｛ｍ２，ｍ３｝との例を示す説明図である。ステップＳ１０において、Ｍｃは空集合でないので（ＮＯ）、Ｍｃの要素ｍ２、ｍ３に対し、ステップＳ２からの処理を再帰的に繰り返す（ステップＳ１２）。
【００３５】
ｍ２を起点モジュールｍｓとし（ステップＳ１）、起点モジュールｍｓから、前条件なしで性質ｐが守られるか検証する（ステップＳ２）。ステップＳ３において、検証結果は判定不能となるので、中央処理装置１１１は、集合Ｍｃを生成する（ステップＳ９）。ここで、ｍ２から直接呼び出されるモジュールのうちｍ７を呼び出す可能性があるｍ６のみが次のＭｃの要素となる。図６は、ｍｓ＝ｍ２の場合の検証範囲Ｍ２と、ｍ２から呼び出され、ｐを含むモジュールｍ７を呼び出すモジュールの集合Ｍｃ＝ｍ６との例を示す説明図である。ｍｓ＝ｍ６に対して、ステップＳ２からの処理が繰り返される。
【００３６】
ｍ６を起点として起点モジュールｍｓとし（ステップＳ１）、起点モジュールｍｓから、前条件なしで性質ｐが守られるか検証する（ステップＳ２）。ステップＳ３において、中央処理装置１１１は、性質ｐは必ずしも守られないと判断する（ＮＯ）。中央処理装置１１１は、ｍｓ（＝ｍ６）の検証開始時における、性質ｐが守られないための条件Ｃｆをｉｄｘ≧２と算出する（ステップＳ５）。図７は、ｍｓ＝ｍ６の場合の検証範囲Ｍ６と、最上位モジュールから条件Ｃｆを検証する検証範囲Ｍｕ＝｛ｍ１，ｍ２｝との例を示す説明図である。
【００３７】
中央処理装置１１１は、条件Ｃｆが成り立つかどうかを、最上位モジュールｍ１からＭｕ＝｛ｍ１，ｍ２｝を検証範囲として、前条件無しで検証する（ステップＳ６）。ｍ６が呼び出される時点では、ｉｄｘ＝１となり、Ｃｆが成立たないので（ステップＳ７におけるＮＯ）、ｍｓ（＝ｍ６）の検証結果Ｒｓは「性質ｐは守られる」となる（ステップＳ４）。
【００３８】
この時点でのｍｓ（＝ｍ６）は最上位モジュールｍ１ではないので、ステップＳ２に移行する（ステップＳ１９）。集合Ｍｃ＝ｍ６について検証結果を算出したため、ステップＳ１３に移行し、ｍ２の下位モジュール群Ｍｃの検証結果からｍ２の検証結果を求める。ここで、Ｍｃに含まれるモジュールはｍ６のみであり、かつｍ６の検証結果は「性質ｐは守られる」である。したがって、ｍ２の全下位モジュールの検証結果は「性質ｐは守られる」となり（ステップＳ１３におけるＹＥＳ）、ｍｓ（＝ｍ２）の検証結果Ｒｓは「性質ｐは守られる」となる（ステップＳ１４）。ステップＳ１８において、ｍｓ（＝ｍ２）は最上位モジュールｍ１ではないので、ステップＳ１２に移行する（ステップＳ１９）。
【００３９】
次に、ｍ３を起点モジュールｍｓとし（ステップＳ１）、起点モジュールｍｓから、前条件なしで性質ｐが守られるか検証する（ステップＳ２）。ステップＳ３において、ｍ３の検証結果も判定不能となるので、中央処理装置１１１は、集合Ｍｃを生成する（ステップＳ９）。ステップＳ９において、中央処理装置１１１は、ｍ３から直接呼び出されるモジュールｍ７のみを要素とするＭｃを生成する。図８は、ｍｓ＝ｍ３の場合の検証範囲Ｍ３と、ｍ３から呼び出され、ｐを含むモジュールの集合Ｍｃ＝ｍ７との例を示す説明図である。ｍｓ＝ｍ７に対して、ステップＳ２からの処理が繰り返される。
【００４０】
ｍ７を起点モジュールｍｓとし（ステップＳ１）、前条件なしで性質ｐが守られるか検証する（ステップＳ２）。ステップＳ３において、中央処理装置１１１は、性質ｐは必ずしも守られないと判断する（ＮＯ）。中央処理装置１１１は、ｍｓ（＝ｍ７）の検証開始時における、性質ｐが守られないための条件Ｃｆをｉｄｘ≧４と算出する（ステップＳ５）。
【００４１】
図９は、ｍｓ＝ｍ７の場合の検証範囲Ｍ７と、最上位モジュールから条件Ｃｆを検証する検証範囲Ｍｕ＝｛ｍ１，ｍ３｝との例を示す説明図である。
【００４２】
中央処理装置１１１は、条件Ｃｆが成り立つかどうかを、最上位モジュールｍ１からＭｕ＝｛ｍ１，ｍ３｝を検証範囲として、前条件なしで検証する（ステップＳ６）。ｍ７が呼び出される時点では、ｉｄｘ＝４となり、Ｃｆが成立つので（ステップＳ７におけるＹＥＳ）、ｍｓ（＝ｍ７）の検証結果Ｒｓは「性質ｐは守られない」となる（ステップＳ８）。
【００４３】
この時点でのｍｓ（＝ｍ７）は最上位モジュールｍ１ではないので、ステップＳ２に移行する（ステップＳ１９）。集合Ｍｃ＝ｍ７について検証結果を算出したため、ステップＳ１３に移行し、ｍ３の下位モジュール群Ｍｃの検証結果からｍ３の検証結果を求める。ここで、Ｍｃに、「性質ｐが守られない」要素ｍ７があるので（ステップＳ１５におけるＹＥＳ）、ｍｓ（＝ｍ３）の検証結果Ｒｓは「性質ｐが守られない」となる（ステップＳ１６）。ステップＳ１８において、ｍｓ（＝ｍ３）は最上位モジュールｍ１ではないので、ステップＳ１２に移行する（ステップＳ１９）。
【００４４】
ｍｓ（＝ｍ１）の下位モジュール群Ｍｃ＝｛ｍ２，ｍ３｝の全ての検証結果を算出したため、ステップＳ１３に移行し、ｍ１の下位モジュール群Ｍｃ＝｛ｍ２，ｍ３｝の検証結果からｍ１の検証結果を求める。
【００４５】
Ｍｃに「性質ｐが守られない」要素ｍ３があるので（ステップＳ１５におけるＹＥＳ）、ｍｓ（＝ｍ１）の検証結果Ｒｓは「性質ｐが守られない」となる（ステップＳ１６）。ｍｓ（＝ｍ１）は最上位モジュールｍ１なので、ｍｓ（＝ｍ１）の検証結果Ｒｓをソフトウェア全体の性質ｐの検証結果Ｒとして、「性質ｐは守られない」とし（ステップＳ２０）、一連の処理を終了する。
【００４６】
以上に説明したように、本実施の形態によれば、部分検証して性質ｐが守られない場合の前条件を求め、最上位モジュールからその前条件が成立するかどうか確認する。そのため、呼び出し関係があるモジュール間で満たすべき条件の設定作業を省略することができ、分割して検証する際の前条件を作業者が設定する場合に比べて、容易にソフトウェアの検証を行うことができる。
【００４７】
また、最上位モジュールから再帰的に検証をおこない、検証結果が得られた場合にのみ、その結果に基づいて条件を求めるため、不適切な条件設定を回避することができ、正確にソフトウェアの検証を行うことができる。
【００４８】
さらに、ソフトウェアを構成するモジュールの呼び出し関係に基づいて、検証の起点を呼び出し関係の上位モジュールから下位モジュールに変えながら、最上位モジュールから再帰的に検証を行い、判定不能の場合にのみ再帰的にモジュールを下降して検証を行う。すなわち、検証対象モジュールの検証結果が判定不能になった場合に下位モジュールの検証を行い、下位モジュールの検証結果から上位モジュールの検証結果を求める処理を再帰的に繰り返す。したがって、特定の性質について検証するために大規模ソフトウェアを適切に分割でき、検証作業者が人手で行っていた部分検証範囲の特定作業を省略することができるため、正確かつ効率的に検証を行うことができる。
【００４９】
例えば、検証対象モジュールの検証結果が判定不能になった場合にのみ、モジュールを下降して検証（すなわち、部分的な検証）を行うことから、大きなコンテキストでの検証が可能となり、小さなコンテキストでの検証を積み重ねる（その度に誤差が入る可能性がある）場合に比べて正確に検証を行うことができる。また、必要な部分だけ分割して検証することから、分割によるオーバヘッドが少なくて済むため、効率的に検証を行うことができる。
【００５０】
なお、上記の実施の形態では、中央処理装置１１１が、各モジュールの検証結果やソフトウェア全体の検証結果を、出力装置１１２に出力する場合を例にしたが、出力装置１１２はなくてもよい。その場合、中央処理装置１１１は、例えば、最終的な処理結果を二次記憶装置１１４に出力してもよい。
【産業上の利用可能性】
【００５１】
本発明は、呼び出し関係がある複数のモジュールを含むソフトウェアを検証する場合に効果的に適用できる。
【図面の簡単な説明】
【００５２】
【図１】本発明によるソフトウェア検証装置の構成例を示すブロック図である。
【図２】検証対象ソフトウェアのモジュール構造の例を示す説明図である。
【図３】検証処理を示すフローチャートである。
【図４】検証対象ソフトウェアの処理内容の例を示す説明図である。
【図５】検証範囲およびモジュールの集合Ｍｃの例を示す説明図である。
【図６】検証範囲およびモジュールの集合Ｍｃの例を示す説明図である。
【図７】検証範囲および検証範囲Ｍｕの例を示す説明図である。
【図８】検証範囲およびモジュールの集合Ｍｃの例を示す説明図である。
【図９】検証範囲および検証範囲Ｍｕの例を示す説明図である。
【符号の説明】
【００５３】
１１１  中央処理装置
１１２  出力装置
１１３  一次記憶装置
１１４  二次記憶装置
【図１】
2008203977.tif 000003
【図２】
2008203977.tif 000004
【図３】
2008203977.tif 000005
【図４】
2008203977.tif 000006
【図５】
2008203977.tif 000007
【図６】
2008203977.tif 000008
【図７】
2008203977.tif 000009
【図８】
2008203977.tif 000010
【図９】
2008203977.tif 000011