(57)【要約】  ソフトウェアモデル検査を行う際に、実行状態の復元および保存をより高速に行う技術を提供すること。  検査対象ソフトウェアの実行状態を表すメモリ１３内のオブジェクトを所定の整列順序で抽出して保存領域にコピーしていくことにより、実行状態を表す情報として保存する状態保存部１１と、保存領域に格納された実行状態を表す情報に含まれるオブジェクトを、格納されている順序でメモリ１３内の復元領域にコピーしていくことにより、実行状態を復元する状態復元部１２と、を備える。
2015087509.tif 000002
【特許請求の範囲】
【請求項１】
検査対象ソフトウェアの実行状態を表すメモリ内のオブジェクトを所定の整列順序で抽出して保存領域にコピーしていくことにより、前記実行状態を表す情報として保存する状態保存手段と、
前記保存領域に格納された前記実行状態を表す情報に含まれる前記オブジェクトを、格納されている順序で前記メモリ内の復元領域にコピーしていくことにより、前記実行状態を復元する状態復元手段と、
を備えた状態保存復元装置。
【請求項２】
前記状態保存手段は、前回の実行状態を表す情報が格納されている保存領域がある場合、前記状態復元手段により前記復元領域に復元された前回の実行状態から前記検査対象ソフトウェアの一部が実行された後の実行状態において、該実行状態を表す前記メモリ内のオブジェクトと、前記前回の実行状態を表す情報に含まれるオブジェクトとを、格納されている順序で比較していき、先頭のオブジェクトから変更のないオブジェクトまでは、前記前回の実行状態を表す情報に含まれるオブジェクトを今回の実行状態の保存領域にコピーすることを特徴とする請求項１に記載の状態保存復元装置。
【請求項３】
前記状態保存手段は、前記メモリ内のオブジェクトを前記整列順序で前記保存領域にコピーする際に、各オブジェクトに関するメタ情報を前記オブジェクトと共に前記保存領域に格納するとともに、前記前回の実行状態を表す情報が格納された保存領域がある場合、前記先頭のオブジェクトから前記変更のないオブジェクトまでは、前記前回の実行状態を表す情報に含まれるオブジェクトおよびこれらに関連付けられる前記メタ情報を今回の実行状態の保存領域にコピーすることを特徴とする請求項２に記載の状態保存復元装置。
【請求項４】
前記実行状態を表す情報に対するハッシュ値が前記実行状態の既達管理に用いられるとき、
前記状態保存手段は、前記メタ情報として、前記先頭のオブジェクトから各オブジェクトまでの情報に対するハッシュ値を算出して前記保存領域に格納し、前記前回の実行状態を表す情報が格納された保存領域がある場合、前記先頭のオブジェクトから前記変更のないオブジェクトまでは、前記前回の実行状態を表す情報に含まれるオブジェクトおよびこれらに関連付けられる前記ハッシュ値を、今回の実行状態の保存領域にコピーすることにより、前記変更のないオブジェクトまでの各ハッシュ値の算出を省略することを特徴とする請求項３に記載の状態保存復元装置。
【請求項５】
前記状態保存手段は、前記メモリ内のオブジェクトを前記整列順序で前記保存領域にコピーする際に、前記オブジェクト内の参照情報を、基底アドレスからのオフセット値で置き換えてコピーし、
前記状態復元手段は、前記保存領域に格納された前記実行状態を表す情報に含まれる前記オブジェクトを格納されている順序で前記復元領域にコピーする際に、前記オブジェクト内の参照情報としてのオフセット値を、前記復元領域の先頭アドレスを足した値に置き換えてコピーすることを特徴とする請求項１から請求項４のいずれか１項に記載の状態保存復元装置。
【請求項６】
前記状態保存手段は、前記整列順序として、前記オブジェクト間の参照関係に基づく幅優先探索順序を適用することを特徴とする請求項１から請求項５のいずれか１つに記載の状態保存復元装置。
【請求項７】
検査対象ソフトウェアの実行状態を表すメモリ内のオブジェクトを所定の整列順序で抽出して保存領域にコピーしていくことにより、前記実行状態を表す情報として保存し、
前記保存領域に格納された前記実行状態を表す情報に含まれる前記オブジェクトを、格納されている順序で前記メモリ内の復元領域にコピーしていくことにより、前記実行状態を復元する、状態保存復元方法。
【請求項８】
検査対象ソフトウェアの実行状態を表すメモリ内のオブジェクトを所定の整列順序で抽出して保存領域にコピーしていくことにより、前記実行状態を表す情報として保存する状態保存ステップと、
前記保存領域に格納された前記実行状態を表す情報に含まれる前記オブジェクトを、格納されている順序で前記メモリ内の復元領域にコピーしていくことにより、前記実行状態を復元する状態復元ステップと、
をコンピュータ装置に実行させるコンピュータ・プログラムを格納した記憶媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェアモデル検査においてソフトウェアの実行状態を保存および復元する技術に関する。
【背景技術】
【０００２】
ソフトウェアを直接実行する形態によってソフトウェアモデル検査を行う技術が知られている。ソフトウェアモデル検査は、検査対象であるソフトウェアプログラム自身を、状態遷移系とみなしたモデルを用いて検査する手法である。このようなソフトウェアモデル検査では、専用のモデル記述言語で作成された検証専用のモデルを用いることなく、ソフトウェアの一部を直接実行し、その実行の前後におけるメモリの状態が保存される。そして、このソフトウェアモデル検査における、ある状態から複数の状態遷移が可能な場合には、必要に応じてメモリの状態を復元し、再度別の状態遷移を行うような網羅的な実行を行う。これにより、このソフトウェアモデル検査は、テスト等では発見しにくいタイミングに依存するバグを見つけやすくする。一方で、このようなソフトウェアを直接実行するソフトウェアモデル検査では、ソフトウェアの一部を実行する前後におけるメモリの状態の保存および復元を、状態遷移数に比例した回数だけ行う必要がある。【０００３】
このようなソフトウェアモデル検査を行う関連技術が非特許文献１に記載されている。非特許文献１に記載されたソフトウェアモデル検査システム９００は、図１３に示すように構成される。
図１３において、ソフトウェアモデル検査システム９００は、以下の構成を備える。
ユーザ定義コード保存部９０１、
プログラム実行部９０２、
メモリ管理部９０３、
メモリ９０４、
初期状態生成部９０５、
状態保存復元部９０６、
要探索状態管理部９０７、
遷移生成部９０８、
遷移実行部９０９、
既達状態管理部９１０、
性質検証部９１１、
判定部９１２。【０００４】
ユーザ定義コード保存部９０１には、検査対象となるソフトウェアのユーザ定義コードが保存される。【０００５】
プログラム実行部９０２は、ユーザ定義コードを実行し、実行の際に用いる情報を、メモリ管理部９０３を用いてメモリ９０４内に記憶する。なお、以降では、メモリ９０４内においてプログラム実行部９０２によって用いられるこれらの情報の状態を、ソフトウェアのその時点での「実行状態を表す情報」と呼ぶものとする。【０００６】
メモリ管理部９０３は、プログラム実行部９０２からの要求に応じて、メモリ９０４内に必要な領域を確保するとともに、その利用状況を管理し、利用されていない領域を解放して再度利用可能にする。【０００７】
メモリ９０４は、プログラム実行部９０２の実行時に必要となる情報を記憶する。【０００８】
初期状態生成部９０５は、ユーザ定義コードがプログラム実行部９０２によって実行される際に用いられる情報の初期の状態（初期状態）をメモリ９０４内に作成（用意）する。また、初期状態生成部９０５は、この初期状態を、後述の状態保存復元部９０６を用いて保存し、後述の探索キューに入れる。【０００９】
状態保存復元部９０６は、メモリ９０４内の実行状態を表す情報を、所定のフォーマットに変換して保存する。保存場所は、メモリ９０４内に確保された領域である。また、状態保存復元部９０６は、保存した実行状態を表す情報を変換し、メモリ９０４内に復元する。【００１０】
要探索状態管理部９０７は、探索が必要な実行状態を探索順で保持する探索キューを管理する。探索キューは、実行状態を表す情報の保存領域の先頭アドレスのキューであってもよい。【００１１】
遷移生成部９０８は、探索キューから取り出された実行状態から可能な遷移を生成する。具体的には、遷移生成部９０８は、その実行状態から次に実行可能なプロセス・スレッド等のプログラム断片を特定する。【００１２】
遷移実行部９０９は、メモリ９０４の状態を、探索キューから取り出された実行状態に復元した後で、その実行状態から可能な遷移を、プログラム実行部９０２に実行させる。なお、可能な遷移は、遷移生成部９０８によって生成された状態である。【００１３】
既達状態管理部９１０は、遷移実行部９０９によって遷移済み（既達）の実行状態を識別可能なハッシュ値を、既達状態として記録する。既達状態管理部９１０は、遷移実行部９０９による遷移後の実行状態が既達であるかどうかを、その実行状態のハッシュ値が既に記録されているか否かにより判断する。【００１４】
性質検証部９１１は、遷移実行部９０９による遷移後の実行状態が既達状態でなければ、その実行状態が所定の性質を満たすかどうかを検査する。そして、性質検証部９１１は、所定の性質を満たした実行状態を表す情報を、探索キューに入れる。【００１５】
判定部９１２は、遷移実行部９０９による遷移後の実行状態が所定の性質を満たさない場合、エラーとして報告する。また、判定部９１２は、遷移生成部９０８によって現在の実行状態から可能な遷移を見つけられない場合、デッドロック・エラーが発生したと判定する。【００１６】
このように構成された関連技術であるソフトウェアモデル検査システム９００は、次のように動作する。【００１７】
まず、初期状態生成部９０５は、検査対象のソフトウェアの初期状態に相当するメモリ領域を作成し、初期状態を表す情報を探索キューに入れる。【００１８】
次に、遷移生成部９０８は、探索キューから実行状態を１つ取り出し、「現在の実行状態」とする。そして、遷移生成部９０８は、「現在の実行状態」から可能な遷移（プロセス・スレッド等のプログラム断片）を生成する。【００１９】
次に、状態保存復元部９０６は、メモリ９０４内の実行状態を「現在の実行状態」に戻す。【００２０】
次に、遷移実行部９０９は、該当するプログラム断片をプログラム実行部９０２に実行させる。【００２１】
次に、状態保存復元部９０６は、遷移後の実行状態を保存する。【００２２】
次に、既達状態管理部９１０は、遷移後の実行状態が既達であるか否かを判断する。既達であれば、ソフトウェアモデル検査システム９００は、「現在の実行状態」から可能な他の遷移について、上述した、状態保存復元部９０６がメモリ９０４内の実行状態を「現在の実行状態」に戻す処理から上記までの処理を繰り返す。【００２３】
遷移後の実行状態が既達でなく、遷移後の実行状態が所定の性質を満たさない場合、性質検証部９１１は、エラーを出力する。【００２４】
遷移後の実行状態が既達でなく、所定の性質を満たす場合、性質検証部９１１は、遷移後の実行状態を探索キューに入れる。また、既達状態管理部９１０は、この実行状態を既達としてハッシュ値を記録する。【００２５】
そして、ソフトウェアモデル検査システム９００は、現在の実行状態から可能な他の遷移について、上述した、状態保存復元部９０６がメモリ９０４内の実行状態を「現在の実行状態」に戻す処理からこれまでの処理を繰り返す。【００２６】
現在の実行状態から可能な全ての遷移について上記の処理を行うと、ソフトウェアモデル検査システム９００は、次の「現在の実行状態」を探索キューから取り出す。その後、上述した、遷移生成部９０８が「現在の実行状態」から可能な遷移を生成する処理からこれまでの処理を繰り返す。【００２７】
なお、現在の実行状態から可能な遷移が存在しない場合、判定部９１２は、デッドロック・エラーを出力する。【００２８】
以上の全処理を、ソフトウェアモデル検査システム９００は、探索キューが空になるまで繰り返す。【００２９】
このように、非特許文献１に記載されたようなソフトウェアを直接実行するソフトウェアモデル検査システムは、テストデータに対するソフトウェアの実行（テスト実行）を行うのではなく、ソフトウェアにおいて可能な状態遷移を全て探索する。ここで、テスト実行は、ソフトウェアに対してテストデータが与えられ、あるデータに対して想定した動作をするか否か、あるいは、想定しない動作をしないか否かをテストする処理である。これに対して、ソフトウェアを直接実行するソフトウェアモデル検査システムは、可能な状態遷移を全て探索することにより、不具合が発生する状態を網羅的に探索することができる。
【先行技術文献】
【非特許文献】
【００３０】
【非特許文献１】Madanlal Musuvathi, “CMC: a MODEL CHECKER FOR NETWORK PROTOCOL IMPLEMENTATIONS”, Technical Report PhD Thesis, Stanford University, January 2004．
【発明の概要】
【発明が解決しようとする課題】
【００３１】
しかしながら、非特許文献１に記載された関連技術には、ソフトウェアモデル検査を行うための実行状態の復元および保存に時間がかかるという課題がある。このため、関連技術では、実行状態を保存する際に状態が保存された部分だけを保存するために、ＯＳ（Operating System）のメモリ保護機能を用いる。したがって、この関連技術を、より一般的な環境（例えば、メモリ保護機能のない環境や、インタプリタ等メモリ保護機能を自由に利用できない環境）で適用するのは難しい。そのため、通常は、実行状態のシリアライズ・デシリアライズ処理として可搬的なフォーマットとの相互変換が行われる。このため、実行状態を保存する際には、メモリ内のオブジェクトの走査によるコストが大きくなる。また、保存した実行状態をメモリ内に復元する際には、オブジェクトの走査および再生成のコストが大きくなる。【００３２】
本発明は、上述の課題を解決するためになされた。本発明は、ソフトウェアモデル検査を行う際に、実行状態の復元および保存をより高速に行う技術を提供することを主たる目的とする。
【課題を解決するための手段】
【００３３】
本発明の状態保存復元装置は、検査対象ソフトウェアの実行状態を表すメモリ内のオブジェクトを所定の整列順序で抽出して保存領域にコピーしていくことにより、前記実行状態を表す情報として保存する状態保存手段と、前記保存領域に格納された前記実行状態を表す情報に含まれる前記オブジェクトを、格納されている順序で前記メモリ内の復元領域にコピーしていくことにより、前記実行状態を復元する状態復元手段と、を備える。【００３４】
また、本発明の状態保存復元方法は、検査対象ソフトウェアの実行状態を表すメモリ内のオブジェクトを所定の整列順序で抽出して保存領域にコピーしていくことにより、前記実行状態を表す情報として保存し、前記保存領域に格納された前記実行状態を表す情報に含まれる前記オブジェクトを、格納されている順序で前記メモリ内の復元領域にコピーしていくことにより、前記実行状態を復元する。【００３５】
また、本発明のコンピュータ・プログラムおよびそれを格納した記憶媒体は、検査対象ソフトウェアの実行状態を表すメモリ内のオブジェクトを所定の整列順序で抽出して保存領域にコピーしていくことにより、前記実行状態を表す情報として保存する状態保存ステップと、前記保存領域に格納された前記実行状態を表す情報に含まれる前記オブジェクトを、格納されている順序で前記メモリ内の復元領域にコピーしていくことにより、前記実行状態を復元する状態復元ステップと、をコンピュータ装置に実行させる。
【発明の効果】
【００３６】
本発明は、ソフトウェアモデル検査を行う際に、実行状態の復元および保存をより高速に行う技術を提供することができる。
【図面の簡単な説明】
【００３７】
【図１】本発明の第1の実施の形態としての状態保存復元装置の機能ブロック図である。
【図２】本発明の第1の実施の形態としての状態保存復元装置のハードウェア構成図である。
【図３】本発明の第1の実施の形態としての状態保存復元装置の状態保存動作を説明するフローチャートである。
【図４】本発明の第1の実施の形態としての状態保存復元装置の状態復元動作を説明するフローチャートである。
【図５】本発明の第２の実施の形態としての状態保存復元装置の機能ブロック図である。
【図６】本発明の第２の実施の形態において保存される実行状態を表す情報の構成の一例を示す図である。
【図７】本発明の第２の実施の形態としての状態保存復元装置の状態保存動作を説明するフローチャートである。
【図８】本発明の第２の実施の形態としての状態保存復元装置の状態復元動作を説明するフローチャートである。
【図９】本発明の第２の実施の形態に検査対象ソフトウェアの初期状態で用いられるオブジェクトの参照グラフの一例を示す図である。
【図１０】本発明の第２の実施の形態において、保存された初期状態を表す情報の一例を示す図である。
【図１１】本発明の第２の実施の形態において、保存された前回の実行状態がある場合に、現在の実行状態を表す情報を保存する動作を模式的に説明する図である。
【図１２】本発明の第２の実施の形態において、保存された前回の実行状態を復元する動作を模式的に説明する図である。
【図１３】関連技術のソフトウェアモデル検査システムの構成を示すブロック図である。
【発明を実施するための形態】
【００３８】
以下、本発明の実施の形態について、図面を参照して詳細に説明する。
【００３９】
（第１の実施の形態）
本発明の第１の実施の形態としての状態保存復元装置１の機能ブロック構成を図１に示す。図１において、状態保存復元装置１は、状態保存部１１と、状態復元部１２と、メモリ１３とを備える。なお、状態保存復元装置１は、ソフトウェアを直接実行することにより実行状態の遷移を探索するソフトウェアモデル検査システムに備えられる。例えば、状態保存復元装置１は、図１３に示したような関連技術のソフトウェアモデル検査システム９００において状態保存復元部９０６の代わりに備えられてもよい。
【００４０】
ここで、状態保存復元装置１は、図２に示すように、ＣＰＵ（Central Processing Unit）１００１と、ＲＡＭ（Random Access Memory）１００２と、ＲＯＭ（Read Only Memory）１００３と、ハードディスク等の記憶装置１００４とを備えたコンピュータ装置によって構成可能である。なお、状態保存復元装置１は、自装置を備えるソフトウェアモデル検査システムを構成するコンピュータ装置によって構成されていてもよい。この場合、メモリ１３は、ＲＡＭ１００２および記憶装置１００４によって構成される。また、状態保存部１１および状態復元部１２は、ＲＯＭ１００３および記憶装置１００４に記憶されたコンピュータ・プログラムおよび各種データをＲＡＭ１００２に読み込んで実行するＣＰＵ１００１によって構成される。なお、状態保存復元装置１およびその各機能ブロックのハードウェア構成は、上述の構成に限定されない。
【００４１】
メモリ１３には、ソフトウェアモデル検査の対象となるソフトウェア（検査対象ソフトウェア）によって実行中に用いられるオブジェクトが保持される領域を備える。本実施の形態では、検査対象ソフトウェアによって用いられる、メモリ１３内に格納されるオブジェクトを、検査対象ソフトウェアのその時点での実行状態を表しているとみなす。メモリ１３におけるこれらのオブジェクトは、検査対象ソフトウェアの少なくとも一部の実行により、適宜更新される。
【００４２】
なお、メモリ１３は、検査対象ソフトウェアによって用いられるオブジェクトに加えて、後述の状態保存部１１によって保存される実行状態を表す情報を保持してもよい。ただし、以下に説明する本発明の各実施の形態では、単に「メモリ１３内のオブジェクト」と記載した場合は、検査対象ソフトウェアのある実行状態においてメモリ１３内で用いられているオブジェクトを指すものとする。
【００４３】
状態保存部１１は、検査対象ソフトウェアの現在の実行状態を表すメモリ１３内のオブジェクトを、所定の整列順序で抽出して保存領域（不図示）にコピーしていくことにより、実行状態を表す情報として保存する。前述のように、保存領域は、メモリ１３内に確保されてもよい。
【００４４】
状態復元部１２は、保存領域に格納されている実行状態を表す情報を、格納されている順序でメモリ１３内の復元領域（不図示）にコピーしていくことにより、実行状態を復元する。このような復元領域は、検査対象ソフトウェアによって次の実行状態に遷移するために用いられる。
【００４５】
以上のように構成された状態保存復元装置１の動作について、図面を参照して説明する。
【００４６】
まず、状態保存復元装置１の状態保存動作を図３に示す。
【００４７】
図３では、まず、状態保存部１１は、現在の実行状態を保存するための連続した保存領域をメモリ１３内に確保する（ステップＳ１）。
【００４８】
次に、状態保存部１１は、検査対象ソフトウェアの現在の実行状態においてメモリ１３内で用いられているオブジェクトを、所定の整列順序で走査しながら抽出し、保存領域にコピーする（ステップＳ２）。
【００４９】
以上で、状態保存復元装置１は、状態保存動作を終了する。
【００５０】
次に、状態保存復元装置１の状態復元動作を図４に示す。
【００５１】
図４では、まず、状態復元部１２は、メモリ１３内に、実行状態を復元するための連続した復元領域を確保する（ステップＳ１１）。
【００５２】
次に、状態復元部１２は、保存領域に格納されている実行状態を表す情報に含まれるオブジェクトを、格納されている順序で復元領域に順次コピーする（ステップＳ１２）。
【００５３】
以上で、状態保存復元装置１は、状態復元動作を終了する。
【００５４】
次に、本発明の第１の実施の形態の効果について述べる。
【００５５】
本発明の第１の実施の形態としての状態保存復元装置１は、ソフトウェアモデル検査を行う際に、実行状態の復元および保存をより高速に行うことができる。
【００５６】
その理由は、状態保存部が、検査対象ソフトウェアの実行状態を表すメモリ内のオブジェクトを所定の整列順序で保存領域にコピーすることにより、実行状態を保存するからである。また、状態復元部が、保存された実行状態を表す情報を、格納されている順序で復元領域にコピーすることにより、実行状態を復元するからである。
【００５７】
本実施形態に係る状態保存復元装置１は、復元された実行状態から遷移した後の実行状態を保存する際に次のように処理を行う。即ち、状態保存復元装置１は、オブジェクトに変更の無い部分に関しては、おおむね所定の整列順序でメモリ内に並んだオブジェクトを、保存領域に順次この並びでコピーすることにより保存を行う。また、本実施形態に係る状態保存復元装置１は、保存領域に連続して保持されたオブジェクトをその順序で復元領域に復元する。したがって、本実施の形態によれば、実行状態の保存および復元におけるオブジェクトのコピーを、おおむねメモリ内に格納されているオブジェクトの並び順に従って行うことができる。従って、本実施形態に係る状態保存復元装置１は、可搬的なフォーマットとの間での変換により保存および復元を行う場合と比べて、より高速である。さらには、本実施形態に係る状態保存復元装置１は、状態の保存および復元を、メモリ内の並び順で極力行うことにより、メモリに対するランダムアクセスによる性能低下を小さくすることもできる。
【００５８】
（第２の実施の形態）
次に、本発明の第２の実施の形態について図面を参照して詳細に説明する。本実施の形態では、状態保存復元装置（２）が、実行状態の既達管理をハッシュ値によって行うソフトウェアモデル検査システムに備えられる例について説明する。
【００５９】
ここで、関連技術に示したようなソフトウェアモデル検査システムでは、状態数が大規模、あるいは、実質無限となる。そこで、既達状態の管理にハッシュ値を用いる手法が広く使われる。一般に、ハッシュ値の衝突の確率は小さいという傾向がある。そこでこの傾向を無視すれば、既に探索した状態かどうかは、その状態を表すメモリ内容のハッシュ値を求めてこの値のみを記録しておき、探索した状態のハッシュ値が既に記録されているか否かにより判定可能である。このような手法は、既達状態を管理するために各状態のメモリ内容を丸ごと保存するのと比較して、大幅にメモリを節約でき、ビットステートハッシングや、ハッシュコンパクトなどと呼ばれて広く知られている。一方で、この手法では、ハッシュ値を計算するために、状態を構成するメモリ内の全てのオブジェクトを走査する必要が生じる。また、この手法では、メモリ内でのオブジェクトの具体的な配置位置に影響されることなく、そのハッシュ値を計算する必要が生じる。本実施の形態では、状態保存復元装置（２）が、ハッシュ値の計算コストを削減することにより、実行状態の保存および復元をさらに高速に行う例について詳細に説明する。なお、本実施の形態の説明において参照する各図面において、本発明の第１の実施の形態と同一の構成および同様に動作するステップには同一の符号を付して本実施の形態における詳細な説明を省略する。
【００６０】
本発明の第２の実施の形態に係る状態保存復元装置２の構成を図５に示す。図５において、状態保存復元装置２は、本発明の第１の実施の形態としての状態保存復元装置１に対して、状態保存部１１に替えて状態保存部２１と、状態復元部１２に替えて状態復元部２２とを備える点が異なる。状態保存復元装置２は、上述のように、検査対象ソフトウェアを直接実行して実行状態の遷移を探索する際に、実行状態の既達管理をハッシュ値により行うソフトウェアモデル検査システムに備えられることとする。例えば、状態保存復元装置２は、図１３に示したような関連技術のソフトウェアモデル検査システム９００において状態保存復元部９０６の代わりに備えられる構成であってもよい。
【００６１】
状態保存復元装置２および各機能ブロックは、図２を参照して説明した本発明の第１の実施の形態としての状態保存復元装置１と同一のハードウェア要素によって構成可能である。なお、状態保存復元装置２および各機能ブロックのハードウェア構成は、上述の構成に限定されない。
【００６２】
状態保存部２１は、検査対象ソフトウェアの現在の実行状態を表すメモリ１３内に格納される各オブジェクトを、当該格納されていた整列順序に従い、抽出すると共に、メモリ１３内部の保存領域にコピーする。この処理は、本発明の第１の実施の形態における状態保存部１１と同様である。さらに本実施の形態では、状態保存部２１は、オブジェクトを整列順序で抽出してコピーする際に、各オブジェクトに関するメタ情報を、オブジェクトと共に保存領域に保存する。本実施の形態では、メタ情報には、先頭のオブジェクトから各オブジェクトまでの情報に対するハッシュ値と、検索開始ノードからの深さを表す情報（詳細は後述する）とが含まれる。なお、保存領域において、先頭のオブジェクトから最後のオブジェクトまでのオブジェクト列は、連続した領域に保持される。また、保存領域において、メタ情報は、オブジェクト列の連続した領域とは異なる領域に保持される。
【００６３】
状態保存部２１は、メモリ１３内のオブジェクトを整列順序で保存領域にコピーする際に、オブジェクト内の参照情報を、基底アドレスからのオフセット値によって置き換えてコピーする。
【００６４】
状態保存部２１は、前回の実行状態を表す情報が格納された保存領域がある場合、前回の実行状態を表す情報に含まれるオブジェクトを、格納されている順序で走査しながら、現在の実行状態におけるメモリ１３内のオブジェクトと比較していく。ここで、現在の実行状態におけるメモリ１３内のオブジェクトは、後述の状態復元部２２によって復元された前回の実行状態から、検査対象ソフトウェアの一部（例えば、プログラム一単位分）が実行された後の状態である。したがって、前回の実行状態を表す情報に含まれるオブジェクトと、現在の実行状態におけるメモリ１３内のオブジェクトとは、先頭のオブジェクトから変更のないオブジェクトまでは、同じ順序で並んでいる。そこで、状態保存部２１は、先頭のオブジェクトから変更のないオブジェクトまでは、前回の実行状態における各オブジェクトおよびそのメタ情報であるハッシュ値および深さを表す情報を、今回の実行状態のための保存領域にコピーする。このように、状態保存部２１は、先頭のオブジェクトから変更のないオブジェクトまでは、ハッシュ値の算出を省略する。
【００６５】
ここで、本実施の形態では、整列順序として、オブジェクトの参照関係に基づく幅優先探索順序を適用することを想定する。幅優先検索とは、グラフ理論において木構造やグラフの探索に用いられる手法で、検索アルゴリズムは根ノードで始まり隣接した全てのノードを探索する。メタ情報に含まれる前述の深さ情報は、該当するオブジェクトの幅優先探索順序におけるルートオブジェクト（根ノード）からの深さを示す情報である。そして、状態保存部２１が、前回の実行状態を表す情報に含まれるオブジェクトと比較して、現在の実行状態において内容に変更のあったメモリ１３内のオブジェクトを検出したとする。この場合、状態保存部２１は、幅優先探索順序において変更のあったオブジェクトと同じ深さに存在するオブジェクト以降については、前回の実行状態を表す情報からのコピーではなく、メモリ１３内のオブジェクトを幅優先探索順序で整列させながら抽出する。そして状態保存部２１は、抽出されたオブジェクトを保存領域へコピーする。また、状態保存部２１は、該当する深さが存在するオブジェクト以降については、ハッシュ値を新たに算出し、深さを表す情報とともにメタ情報として保存領域に格納する。
【００６６】
保存領域に格納される実行状態を表す情報の構成の一例を、模式的に図６に示す。図６において、実行状態を表す情報は、幅優先探索順序で連続した領域に並ぶオブジェクト列と、メタ情報とから成る。メタ情報は、オブジェクト列の各オブジェクトについて、ハッシュ値と、そのオブジェクトの深さを表す情報とを保持する。ハッシュ値は、オブジェクト列の先頭のオブジェクト（ルートオブジェクト）から該当するオブジェクトまでの情報に対して算出されるハッシュ値である。そのようなハッシュ値は、ルートオブジェクトから最後尾のオブジェクトまでの情報に対して算出されるハッシュ値の途中計算値である。以降、各オブジェクトについて算出されるこのようなハッシュ値を、「ハッシュ値の途中計算値」とも記載する。また、オブジェクトの深さを表す情報は、前述のように、そのオブジェクトの幅優先探索順序におけるルートオブジェクトからの深さである。このようなハッシュ値の途中計算値および深さを表す情報を保持するメタ情報のデータ構造の一例として、図６には、ハッシュ・キャッシュ・テーブルを示している。ハッシュ・キャッシュ・テーブルは、オブジェクト列のオブジェクトと同じ個数の要素を持つ配列である。ハッシュ・キャッシュ・テーブルのｉ（ｉ＝1、2、3、・・・、Ｌ）番目の要素は、ルートオブジェクト（ｒｏｏｔ）からｉ番目のオブジェクトｏｂｊ_ｉまでのハッシュ値の途中計算値ｈ＿ｉと、そのオブジェクトｏｂｊ＿ｉの幅優先探索順序での深さｄ＿ｉとが組となった情報である。ハッシュ値の性質上、ハッシュ値の途中計算値ｈ＿ｉと、（ｉ＋１）番目のオブジェクトｏｂｊ＿ｉ＋１とを用いて、ハッシュ値の途中計算値ｈ_ｉ＋１が算出可能である。このようにして算出された最後の要素のハッシュ値ｈ＿Ｌの値は、ルートオブジェクト（ｒｏｏｔ）から最後のオブジェクトｏｂｊ＿Ｌまでの全体を幅優先探索順序で整列した情報に対するハッシュ値と等しくなる。
【００６７】
状態復元部２２は、本発明の第１の実施の形態における状態復元部１２と同様に、保存領域に格納された実行状態を表す情報を、格納されている順序に従ってメモリ１３内の復元領域にコピーしていくことにより、実行状態の復元を行う。このとき、本実施の形態では、状態復元部２２は、オブジェクト内においてオフセット値に置き換えられた参照情報を、そのオフセット値に復元領域の先頭アドレスを足した値に置き換えて復元領域にコピーする。
【００６８】
以上のように構成された状態保存復元装置２の動作について、図面を参照して説明する。
【００６９】
状態保存復元装置２の状態保存動作を図７に示す。
【００７０】
図７では、まず、状態保存部２１は、実行状態を保存するための保存領域をメモリ１３の内部に確保する（ステップＳ２１）。このとき、状態保存部２１は、少なくともオブジェクト列を保存する領域については、連続した領域を確保するようにする。
【００７１】
次に、状態保存部２１は、メモリ１３の内部に前回の実行状態を表す情報が格納された保存領域があるかどうかを調べる（ステップＳ２２）。
【００７２】
ここで、前回の実行状態を表す情報が存在しない場合というのは、例えば、ソフトウェアモデル検査を実行するための初期の実行状態（初期状態）が生成された直後である。
【００７３】
この場合、状態保存部２１は、この初期状態におけるメモリ１３内のルートオブジェクトと深さ０とを組とし、オブジェクトを幅優先探索順序で抽出するための幅優先探索キューを初期化する（ステップＳ２３）。つまり、この状態では、幅優先探索キューには、ルートオブジェクトを表す情報と深さ０との組が保持されている。
【００７４】
そして、状態保存部２１は、幅優先探索キューから取り出したオブジェクトによって参照される各オブジェクトを、オブジェクト探索キューに入れるとともに、取り出したオブジェクトを保存領域にコピーする。このとき、状態保存部２１は、オブジェクト内に参照情報があれば、その参照情報を基底アドレスからのオフセット値に置き換えて保存領域にコピーする。併せて、状態保存部２１は、ハッシュ・キャッシュ・テーブルの各々の要素に紐付けられる深さを表す情報を更新する（ステップＳ２４）。
【００７５】
状態保存部２１は、ステップＳ２４を繰り返すことにより、メモリ１３内のオブジェクトを、幅優先探索キューを用いて幅優先探索順序で抽出しながら、確保した保存領域に順次コピーしていく。
【００７６】
幅優先探索によるオブジェクトのコピーが終了したら、状態保存部２１は、保存されたオブジェクトを保存領域に並んでいる順序に従って走査しながら、ルートオブジェクトから各オブジェクトまでのハッシュ値の途中計算値を求める。そして、状態保存部２１は、ハッシュ・キャッシュ・テーブルにおける対応する要素のハッシュ値を更新する（ステップＳ２５）。
【００７７】
このようにして、ソフトウェアモデル検査において最初に生成された初期状態を保存する場合には、メモリ１３内のオブジェクト全体が幅優先探索順序に従って抽出されて保存される。また、ハッシュ・キャッシュ・テーブルの最後の値は、保存された初期状態を表す情報全体に対するハッシュ値となっている。
【００７８】
一方、ソフトウェアモデル検査の過程において、検査対象ソフトウェアの一部が状態遷移のために実行された後の状態の場合には、ステップＳ２２において、前回の実行状態を表す情報が存在すると判断される。
【００７９】
この場合、状態保存部２１は、保存されている前回の実行状態を表す状態に含まれるオブジェクトを、その格納順に、状態遷移後の実行状態におけるメモリ１３内のオブジェクトと１つずつ比較する。そして、状態保存部２１は、この比較の結果、これらのオブジェクトが同じ間だけ、前回の実行状態を表す情報から、オブジェクトおよびこれらに関連付けされたハッシュ・キャッシュ・テーブルの要素を、今回の実行状態を保存するための保存領域にコピーする（ステップＳ２６）。本ステップにおいて、これらのオブジェクトが同じとは、比較した２つのオブジェクトが同一であることを意味する。
【００８０】
具体的には、例えば、オブジェクトが数字や文字列といった値の場合には、状態保存部２１は、値同士を比較する。また、例えば、オブジェクトが配列やリストのように他のオブジェクトを包含できるコンテナの場合には、状態保存部２１は、保存されたオブジェクトおよびメモリ１３内のオブジェクトを、コンテナ中のフィールドごとに比較する。また、フィールドが他のオブジェクトへの参照を表す場合には、前回の実行状態を表す情報においてオブジェクトへの参照は、基底アドレス０からのオフセット値で表現されている。また、この場合、メモリ１３のオブジェクトにおけるオブジェクトへの参照は、ポインタとなっている。そこで、この場合、状態保存部２１は、メモリ１３内のオブジェクトにおけるポインタから、メモリ１３内のルートオブジェクトのアドレスＹを減算することによりオフセット値に変換した後、前回の実行状態を表す状態に含まれるオブジェクトと比較する。
【００８１】
次に、状態保存部２１は、前回の実行状態を表す情報に含まれるオブジェクトに対して、メモリ１３内のオブジェクトの内、異なるオブジェクトを検出する。そして状態保存部２１は、検出したオブジェクトと同じ深さにあるオブジェクトを用いて、幅優先探索キューを初期化する（ステップＳ２７）。
【００８２】
ここで、前回の実行状態を表す情報とは異なるオブジェクト（変更されたオブジェクト）が検出されるのは、ソフトウェアモデル検査の過程で状態遷移のために、検査対象ソフトウェアを構成するプログラムの一部が実行されたことに起因する。ここでは、説明のため、前回の実行状態を表す情報に対して異なることが検出されたメモリ１３内のオブジェクトをＯ＿Ｈ＿Ｄｉｆｆと記載する。また、Ｏ＿Ｈ＿Ｄｉｆｆに紐付けられた、前回の実行状態を表す情報の中のオブジェクトをＯ＿Ｓ＿Ｄｉｆｆと記載する。
【００８３】
詳細には、前回の実行状態を表す情報には、幅優先探索順序でオブジェクトが含まれている。したがって、Ｏ＿Ｓ＿ＤｉｆｆおよびＯ＿Ｈ＿Ｄｉｆｆが異なる場合に、Ｏ＿Ｈ＿Ｄｉｆｆに行われた変更の影響によって、幅優先探索順序でＯ＿Ｈ＿Ｄｉｆｆよりも深さが大きいオブジェクトの並び方に影響が出る可能性がある。幅優先探索順序でＯ＿Ｈ＿Ｄｉｆｆよりも深さが大きいオブジェクトは、Ｏ＿Ｈ＿Ｄｉｆｆと同じ深さでＯ＿Ｈ＿Ｄｉｆｆよりも先に抽出されたオブジェクトからも参照されうる。そこで、状態保存部２１は、ハッシュ・キャシュ・テーブルを参照することにより、Ｏ＿Ｈ＿Ｄｉｆｆの幅優先探索順序における深さｄと同じ深さにあるオブジェクトおよびその順序を特定する。そして、状態保存部２１は、同じ深さｄにあるオブジェクト群をその順序で、幅優先探索キューの初期値として初期化する。このように初期化された幅優先探索キューから探索されるオブジェクトは、前回の実行状態から変更が加えられているか、あるいは、変更によってメモリ１３内での相対位置が変化している可能性があるものである。
【００８４】
状態保存部２１は、このように変更のあった深さのオブジェクト群で初期化された幅優先探索キューを用いて、前述のステップＳ２４を実行する。すなわち、状態保存部２１は、幅優先探索キューから取り出したオブジェクトによって参照される各オブジェクトを幅優先探索キューに入れるとともに、取り出したオブジェクトを保存領域にコピーする。併せて、状態保存部２１は、参照情報のオフセット値への変換と、ハッシュ・キャッシュ・テーブルにおける深さを表す情報を更新する。
【００８５】
幅優先探索によるオブジェクトのコピーが終了したら、状態保存部２１は、前述のステップＳ２５を実行する。すなわち、状態保存部２１は、保存されたオブジェクトを保存領域に並んでいる順序で走査しながら、ルートオブジェクトから各オブジェクトまでのハッシュ値の途中計算値を求める。ただし、この場合、ステップＳ２６において、ルートオブジェクトから変更のなかったオブジェクトまでの各オブジェクトについては、既にハッシュ値の途中計算値が、ハッシュ・キャッシュ・テーブルの各々の要素に関連付けられた値にコピーされている。したがって、状態保存部２１は、変更のあったオブジェクト以降について、ハッシュ値の途中計算値を算出し、ハッシュ・キャッシュ・テーブルにおける各要素を更新すればよい。
【００８６】
このようにして、ソフトウェアモデル検査の過程では、状態遷移後の実行状態を保存する場合には、メモリ１３内のオブジェクトのうち前回からの変更がない部分までは前回の実行状態を表す情報からコピーされる。また、変更のあったオブジェクトと同じ深さのオブジェクト以降は、新たに幅優先探索により整列されてメモリ１３内から抽出され保存される。また、ハッシュ・キャッシュ・テーブルの最後の値は、状態遷移後の実行状態を表す情報全体のハッシュ値となっている。
【００８７】
以上で、状態保存復元装置２は、状態保存動作を終了する。
【００８８】
次に、状態保存復元装置２の状態復元動作を、図８に示す。
【００８９】
図８では、まず、状態復元部２２は、メモリ１３内に、連続した復元領域を確保する（ステップＳ３１）。例えば、状態復元部２２は、復元対象の前回の実行状態を表す情報を参照することにより、そのオブジェクト列のサイズＬ以上の連続した復元領域を確保すればよい。説明のため、復元領域の先頭アドレスをＸとする。
【００９０】
次に、状態復元部２２は、オブジェクトの相対位置ｉを０で初期化する（ステップＳ３２）。
【００９１】
次に、状態復元部２２は、前回の実行状態を表す情報において相対位置がｉのオブジェクトを、メモリ１３内の復元領域に書き戻す（ステップＳ３３）。もし、書き戻すオブジェクトが、数字や文字列等の値の場合には、状態復元部２２は、値をそのまま復元領域にコピーする。また、書き戻すオブジェクトが、配列やリストのように他のオブジェクトを包含できるコンテナの場合には、状態復元部２２は、コンテナ中に含まれる他のオブジェクトへの参照であるオフセット値に対して、復元領域の先頭アドレスＸを足す。尚、状態復元部２２は、オフセット値を、先頭アドレスＸを足した値に変更した際に、コンテナ中の各フィールドを復元領域にコピーする処理も行うものとする。これにより、保存された前回の実行状態を表す情報の中では、基底アドレス０からのオフセット値で表現されていたオブジェクトへの参照が、メモリ１３内に確保された復元領域の先頭アドレスＸをもとにしたポインタ値へと変換される。
【００９２】
次に、状態復元部２２は、相対位置ｉに１を加算して更新する（ステップＳ３４）。
【００９３】
ここで、ｉが、前回の実行状態を表す情報に含まれるオブジェクト列のサイズＬと同じになったら（ステップＳ３５でＹｅｓ）、状態復元部２２は復元動作を終了する。
【００９４】
ｉがオブジェクト列のサイズＬ未満であれば、状態復元部２２は、次のオブジェクトの復元を行うため、ステップＳ３３からの動作を繰り返す。
【００９５】
以上で、状態保存復元装置２は、状態復元動作を終了する。
【００９６】
次に、状態保存復元装置２の動作を具体例で示す。
【００９７】
なお、この具体例において、保存領域に格納される実行状態を表す情報は、前述の図６に示した構成であるものとする。
【００９８】
また、この具体例において、検査対象ソフトウェアによって初期状態において用いられるメモリ１３内のオブジェクトについて、その参照グラフの一部を図９に示す。図９では、ルートオブジェクトｒｏｏｔは、オブジェクトｏｂｊＡ、オブジェクトｏｂｊＢ、オブジェクトｏｂｊＣ、オブジェクトｏｂｊＤ、オブジェクトｏｂｊＥを参照する。オブジェクトｏｂｊＡは、オブジェクトｏｂｊＰを参照する。オブジェクトｏｂｊＢは、オブジェクトｏｂｊＱを参照する。オブジェクトｏｂｊＣは、オブジェクトｏｂｊＲを参照する。この場合、幅優先探索順序でオブジェクトを整列すると、以下のような、順序となるものとする。
ルートオブジェクトｒｏｏｔ、
オブジェクトｏｂｊＡ、
オブジェクトｏｂｊＢ、
オブジェクトｏｂｊＣ、
オブジェクトｏｂｊＤ、
オブジェクトｏｂｊＥ、
オブジェクトｏｂｊＰ、
オブジェクトｏｂｊＱ、
オブジェクトｏｂｊＲ。
【００９９】
このとき、状態保存復元装置２は、以下のように動作して実行状態を保存する。
【０１００】
状態保存部２１は、実行状態を保存するための保存領域を確保する（図７のステップＳ２１）。
【０１０１】
次に、状態保存部２１は、前回の実行状態を表す情報が格納された保存領域があるかどうかを調べる。ここでは、初期状態なので、前回の実行状態を表す情報は存在しない（ステップＳ２２でＮｏ）。
【０１０２】
そこで、状態保存部２１は、初期状態のメモリ１３におけるルートオブジェクトであるオブジェクトｒｏｏｔおよび深さ０を組として、幅優先探索キューを初期化する（ステップＳ２３）。
【０１０３】
そして、状態保存部２１は、幅優先探索キューの中のオブジェクトを参照しながら幅優先探索順序でオブジェクトを抽出し、ステップＳ２１で確保した保存領域にコピーする。このとき、状態保存部２１は、各オブジェクトに含まれる他のオブジェクトへの参照情報（ポインタ）を、ルートオブジェクトｒｏｏｔの位置を０番地としたときのオフセット値に置き換えてから、保存領域にコピーする。併せて、状態保存部２１は、ハッシュ・キャッシュ・テーブルの各々の要素に紐付けられた深さの情報を更新する（ステップＳ２４）。
【０１０４】
ここで、メモリ１３内においてどの番地に各オブジェクトが配置されていても、保存対象となる全オブジェクトの参照グラフ中でのオブジェクトの位置が変わらなければ、そのオブジェクトに対する参照としてのオフセット値は同じになる。したがって、状態保存部２１は、参照情報をオフセット値に置き換えることにより、メモリ１３内での実際の配置番地によらずに、実行状態を保存できる。
【０１０５】
次に、幅優先探索によるオブジェクトのコピーが終了したら、状態保存部２１は、保存領域に格納されたオブジェクトを並んでいる順序で走査しながら、先頭オブジェクトから各オブジェクトまでのハッシュ値の途中計算値を求める。そして、状態保存部２１は、ハッシュ・キャッシュ・テーブルの各要素に含まれるハッシュ値の情報を、求めた途中計算値に更新する（ステップＳ２５）。
【０１０６】
これにより、ソフトウェアモデル検査において最初に生成された初期状態を表す情報が保存された。このように、初期状態を保存する場合には、メモリ１３内のオブジェクト全体が、幅優先探索順序で抽出されて保存される。このようにして保存領域に保存された初期状態を表す情報を、図１０に示す。図１０において、オブジェクト列には、メモリ１３内のルートオブジェクトｒｏｏｔに対して保存されたルートオブジェクトｒｏｏｔが先頭（０番）に格納されている。続いて、幅優先探索順序に従って整列されたオブジェクトｏｂｊＡからオブジェクトｏｂｊＲ（Ｌ番）までが順次格納されている。また、メタ情報のハッシュ・キャッシュ・テーブルは、幅優先探索順序で整列されたオブジェクトｒｏｏｔからオブジェクトｏｂｊＲまでと同じ８個の要素を含む。また、各要素は、ハッシュ値の途中結果値と、幅優先探索順序における深さとからなる。例えば、ハッシュ・キャッシュ・テーブルにおける１つ目の要素＜ｈ＿０、０＞は、ルートオブジェクトｒｏｏｔのハッシュ値ｈ＿０および深さ０を表す情報を表している。また、２つ目の要素＜ｈ＿１，１＞は、ルートオブジェクトｒｏｏｔからオブジェクトｏｂｊＡまでのバイト列に対するハッシュ値ｈ＿１と、幅優先探索における深さ１を表す情報を表している。
【０１０７】
なお、状態保存部２１は、このハッシュ値の計算に、どのような技術を用いてもよいが、一例としてＭＤ５（Message Digest Algorithm ５）を用いてもよい。通常、このようなハッシュ関数によれば、先頭のオブジェクトから（ｉ＋１）番目のオブジェクトまでのハッシュ値ｈ＿ｉ＋１を追加的に算出することができる。この計算の際には、先頭のオブジェクトからｉ番目のオブジェクトまでのハッシュ値ｈ＿ｉと、（ｉ＋１）番目のオブジェクトのバイト列とを用いる。具体的には、例えば、オブジェクトｏｂｊＢまでのハッシュ値ｈ＿２は、オブジェクトｏｂｊＡまでのハッシュ値ｈ＿１とオブジェクトｏｂｊＢのバイト列とから算出できる。そして、このような追加的な算出により算出されたハッシュ・キャッシュ・テーブルの最後の要素のハッシュ値ｈ＿８は、保存されたすべてのオブジェクト列に対するハッシュ値となる。このような全オブジェクトに対するハッシュ値は、メモリ１３内から抽出されて保存された全オブジェクトおよびオブジェクト間の参照グラフが同じであれば同一となる。したがって、このようなハッシュ値によれば、状態保存復元装置２の実行状態の既達管理（即ち、どこまで実効が済んだかの管理）が可能である。
【０１０８】
次に、このようにして保存された初期状態または他の実行状態が復元された状態から、検査対象ソフトウェアの一部が実行された後の状態において、状態保存復元装置２が、実行状態を保存する動作について、図１１の模式図を用いて説明する。
【０１０９】
図１１では、前回の実行状態を表す情報が格納された保存領域を、Ｓ＿Ｂｅｆｏｒｅと呼ぶものとする。また、Ｓ＿Ｂｅｆｏｒｅが復元されたメモリ１３内のオブジェクトは、アドレスＹを始点に並ぶものとする。また、この復元されたメモリ１３内のオブジェクトを用いて検査対象ソフトウェアの一部が実行された後の「現在の実行状態」が新たに保存される保存領域を、Ｓ＿Ａｆｔｅｒと呼ぶものとする。
【０１１０】
ここでは、状態保存部２１は、前回の実行状態を表す情報が格納されている保存領域Ｓ＿Ｂｅｆｏｒｅがあると判断する（ステップＳ２２でＹｅｓ）。この場合、状態保存部２１は、Ｓ＿Ｂｅｆｏｒｅ中に含まれるオブジェクトと、現在の実行状態においてアドレスＹを始点に並ぶオブジェクトとを、格納順に１つずつ比較していく。状態保存部２１は、オブジェクトが数字あるいは文字列といった値の場合には、そのまま比較する。また、状態保存部２１は、オブジェクトが、配列やリストのように他のオブジェクトを包含できるコンテナの場合には、Ｓ＿Ｂｅｆｏｒｅ中のオブジェクトとメモリ１３内のオブジェクトとを、コンテナの中のフィールドごとに比較する。また、フィールドが他のオブジェクトへの参照の場合、状態保存部２１は、Ｓ＿Ｂｅｆｏｒｅにおけるオブジェクトへの参照であるオフセット値と、メモリ１３内におけるオブジェクトへ参照であるポインタ値からアドレスＹを引いた値とを比較すればよい。
【０１１１】
ここで、アドレスＹを始点に並ぶメモリ１３内のオブジェクトは、状態復元部２２により連続した領域に配置されたものである。このため、変更のないオブジェクトまでは、Ｓ＿Ｂｅｆｏｒｅ中のオブジェクト列と等価な情報がメモリ１３内に同じ幅優先探索順序で配置されている。したがって、状態保存部２１は、オブジェクト単位で比較した結果が等価な場合に、Ｓ＿Ｂｅｆｏｒｅ中の該当するオブジェクトおよびハッシュ・キャッシュ・テーブルの該当する要素を、Ｓ＿Ａｆｔｅｒ中にそのままコピーすればよい。
【０１１２】
そこで、状態保存部２１は、Ｓ＿Ｂｅｆｏｒｅ中のオブジェクトとメモリ１３内のオブジェクトとを比較して同一である間だけ、Ｓ＿ＢｅｆｏｒｅからＳ＿Ａｆｔｅｒにオブジェクトをコピーする。また、状態保存部２１は、Ｓ＿Ｂｅｆｏｒｅ中のハッシュ・キャッシュ・テーブルの各々の要素に紐付けられる要素を、Ｓ＿Ａｆｔｅｒ中のハッシュ・キャッシュ・テーブルにコピーする（ステップＳ２６）。
【０１１３】
ここで、検査対象ソフトウェアの一部の実行により、前回の実行状態に対して、オブジェクトｏｂｊＱが別のオブジェクトｏｂｊＸを参照するように変更され、オブジェクトｏｂｊＲが別のオブジェクトｏｂｊＹを参照するように変更されていたとする。この場合、幅優先探索順序で比較して同じであったルートオブジェクトｒｏｏｔからオブジェクトｏｂｊＰまでは幅優先探索順序が変わらない。しかしながら、オブジェクトｏｂｊＱ以降に並ぶオブジェクトは、追加、変更あるいは削除により幅優先探索順序における出現位置が変化する可能性がある。このとき、幅優先探索順序でオブジェクトｏｂｊＱ以降に表れるオブジェクトは、幅優先探索順序でオブジェクトｏｂｊＱと同じ深さのオブジェクトだけから探索される。したがって、状態保存部２１は、オブジェクトｏｂｊＱの幅優先探索順序での深さ２と同じ深さのオブジェクトから、幅優先探索順序でオブジェクトの再走査を行う。具体的には、状態保存部２１は、ハッシュ・キャシュ・テーブルを参照することにより、変更のあったｏｂｊＱと同じ深さ２のオブジェクトとして、オブジェクトｏｂｊＰ、オブジェクトｏｂｊＱおよびオブジェクトｏｂｊＲを得る。そこで、状態保存部２１は、これらのオブジェクトｏｂｊＰ、ｏｂｊＱ、ｏｂｊＲを用いて幅優先探索キューを初期化する（ステップＳ２７）。
【０１１４】
以降、状態保存部２１は、幅優先探索キューを用いることにより幅優先探索順序で抽出したオブジェクトを、Ｓ＿Ａｆｔｅｒにコピーしていく。併せて、状態保存部２１は、参照情報のオフセット値への変換と、ハッシュ・キャッシュ・テーブルの各々の要素に紐付けられる深さ情報を更新する（ステップＳ２４）。
【０１１５】
次に、幅優先探索順序によるオブジェクトコピーが終了したら、状態保存部２１は、Ｓ＿Ａｆｔｅｒに格納されているオブジェクトを、並んでいる順序で走査しながらハッシュ値の途中計算値を求め、ハッシュ・キャッシュ・テーブルを更新する（ステップＳ２５）。
【０１１６】
このとき、Ｓ＿Ａｆｔｅｒ中において、オブジェクトｒｏｏｔからオブジェクトｏｂｊＰまでの各オブジェクトに関連付けられるハッシュ・キャッシュ・テーブルのハッシュ値ｈ＿０〜ｈ＿６は、コピーにより既に格納されている。そこで、状態保存部２１は、ルートオブジェクトｒｏｏｔからオブジェクトｏｂｊＱまでのハッシュ値ｈ’＿７を、ハッシュ・キャッシュ・テーブルの一つ前の要素のハッシュ値ｈ＿６と、オブジェクトｏｂｊＱのバイト列とから算出すればよい。そして、状態保存部２１は、次のハッシュ値ｈ’＿８を、ハッシュ値ｈ’＿７と、オブジェクトｏｂｊＲのバイト列とから算出する処理を繰り返す。そして、状態保存部２１は、Ｓ＿Ａｆｔｅｒ中の最後のオブジェクトに関連付けられるハッシュ・キャッシュ・テーブルのハッシュ値までを更新する。このようにして、状態保存部２１は、変更のあったオブジェクトｏｂｊＱ以降についてハッシュ値の途中計算値を算出していくだけで、Ｓ＿Ａｆｔｅｒ中に格納された全オブジェクトに対するハッシュ値を算出することができた。このハッシュ値は、本実施の形態を用いたソフトウェアモデル検査システムによって、既達状態の管理に用いられる。
【０１１７】
以上で、状態保存動作の具体例の説明を終了する。
【０１１８】
次に、状態復元動作の具体例を、図１２を参照して説明する。
【０１１９】
ここでは、状態復元部２２は、図１１のＳ＿Ｂｅｆｏｒｅを復元するものとする。
【０１２０】
まず、状態復元部２２は、Ｓ＿Ｂｅｆｏｒｅに含まれるオブジェクト列のサイズであるＬ１以上の連続した領域を、メモリ１３内に復元領域として確保する（ステップＳ３１）。ここでは、確保した復元領域の先頭アドレスはＸであるものとする。
【０１２１】
次に、状態復元部２２は、復元するオブジェクトの相対位置ｉをゼロで初期化する（ステップＳ３２）。
【０１２２】
次に、状態復元部２２は、Ｓ＿Ｂｅｆｏｒｅ中で相対位置ｉにあるオブジェクトを、メモリ１３内の復元領域にコピーする（ステップＳ３３）。このとき、状態復元部２２は、コピー対象のオブジェクトが値であればそのままコピーする。また、状態復元部２２は、コピー対象のオブジェクトが他のオブジェクトへの参照を含むコンテナの場合には、オブジェクト中で参照を表しているオフセット値を、復元領域の先頭アドレスＸを加算した値に変換してからコピーする。状態復元部２２は、ステップＳ３３の動作を、相対位置ｉに１を加算して更新しながらｉがオブジェクト列のサイズＬ（図１２ではＬ１）になるまで繰り返す（ステップＳ３４、Ｓ３５）。
【０１２３】
以上で、状態復元動作の具体例の説明を終了する。
【０１２４】
次に、本発明の第２の実施の形態の効果について述べる。
【０１２５】
本発明の第２の実施の形態としての情報保存復元装置２は、実行状態を表す情報に対するハッシュ値が実行状態の既達管理に用いられるソフトウェアモデル検査に際して、ハッシュ値の計算コストをより削減して、実行状態の復元および保存をさらに高速に行うことができる。
【０１２６】
その理由は、状態保存部２１が、メモリ内のオブジェクトを所定の整列順序で保存領域にコピーする際に、先頭のオブジェクトから各オブジェクトまでの情報に対するハッシュ値（途中計算値）を算出してオブジェクトと共に保存領域に保存するからである。そして、状態保存部が、前回の実行状態を表す情報が格納された保存領域がある場合、前回の実行状態を表す情報に含まれるオブジェクトを格納されている順序でメモリ１３内のオブジェクトと比較する。比較の際、状態保存部２１は、先頭のオブジェクトから変更のないオブジェクトまでは、前回の実行状態を表す情報に含まれるオブジェクトおよびその途中計算値を今回の実行状態の保存領域にコピーするからである。また、状態保存部２１が、保存領域に保存された実行状態を表す情報に含まれるオブジェクトを、格納されている順序でメモリ内の復元領域にコピーしていくことにより復元するからである。
【０１２７】
ソフトウェアモデル検査の過程において、メモリ１３内のオブジェクトは、状態復元部２１によって前回の実行状態が復元された状態から遷移したオブジェクトであるので、メモリ１３内での並びは、前回の実行状態を表す情報の中のオブジェクトの並びとおおむね同一となる。通常、ソフトウェアモデル検査においてプログラムを一単位分実行することで発生する一回の状態遷移によるオブジェクトの変更は小さい。したがって、状態保存部２１は、ルートオブジェクトから変更の無いオブジェクトまでに関しては、おおむねメモリ１３内に並んだ順序で走査しながらコピーし、変更の有ったオブジェクト以降を抽出すればよい。また、状態復元部２１は、保存領域に連続して並んだオブジェクトを、その順序に従ってメモリ１３内に復元する。
【０１２８】
これにより、本実施の形態は、状態の保存から復元におけるオブジェクトのコピーを、保存領域またはメモリ１３内の順序で行うことができるので、簡便である。したがって、本実施の形態は、状態の抽出および復元を極力メモリ１３内部のオブジェクトの格納順に行うことで、メモリ１３へのランダムアクセスによる性能低下を小さくすることができる。
【０１２９】
このように、本実施の形態は、ソフトウェアモデル検査に必要な実行状態の保存を、内部のメモリ形式に近い形態でかつ連続した領域に保存することで、復元する場合にも、メモリ１３内の連続する領域にコピーすることができる。したがって、本実施の形態は、オブジェクトの再生成処理やそのためのオブジェクト参照グラフの走査によるオーバーヘッドを小さくできる。
【０１３０】
また、本実施の形態は、メモリ１３内からオブジェクトを抽出して実行状態を保存する際に、前回の実行状態を表す情報に対して差分のあったオブジェクトを検出し、そのオブジェクト以降からハッシュ値の途中計算値を追加的に算出する。つまり、本実施の形態は、ソフトウェアモデル検査において既達状態の管理に用いるハッシュ計算の途中計算値を、保存された実行状態を表す情報中にキャッシュする。これにより本実施の形態によれば、次に実行状態の保存を行う際には、変更のあった部分以降だけを再計算だけでよいので、ハッシュ値計算のコストを削減することができる。
【０１３１】
さらに、本実施の形態は、状態復元部が、状態保存部により実行状態を抽出しやすい形態でメモリ１３内に実行状態を復元するので、効果が累積的になり、ソフトウェアモデル検査で問題となる状態の復元および保存と、既達状態管理のためのハッシュ値の計算を効率化することができる。
【０１３２】
本発明の第２の実施の形態において、実行状態を保存するために抽出するオブジェクトの整列順序として、幅優先探索順序を適用する例を中心に説明した。しかしながら、上述した各実施の形態を例に説明した本発明において、整列順序は、その他の順序であってもよい。そのような整列順序は、オブジェクトの参照関係が変わらない限り、その整列順序における各オブジェクトの位置が一意に定まる順序であればよい。
【０１３３】
本発明の第２の実施の形態において、実行状態を表す情報に含まれるメタ情報が、ハッシュ値の途中計算値および幅優先探索順序における深さの情報から成る例を中心に説明した。しかしながら、上述した各実施の形態を例に説明した本発明において、メタ情報は、各オブジェクトに関するその他の情報を含んでいてもよい。
【０１３４】
本発明の第２の実施の形態において、実行状態を表す情報に含まれるメタ情報が、ハッシュ・キャッシュ・テーブルとして構成される例を中心に説明したが、実行状態を表す情報は、その他のデータ構造であってもよい。
【０１３５】
本発明の第２の実施の形態において、状態保存部２１は、特に、ヒープメモリ内のオブジェクトを抽出して保存し、ヒープメモリ内に復元するようにしてもよい。ソフトウェアによって用いられるヒープメモリ内のオブジェクトは、その内容および参照関係を正しく復元すれば再度利用することができ、本発明による保存および復元の対象として適している。これにより、各実施の形態は、実行状態を表す情報として保存する情報のサイズや、その保存および復元にかかる時間をいたずらに増大させることなく、ソフトウェアモデル検査での状態探索に必要な情報を保存および復元することができる。
【０１３６】
上述した本発明の各実施の形態においては、状態保存復元装置の各機能ブロックが、記憶装置またはＲＯＭに記憶されたコンピュータ・プログラムを実行するＣＰＵによって実現される例を中心に説明した。しかしながら、上述した各実施の形態を例に説明した本発明は、各機能ブロックの一部、全部、または、それらの組み合わせが専用のハードウェアにより実現されていてもよい。
【０１３７】
上述した本発明の各実施の形態において、状態保存復元装置の機能ブロックは、複数の装置に分散されて実現されてもよい。
【０１３８】
上述した各実施の形態において、各フローチャートを参照して説明した状態保存復元装置の動作は、コンピュータ・プログラムとしてコンピュータ装置の記憶装置（記憶媒体）に格納しておき、係るコンピュータ・プログラムを当該ＣＰＵが読み出して実行することによって実現してもよい。そして、このような場合において、本発明は、係るコンピュータ・プログラムを表すコードあるいはそのコードがコンピュータ読み取り可能に格納された記憶媒体によって構成されると捉えることができる。
【０１３９】
上述した各実施の形態は、適宜組み合わせて実施されることが可能である。
【０１４０】
以上、上述した実施形態を模範的な例として本発明を説明した。しかしながら、本発明は、上述した実施形態には限定されない。即ち、本発明は、本発明のスコープ内において、当業者が理解し得る様々な態様を適用することができる。
この出願は２０１３年１２月１１日に出願された日本出願特願２０１３−２５６１６１を基礎とする優先権を主張し、その開示の全てをここに取り込む。
【符号の説明】
【０１４１】
１、２    状態保存復元装置
１１、２１    状態保存部
１２、２２    状態復元部
１３    メモリ
９００    ソフトウェアモデル検査システム
９０１    ユーザ定義コード保存部
９０２    プログラム実行部
９０３    メモリ管理部
９０４    メモリ
９０５    初期状態生成部
９０６    状態保存復元部
９０７    要探索状態管理部
９０８    遷移生成部
９０９    遷移実行部
９１０    既達状態管理部
９１１    性質検証部
９１２    判定部
１００１    ＣＰＵ
１００２    ＲＡＭ
１００３    ＲＯＭ
１００４    記憶装置
【図１】
2015087509.tif 000003
【図２】
2015087509.tif 000004
【図３】
2015087509.tif 000005
【図４】
2015087509.tif 000006
【図５】
2015087509.tif 000007
【図６】
2015087509.tif 000008
【図７】
2015087509.tif 000009
【図８】
2015087509.tif 000010
【図９】
2015087509.tif 000011
【図１０】
2015087509.tif 000012
【図１１】
2015087509.tif 000013
【図１２】
2015087509.tif 000014
【図１３】
2015087509.tif 000015
【手続補正書】
【提出日】平成28年4月21日(2016.4.21)
【手続補正２】
【補正対象書類名】特許請求の範囲
【補正対象項目名】請求項８
【補正方法】変更
【補正の内容】
【請求項８】
検査対象ソフトウェアの実行状態を表すメモリ内のオブジェクトを所定の整列順序で抽出して保存領域にコピーしていくことにより、前記実行状態を表す情報として保存する状態保存ステップと、
前記保存領域に格納された前記実行状態を表す情報に含まれる前記オブジェクトを、格納されている順序で前記メモリ内の復元領域にコピーしていくことにより、前記実行状態を復元する状態復元ステップと、
をコンピュータ装置に実行させるプログラム。
【国際調査報告】
2015087509.tif 000016
2015087509.tif 000017