(57)【要約】【課題】  ソフトウェアのモデル検査において、メモリ容量を節約できる検査装置、検査方法及びプログラムを提供する。【解決手段】  ユーザ定義コードの内容に状態を変化させる命令を検出した場合、変更記録を出力する命令を前記コードに追加するユーザ定義コード処理部と、前記ユーザ定義コード処理部が記憶するユーザ定義コード実行前の状態を記憶する状態記憶部と、検査を実施する対象の状態を、状態へのアドレスと変更記録の組み合わせで記憶する検査待ち状態記憶部と、前記状態へのアドレスと前記変更記録から検査を実施する対象の状態を生成する検査待ち状態生成部と、生成した状態に対して、前記コードを実行し、実行後の状態と前記状態の変更記録を出力するユーザ定義コード実行部と、実行後の状態に対し検査し、実行前の状態へのアドレスと前記変更記録を登録する状態検査部とを含むソフトウェアモデル検査装置。【選択図】      図１
2015032083.tif 000002
【特許請求の範囲】
【請求項１】
ユーザ定義コードの内容を走査し、状態を変化させる命令を検出した場合、前記ユーザ定義コード実行時にその状態の変更記録を出力するような命令を前記ユーザ定義コードに追加し記憶するユーザ定義コード処理部と、
前記ユーザ定義コード処理部が記憶するユーザ定義コード実行前の状態を記憶する状態記憶部と、
検査を実施する対象の状態を、前記状態記憶部が記憶する状態へのアドレスと、変更記録との組み合わせで記憶する検査待ち状態記憶部と、
前記検査待ち状態記憶部が記憶する前記状態へのアドレスと前記変更記録とから、検査を実施する対象の状態を生成する検査待ち状態生成部と、
前記検査待ち状態生成部が生成した状態に対して、前記ユーザ定義コード処理部が記憶する前記ユーザ定義コードを実行し、ユーザ定義コード実行後の状態と前記状態の変更記録を出力するユーザ定義コード実行部と、
前記ユーザ定義コード実行部が出力した前記ユーザ定義コード実行後の状態に対し、既に検査済みであるかどうかを確認し、検査していない場合、事前に与えられた性質を満たすかどうかを検査し、前記ユーザ定義コード実行前の状態へのアドレスと前記変更記録を前記検査待ち状態記憶部に登録する状態検査部と
を含むソフトウェアモデル検査装置。
【請求項２】
ユーザ定義コード処理部が、ユーザ定義コードの内容を走査し、状態を変化させる命令を発見した場合、前記ユーザ定義コード実行時にその状態の変更記録を出力するような命令を前記ユーザ定義コードに追加し記憶し、
状態記憶部が、前記ユーザ定義コード処理部が記憶するユーザ定義コード実行前の状態を記憶し、
検査待ち状態記憶部が、検査を実施する対象の状態を、前記状態記憶部が記憶する状態へのアドレスと変更記録の組み合わせで記憶し、
検査待ち状態生成部が、前記検査待ち状態記憶部が記憶する前記状態へのアドレスと前記変更記録から、検査を実施する対象の状態を生成し、
ユーザ定義コード実行部が、前記検査待ち状態生成部が生成した状態に対して、前記ユーザ定義コード処理部が記憶する前記ユーザ定義コードを実行し、ユーザ定義コード実行後の状態と前記状態の変更記録を出力し、
状態検査部が、前記ユーザ定義コード実行部が出力した前記ユーザ定義コード実行後の状態に対し、既に検査済みであるかどうかを確認し、検査していない場合、事前に与えられた性質を満たすかどうかを検査し、前記ユーザ定義コード実行前の状態へのアドレスと前記変更記録を前記検査待ち状態記憶部に登録する
ソフトウェアモデル検査方法。
【請求項３】
ユーザ定義コード処理部が、ユーザ定義コードの内容を走査し、状態を変化させる命令を発見した場合、前記ユーザ定義コード実行時にその状態の変更記録を出力するような命令を前記ユーザ定義コードに追加し記憶し、
状態記憶部が、前記ユーザ定義コード処理部が記憶するユーザ定義コード実行前の状態を記憶し、
検査待ち状態記憶部が、検査を実施する対象の状態を、前記状態記憶部が記憶する状態へのアドレスと変更記録の組み合わせで記憶し、
検査待ち状態生成部が、前記検査待ち状態記憶部が記憶する前記状態へのアドレスと前記変更記録から、検査を実施する対象の状態を生成し、
ユーザ定義コード実行部が、前記検査待ち状態生成部が生成した状態に対して、前記ユーザ定義コード処理部が記憶する前記ユーザ定義コードを実行し、ユーザ定義コード実行後の状態と前記状態の変更記録を出力し、
状態検査部が、前記ユーザ定義コード実行部が出力した前記ユーザ定義コード実行後の状態に対し、既に検査済みであるかどうかを確認し、検査していない場合、事前に与えられた性質を満たすかどうかを検査し、前記ユーザ定義コード実行前の状態へのアドレスと前記変更記録を前記検査待ち状態記憶部に登録する処理
をコンピュータに実行させるプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェアモデル検査を行う装置、検査方法、及びそのためのプログラムに関する。
【背景技術】
【０００２】
ソフトウェア開発分野において、モデル検査技術が知られている。このモデル検査技術は、ソフトウェア、例えば実行可能なプログラムを対象とし、実行過程を網羅的に探索し問題を発見する。
【０００３】
ソフトウェアのモデル検査技術の一例が特許文献１に記載されている。特許文献１に記載されたモデル検査技術は、状態を木構造で把握し、その木構造に対して、深さ優先探索法によって状態探索を行う。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開２０１２−２４８１２１号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
しかしながら、上述した特許文献１に記載された技術は、深さ優先探索法によって状態探索を行うため、バックトラックが必要となる。バックトラックとは、探索木のある枝
の末端まで検査が終了したら、既に検査した探索木を辿って、未検査の枝への分岐点まで
戻り、未調査の枝に対して検査を続行することである。したがって、特許文献１に記載された技術は、途中の枝（シーケンス状態）をすべて記憶している必要があり、探索空間が広くなるにつれて膨大なメモリが必要という問題点がある。
【０００６】
本発明の目的の一例は、上述した問題点を解決できるソフトウェアモデル検査装置、検査方法及びプログラムを提供することにある。
【課題を解決するための手段】
【０００７】
本発明の一形態におけるソフトウェアモデル検査装置は、ユーザ定義コードの内容を走査し、状態を変化させる命令を検出した場合、前記ユーザ定義コード実行時にその状態の変更記録を出力するような命令を前記ユーザ定義コードに追加し記憶するユーザ定義コード処理部と、前記ユーザ定義コード処理部が記憶するユーザ定義コード実行前の状態を記憶する状態記憶部と、検査を実施する対象の状態を、前記状態記憶部が記憶する状態へのアドレスと、変更記録との組み合わせで記憶する検査待ち状態記憶部と、前記検査待ち状態記憶部が記憶する前記状態へのアドレスと前記変更記録とから、検査を実施する対象の状態を生成する検査待ち状態生成部と、前記検査待ち状態生成部が生成した状態に対して、前記ユーザ定義コード処理部が記憶する前記ユーザ定義コードを実行し、ユーザ定義コード実行後の状態と前記状態の変更記録を出力するユーザ定義コード実行部と、前記ユーザ定義コード実行部が出力した前記ユーザ定義コード実行後の状態に対し、既に検査済みであるかどうかを確認し、検査していない場合、事前に与えられた性質を満たすかどうかを検査し、前記ユーザ定義コード実行前の状態へのアドレスと前記変更記録を前記検査待ち状態記憶部に登録する状態検査部とを備える。
【０００８】
本発明の一形態におけるソフトウェアモデル検査方法は、ユーザ定義コード処理部が、ユーザ定義コードの内容を走査し、状態を変化させる命令を発見した場合、前記ユーザ定義コード実行時にその状態の変更記録を出力するような命令を前記ユーザ定義コードに追加し記憶し、状態記憶部が、前記ユーザ定義コード処理部が記憶するユーザ定義コード実行前の状態を記憶し、検査待ち状態記憶部が、検査を実施する対象の状態を、前記状態記憶部が記憶する状態へのアドレスと変更記録の組み合わせで記憶し、検査待ち状態生成部が、前記検査待ち状態記憶部が記憶する前記状態へのアドレスと前記変更記録から、検査を実施する対象の状態を生成し、ユーザ定義コード実行部が、前記検査待ち状態生成部が生成した状態に対して、前記ユーザ定義コード処理部が記憶する前記ユーザ定義コードを実行し、ユーザ定義コード実行後の状態と前記状態の変更記録を出力し、状態検査部が、前記ユーザ定義コード実行部が出力した前記ユーザ定義コード実行後の状態に対し、既に検査済みであるかどうかを確認し、検査していない場合、事前に与えられた性質を満たすかどうかを検査し、前記ユーザ定義コード実行前の状態へのアドレスと前記変更記録を前記検査待ち状態記憶部に登録する。
【０００９】
本発明の一形態におけるプログラムは、コンピュータに、ユーザ定義コード処理部が、ユーザ定義コードの内容を走査し、状態を変化させる命令を発見した場合、前記ユーザ定義コード実行時にその状態の変更記録を出力するような命令を前記ユーザ定義コードに追加し記憶し、状態記憶部が、前記ユーザ定義コード処理部が記憶するユーザ定義コード実行前の状態を記憶し、検査待ち状態記憶部が、検査を実施する対象の状態を、前記状態記憶部が記憶する状態へのアドレスと変更記録の組み合わせで記憶し、検査待ち状態生成部が、前記検査待ち状態記憶部が記憶する前記状態へのアドレスと前記変更記録から、検査を実施する対象の状態を生成し、ユーザ定義コード実行部が、前記検査待ち状態生成部が生成した状態に対して、前記ユーザ定義コード処理部が記憶する前記ユーザ定義コードを実行し、ユーザ定義コード実行後の状態と前記状態の変更記録を出力し、状態検査部が、前記ユーザ定義コード実行部が出力した前記ユーザ定義コード実行後の状態に対し、既に検査済みであるかどうかを確認し、検査していない場合、事前に与えられた性質を満たすかどうかを検査し、前記ユーザ定義コード実行前の状態へのアドレスと前記変更記録を前記検査待ち状態記憶部に登録する処理を実行させる。
【発明の効果】
【００１０】
本発明によれば、ソフトウェアのモデル検査において、メモリ容量を節約できるという効果が得られる。
【図面の簡単な説明】
【００１１】
【図１】図１は、本発明の第１の実施形態の構成を示すブロック図である。
【図２】図２は、第１の実施の形態におけるユーザ定義コードが参照するデータのデータ構造と変更記録の一例を示す図である。
【図３】図３は、第１の実施の形態における検査待ち状態記憶部３００および検査待ち状態生成部４００における動作の一例を示す図である。
【図４】図４は、第１の実施の形態における検査待ち状態記憶部３００および検査待ち状態生成部４００における動作の一例を示す図である。
【図５】図５は、第１の実施の形態におけるソフトウェアモデル検査装置１０００をコンピュータおよびその周辺装置で実現したハードウェア構成を示す図である。
【図６】図６は、第１の実施の形態におけるソフトウェアモデル検査装置１０００でのソフトウェアモデル検査の動作の概要を示すフローチャートである。
【図７】図７は、第１の実施の形態におけるソフトウェアモデル検査装置１０００でのソフトウェアモデル検査の動作の概要を示すフローチャートである。
【発明を実施するための形態】
【００１２】
次に、本発明の実施形態について図面を参照して詳細に説明する。
【００１３】
［第１の実施の形態］
以下説明する実施の形態において、ユーザ定義コードとは、ユーザが定義したプログラムの命令列である。状態とは、ユーザ定義コードを実行する際にユーザ定義コードから参照されるデータおよびそのデータが参照するデータの集合である。このデータが実際にどのように保持されるかはプログラミング言語の処理系により異なる。また、遷移とは、ある状態から、ユーザ定義コードを実行することで別の状態に、データが変化する場合に与えられる種類を識別するための名前と、それに与えられる引数である。具体的には遷移とは、プログラムまたは関数の名称と、その引数の値である。さらに、可能な遷移とは、ある状態に対して、モデル検査の網羅探索の範囲として考慮しなければいけない遷移の部分集合である。可能な遷移を行うとは、部分集合の遷移を実行して状態を生成することである。
【００１４】
図１は、本発明の第１の実施の形態におけるソフトウェアモデル検査装置１０００の構成を示すブロック図である。図１を参照すると、ソフトウェアモデル検査装置１０００は、ユーザ定義コード処理部１００と状態記憶部２００と検査待ち状態記憶部３００と検査待ち状態生成部４００とユーザ定義コード実行部５００と状態検査部６００と、を備える。
【００１５】
次に、第１の実施の形態におけるソフトウェアモデル検査装置１０００の構成について説明する。
【００１６】
ユーザ定義コード処理部１００は、入力されたユーザ定義コード（第１のコード）に、状態の変化の履歴を示す変更記録を出力するためのコード（命令、またはプログラム）を挿入する処理を実行する。すなわち、ユーザ定義コード処理部１００は、入力されるユーザ定義コード（第１のコード）を解読する処理（走査ともいう）を実行し、その内容の中から、コードの実行によって状態を変化させる命令を検出する。その命令を検出した場合、ユーザ定義コード処理部１００は、その命令を実行する場合に生じるその状態の変化の履歴（変更記録）を出力するための命令を、ユーザ定義コードに追加する。あるいは、変更記録を出力できるようにユーザ定義コードを変更する。さらに、ユーザ定義コード処理部１００は、追加した命令を含むユーザ定義コード（第２のコード）を図示しない記憶部に記憶する。
【００１７】
ユーザ定義コードが参照するデータのデータ構造（状態）と変更記録の一例を図２に示す。図２において、状態２０００は、変更記録を出力するための命令を追加したユーザ定義コード（第２コード）を実行する前の状態で、状態２００１は、第２コードを実行した後の状態である。また、変更記録２００２は、変更記録を出力するための命令によって出力された変更記録である。
【００１８】
状態２０００は、フィールド名がｆｉｅｌｄ＿１乃至ｆｉｅｌｄ＿ｎで示されるデータを含む。各フィールドには、値（データ、オブジェクトともいう）が格納されている。ｏｂｊ１〜ｏｂｊ５は、それぞれ代表的なオブジェクトを示し、“ｏｂｊ”はｏｂｊｅｃｔ（オブジェクト）の略である。矢印は、データの参照先を示す。データｏｂｊ１において、フィールドＸ、Ｙの値がそれぞれｏｂｊ５、ｏｂｊ２である。データｏｂｊ５において、フィールドＹの値が、ｏｂｊ４ｏｌｄである。データｏｂｊ２において、フィールドＸの値がｏｂｊ３である。データｏｂｊ３において、フィールドＸの値がｏｂｊ４ｏｌｄである。
【００１９】
状態２０００と状態２００１を比較すると、ユーザ定義コードを実行することで、状態２０００のデータｏｂｊ３のフィールドＸの値がｏｂｊ４ｏｌｄからｏｂｊ４ｎｅｗに変化していることがわかる。このような状態の変化は、変更記録２００２に、対象データ、フィールド、フィールドの旧値、フィールドの新値の組み合わせデータとして記録される。このため状態２００１は、状態２０００と変更記録２００２によって生成可能となる。これは一例であり、状態における要素（ｏｂｊｅｃｔ）が、どの値からどの値に変更されるかが明確に示される組み合わせであれば、変更記録の構成要素がいずれでも、また変更記録の形式がどのような方法であっても構わない。
【００２０】
状態記憶部２００は、モデル検査実施時、モデル検査を実施する対象の状態の遷移前の状態を記憶する。具体的には、状態記憶部２００は、検査待ち状態生成部４００が生成した次に検査する状態を記憶する。
【００２１】
検査待ち状態記憶部３００は、検査を実施する対象の状態を記憶する。検査を実施する対象の状態は、ユーザ定義コード処理部１００が記憶するユーザ定義コード（第２のコード）を実行する前の状態、もしくは既に検査待ち状態記憶部３００に記憶されている状態に対応する。ただし、既に検査待ち状態記憶部３００に、遷移の実行前の状態が記憶されている場合、検査待ち状態記憶部３００は、その状態を指定するアドレスと変更記録との組み合わせデータを、検査を実施する対象の状態として記憶する。なお、検査待ち状態記憶部３００は、組み合わせデータを保持するキューを含む。
【００２２】
検査待ち状態生成部４００は、検査待ち状態記憶部３００が記憶する状態もしくは状態を指定するアドレスと、差分情報とから、検査を実施する対象の状態を生成する。差分情報は、後述するように変更記録を含む。
【００２３】
検査待ち状態記憶部３００および検査待ち状態生成部４００における動作の一例を図３、図４に示す。
【００２４】
図３及び図４において、状態２１００は、図２の示す状態２０００に対応する。図３において、検査待ち状態生成部４００は、ある状態２１００から、可能な遷移を行う。その遷移の実行の結果、検査待ち状態生成部４００は、状態２１０１とその状態への変化の履歴を記録する変更記録２１１１、状態２１０２とその状態への変化の履歴を記録する変更記録２１１２、状態２１０３とその状態への変化の履歴を記録する変更記録２１１３を、それぞれ生成する。検査待ち状態生成部４００は、これらの状態を生成するたびに、各状態２１０１、２１０２、２１０３に対して、その前の状態２１００とともに、検査待ち状態記憶部３００に保存する（図４）。これを可能な遷移に対して順次行う。
【００２５】
検査待ち状態生成部４００によって検査待ち状態記憶部３００のキューの中に保存されるべき各状態２１０１、２１０２、２１０３は、前状態２１００とそこからの差分情報（変更記録２１１１、２１１２、２１１３を含む）との組で表現される。このうち、前状態２１００は、各状態２１０１、２１０２、２１０３により共有される。
【００２６】
このような形で、検査待ち状態記憶部３００は、各状態でそれぞれ完全なデータを保持するのではなく、もとになる状態とその差分情報を保存する。これにより、本実施の形態では同時に保存される状態を小さくすることができる。検査待ち状態生成部４００は、検査待ち状態記憶部３００に保存されている探索すべき情報が、前状態２１００とそこからの差分情報である場合には、その差分情報に含まれる変更記録を順次、記録した順序で、状態を表すデータ構造から探索し、変更対象と同じオブジェクトを発見した場合、そのフィールドの値が古い値と同じ場合に新しい値で置き換えればよい。もし、先の状態と変更記録の情報のサイズの和が、新たな状態より大きな場合には、新たな状態のみを保持してもよい。例えば、状態２１００と変更記録２１１１の情報のサイズの和が、状態２１０１の情報のサイズより大きい場合は、空の変更記録と状態２１０１の組として表現してもよい。
【００２７】
ユーザ定義コード実行部５００は、検査待ち状態生成部４００が生成した状態を使って、ユーザ定義コード処理部１００が記憶するユーザ定義コードを実行（遷移を行い）し、ユーザ定義コード実行（遷移）後の状態と状態の変更記録を出力する。
【００２８】
状態検査部６００は、ユーザ定義コード実行部５００が出力したユーザ定義コード実行後の状態に対し、既に検査済みであるかどうかを確認する。検査していない場合、状態検査部６００は、事前に与えられた性質を満たすかどうかを検査する。検査後、状態検査部６００は、検査完了した状態を、検査済み情報として記録する。かつ状態検査部６００は、遷移後の状態が取り得る可能な遷移を、更なる状態探索の対象とするため、遷移後の状態を検査待ち状態記憶部３００に登録する。この場合、遷移後の状態は遷移前の状態と遷移前後の差分情報である変更記録によって生成可能であるため、状態検査部６００は、遷移前の状態と変更記録を検査待ち状態記憶部３００に登録する。さらに、遷移前の状態は既に状態記憶部２００に記憶されているので、状態記憶部２００に記憶されている遷移前の状態を指示するアドレスを変更記録とともに検査待ち状態記憶部３００に登録する。
【００２９】
図５は、本発明の第１の実施の形態におけるソフトウェアモデル検査装置１０００をコンピュータおよびその周辺装置で実現したハードウェア構成を示す図である。図５に示されるように、ソフトウェアモデル検査装置１０００は、ＣＰＵ１１、出力装置１２、入力装置１３、主記憶装置１４、および二次記憶装置１５を含む。
【００３０】
ＣＰＵ１１は、オペレーティングシステムを動作させて本発明の第１の実施の形態に係るソフトウェアモデル検査装置１０００の全体を制御する。また、ＣＰＵ１１は、例えば二次記憶装置１５から主記憶装置１４にプログラムやデータを読み出す。そして、ＣＰＵ１１は、第１の実施の形態におけるユーザ定義コード処理部１００、検査待ち状態生成部４００、ユーザ定義コード実行部５００、状態検査部６００として機能し、プログラム制御に基づいて各種の処理を実行する。また、ＣＰＵ１１は、１つに限らず２つ以上備えていてもよい。
【００３１】
出力装置１２は、例えばディスプレイ、表示器で実現され、出力を確認するために用いられる。
【００３２】
入力装置１３は、例えばマウスやキーボード、内蔵のキーボタンなどで実現され、入力操作に用いられる。入力装置１３は、マウスやキーボード、内蔵のキーボタンに限らず、例えばタッチパネルでもよい。
【００３３】
二次記憶装置１５は、例えば光ディスク、フレキシブルディスク、磁気光ディスク、外付けハードディスク、または半導体メモリ等であって、コンピュータプログラムをコンピュータ読み取り可能に記録する。また、コンピュータプログラムは、通信網に接続されている図示しない外部コンピュータからダウンロードされてもよい。第１の実施の形態においては状態記憶部２００、検査待ち状態記憶部３００として機能する。
【００３４】
なお、第１の実施の形態の説明において利用されるブロック図（図１）には、ハードウェア単位の構成ではなく、機能単位のブロックが示されている。これらの機能ブロックは図５に示されるハードウェア構成によって実現される。ただし、ソフトウェアモデル検査装置１０００が備える各部の実現手段は特に限定されない。すなわち、ソフトウェアモデル検査装置１０００は、物理的に結合した一つの装置により実現されてもよいし、物理的に分離した二つ以上の装置を有線または無線で接続し、これら複数の装置により実現されてもよい。
【００３５】
また、ＣＰＵ１１は、二次記憶装置１５に記録されているコンピュータプログラムを読み込み、そのプログラムにしたがって、ユーザ定義コード処理部１００、検査待ち状態生成部４００、ユーザ定義コード実行部５００、状態検査部６００として動作してもよい。
【００３６】
また、前述のプログラムのコードを記録した記録媒体（または記憶媒体）が、ソフトウェアモデル検査装置１０００に供給され、ソフトウェアモデル検査装置１０００が記録媒体に格納されたプログラムのコードを読み出し実行してもよい。すなわち、本発明は、第１の実施の形態におけるソフトウェアモデル検査装置１０００が実行するためのプログラムを一時的に記憶するまたは非一時的に記憶する二次記憶装置１５も含む。
【００３７】
以上のように構成されたソフトウェアモデル検査装置１０００の動作について、図６、図７のフローチャートを参照して説明する。
【００３８】
図６、図７は、第１の実施の形態におけるソフトウェアモデル検査装置１０００でのソフトウェアモデル検査の動作の概要を示すフローチャートである。尚、このフローチャートによる処理は、前述したＣＰＵによるプログラム制御に基づいて、実行されても良い。
【００３９】
図６、図７に示すように、まず、ユーザ定義コード処理部１００は、図示しない入力部により入力されたユーザ定義コードの内容を走査する（ステップＳ１０１）。
【００４０】
次に、ユーザ定義コードに状態を変化させる命令を検出した場合（ステップＳ１０２）、ユーザ定義コード処理部１００は、ユーザ定義コード実行時にその状態の変更記録を出力するような命令をユーザ定義コードに追加する（ステップＳ１０３）。
【００４１】
次に、ユーザ定義コード処理部１００がユーザ定義コードの内容を走査し終わった場合（ステップＳ１０４）、命令を追加したユーザ定義コードをユーザ定義コード処理部１００に記憶する（ステップＳ１０５）。ユーザ定義コードの内容を走査し終わっていない場合は、ステップＳ１０２に戻る。
【００４２】
次に、状態記憶部２００は、初期状態を記憶する（ステップＳ１０６）。初期状態とは、ソフトウェアモデル検査を実施するにあたり、網羅すべき状態の中で最初に与えられる状態である。初期状態は、入力装置１３により与えられてもよいし、図示しない初期状態生成部により生成され状態記憶部２００に送信される情報でもよい。
【００４３】
次に、検査待ち状態記憶部３００は、ステップＳ１０６で記憶された初期状態へのアドレスを記憶する（ステップＳ１０７）。検査待ち状態記憶部３００は、状態へのアドレスと変更記録の組み合わせデータを記憶するが、初期状態は変更記録がないため、検査待ち状態記憶部３００は初期状態へのアドレスのみを記憶する。
【００４４】
次に、検査待ち状態生成部４００は、検査待ち状態記憶部３００のキューから、検査を実施する対象の状態へのアドレスと、変更記録との組み合わせデータのうちの１つを取り出す（ステップＳ１０８）。本ステップの一回目は検査待ち状態記憶部３００には初期状態へのアドレスのみが記憶されているので、初期状態へのアドレスのみを取り出す。
【００４５】
次に、検査待ち状態生成部４００は、取り出した状態へのアドレスと変更記録との組み合わせデータから、次に検査する状態を生成する（ステップＳ１０９）。具体的には、図２に示すように、取り出したアドレスが指し示している状態のデータのうち、変更記録に記載される対象データｏｂｊ３のフィールドＸが、検査待ち状態生成部４００によって旧値（ｏｂｊ４）から新値（ｏｂｊ４ｎｅｗ）に書き換えられる。本ステップの一回目は初期状態へのアドレスのみが取り出されているので、本ステップでは検査待ち状態生成部４００は、初期状態を生成する。
【００４６】
次に、状態記憶部２００は、検査待ち状態生成部４００が生成した、次に検査する状態を記憶する（ステップＳ１１０）。本ステップの一回目は初期状態が生成されるが、既にステップＳ１０６で状態記憶部２００は初期状態を記憶しているので、本ステップは省略される。
【００４７】
次に、ユーザ定義コード実行部５００は、検査待ち状態生成部４００が生成した状態に対して、実行していない取り得る可能な遷移があるか確認する（ステップＳ１１１）。実行していない取り得る可能な遷移がない場合、ユーザ定義コード実行部５００は、デッドロック状態である旨のメッセージを出力し（ステップＳ１１２）モデル検査を終了する。実行していない取り得る可能な遷移がある場合、ユーザ定義コード実行部５００は、そのうちの一つの遷移を実行（ユーザ定義コード処理部１００が記憶するユーザ定義コードを実行）し、遷移後の状態と状態の変更記録を出力する（ステップＳ１１３）。
【００４８】
次に、状態検査部６００は、ユーザ定義コード実行部５００が出力した遷移後の状態に対し、既に検査済みであるかどうかを確認する（ステップＳ１１４）。具体的には、図５に示す主記憶装置１４もしくは図示しない検査済み状態記憶部に、当該の状態が検査済みである旨記録されているかどうかを確認する。当該の状態が検査されていない場合、状態検査部６００は、当該の状態が事前に与えられた性質を満たすかどうかを検査する（ステップＳ１１５）。
【００４９】
次に、状態検査部６００は、検査の結果、当該の状態が事前に与えられた性質を満たしていなければ（ステップＳ１１５でＮＯ）、エラーメッセージを出力し（ステップＳ１１６）モデル検査を終了する。当該の状態が事前に与えられた性質を満たしている場合は（ステップＳ１１５でＹＥＳ）、当該の状態を検査済みとして記録する（ステップＳ１１７）。ステップＳ１１４と同様、具体的には主記憶装置１４もしくは図示しない検査済み状態記憶部に、当該の状態が検査済みである旨記録する。
【００５０】
次に、状態検査部６００は、状態記憶部２００に記憶されている遷移前の状態へのアドレスとステップＳ１１３で出力された状態の変更記録（差分情報）とを組み合わせて検査待ち状態記憶部３００のキューに追加する（ステップＳ１１８）。
【００５１】
ステップＳ１１４において、当該の状態が既に検査済みである場合、重複の検査となるため、ステップＳ１１５〜ステップＳ１１８は行わない。
【００５２】
次に、ユーザ定義コード実行部５００は、遷移前の状態（ステップＳ１０９において検査待ち状態生成部４００が生成した状態）に対して、実行していない取り得る可能な遷移があるか確認する（ステップＳ１１９）。実行していない取り得る可能な遷移がある場合、ステップＳ１１３に戻る。
【００５３】
ステップＳ１１９で実行していない取り得る可能な遷移がない場合、検査待ち状態生成部４００は、検査待ち状態記憶部３００のキューから取り出せる、状態へのアドレスと変更記録との組み合わせデータがあるかどうか確認する（ステップＳ１２０）。もしあればステップＳ１０８に戻る。検査待ち状態記憶部３００のキューから取り出せる状態へのアドレスと変更記録の組み合わせデータがない場合、モデル検査を終了する。
【００５４】
以上で、ソフトウェアモデル検査装置１０００は、ソフトウェアモデル検査の動作を終了する。
【００５５】
次に、本発明の第１の実施の形態の効果について説明する。
【００５６】
上述した本実施形態におけるソフトウェアモデル検査装置１０００は、ソフトウェアのモデル検査において、メモリ容量を節約できる。
【００５７】
その理由は、以下のような構成を含むからである。即ち、第１に検査待ち状態記憶部３００は、検査を実施する対象の状態を、それぞれの状態を指定するアドレスと変更記録との組み合わせデータとして記憶する。これにより、検査待ち状態記憶部３００は、状態であるデータ構造そのものを逐次記憶せず、既に記憶されている状態へのアドレスと、その状態から本来記憶すべき状態との差分情報である変更記録のみを記憶するので、ソフトウェアのモデル検査において、メモリ容量を節約できるという効果が得られる。
【００５８】
以上説明した、本発明の実施形態における各構成要素は、その機能をハードウェア的に実現することはもちろん、プログラム制御に基づくコンピュータ装置、ファームウェアで実現することができる。プログラムは、磁気ディスクや半導体メモリなどのコンピュータ可読記録媒体に記録されて提供され、コンピュータの立ち上げ時などにコンピュータに読み取られる。この読み取られたプログラムは、そのコンピュータの動作を制御することにより、そのコンピュータを前述した実施の形態における構成要素として機能させる。
【００５９】
以上、実施の形態を参照して本発明を説明したが、本発明は上記実施の形態に限定されるものではない。本発明の構成や詳細には、本発明のスコープ内で当業者が理解しえる様々な変更をすることができる。
【００６０】
たとえば、以上の実施形態で説明した各構成要素は、必ずしも個々に独立した存在である必要はない。例えば、各構成要素は、複数の構成要素が１個のモジュールとして実現されたり、一つの構成要素が複数のモジュールで実現されたりしてもよい。また、各構成要素は、ある構成要素が他の構成要素の一部であったり、ある構成要素の一部と他の構成要素の一部とが重複していたり、といったような構成であってもよい。
【００６１】
また、以上説明した実施形態では、複数の動作をフローチャートの形式で順番に記載してあるが、その記載の順番は複数の動作を実行する順番を限定するものではない。このため、実施形態を実施するときには、その複数の動作の順番は内容的に支障しない範囲で変更することができる。
【符号の説明】
【００６２】
１００    ユーザ定義コード処理部
２００    状態記憶部
３００    検査待ち状態記憶部
４００    検査待ち状態生成部
５００    ユーザ定義コード実行部
６００    状態検査部
１０００    ソフトウェアモデル検査装置
２０００、２００１、２１００、２１０１、２１０２、２１０３    状態
２００２、２１１１、２１１２、２１１３    変更記録
【図１】
2015032083.tif 000003
【図２】
2015032083.tif 000004
【図３】
2015032083.tif 000005
【図４】
2015032083.tif 000006
【図５】
2015032083.tif 000007
【図６】
2015032083.tif 000008
【図７】
2015032083.tif 000009