(57)【要約】【課題】状態爆発を抑える観点からイベント発生を抑制したモデル検査プログラムを自動生成する検査モデル生成装置を提供する。【解決手段】モデル検査プログラムを生成する際に用いる記述言語の変換ルールを保持する変換ルール部と、ソフトウェアの動作仕様を表し、遷移前状態と遷移後状態とで規定される遷移及びその遷移を起こすイベントを含む状態遷移仕様、動作仕様の検査条件を記述する検査式及び外部環境変数を入力し、検査式及び外部環境変数を解析して、状態遷移仕様に対して縮約処理を施して変換状態遷移仕様に変換するとともに、変換ルールを用いて、変換状態遷移仕様に基づいてモデル検査プログラムを生成するコード変換器とを備え、コード変換器は、イベントがランダムに発生し、且つ検査式にイベントが入っていなければ、イベントを全て削除して変換状態遷移仕様を生成する検査モデル生成装置。【選択図】図２
2014134965.tif 000002
【特許請求の範囲】
【請求項１】
モデル検査プログラムを生成する際に用いる記述言語の変換ルールを保持する変換ルール部と、
ソフトウェアの動作仕様を表し、遷移前状態と遷移後状態とで規定される遷移及びその遷移を起こすイベントを含む状態遷移仕様、前記動作仕様の検査条件を記述する検査式及び外部環境変数を入力し、前記検査式及び外部環境変数を解析して、前記状態遷移仕様に対して縮約処理を施して変換状態遷移仕様に変換するとともに、前記変換ルールを用いて、前記変換状態遷移仕様に基づいてモデル検査プログラムを生成するコード変換器とを備え、
前記コード変換器は、前記イベントがランダムに発生し、且つ前記検査式に前記イベントが入っていなければ、前記イベントを全て削除して前記変換状態遷移仕様を生成する検査モデル生成装置。
【請求項２】
前記状態遷移仕様、検査式及び外部環境変数を入力する入力部と、
入力した前記状態遷移仕様、検査式及び外部環境変数を保持する第１のメモリと、
前記変換状態遷移仕様を保持する第２のメモリとを備える請求項１記載の検査モデル生成装置。
【請求項３】
前記コード変換器は、前記イベントがランダムに発生し、前記検査式に前記イベントが入っていれば当該イベントを残し、前記検査式に入っていない残りの前記イベントを削除して前記変換状態遷移仕様を生成する請求項１又は請求項２記載の検査モデル生成装置。
【請求項４】
前記コード変換器は、前記検査式に前記イベントは入っていないが、前記イベントが外部変数の状態によって発生する場合には、前記イベントは全て削除するが当該イベント発生条件を残して前記変換状態遷移仕様を生成することを特徴とする請求項１又は請求項２記載の検査モデル生成装置。
【請求項５】
前記モデル検査プログラムは、前記検査式に前記イベントが含まれていない場合に、状態のみで構成され遷移行で展開する請求項１又は請求項２記載の検査モデル生成装置。
【請求項６】
前記モデル検査プログラムは、前記検査式にある前記イベントのみを記述し、遷移列を展開した後、イベント無しの遷移行の状態を展開する請求項３記載の検査モデル生成装置。
【請求項７】
前記モデル検査プログラムは、前記イベントの外部環境変数の発生条件のみを残し、前記イベントの発生条件を記述して遷移列を展開した後、前記イベント無しの遷移行の状態を展開する請求項４記載の検査モデル生成装置。
【請求項８】
前記変換状態遷移仕様は、前記状態遷移仕様を元にして、前記イベントを全て削除し、状態遷移先のOR状態を左詰めで記述したものである請求項１記載の検査モデル生成装置。
【請求項９】
前記変換状態遷移仕様は、前記状態遷移仕様を元にして、前記イベントの列だけ残し、前記検査式に含まれていないイベントについては削除し、削除した前記イベントについては、遷移先状態のORをとってランダムに遷移させるとともに、削除した前記イベントにはNULLを一律設定する請求項３記載の検査モデル生成装置。
【請求項１０】
前記変換状態遷移仕様は、前記状態遷移仕様を元にして、発生条件が無く削除する前記イベントに対しては、遷移先状態のORをとってランダムに遷移する請求項４記載の検査モデル生成装置。
【請求項１１】
前記外部環境変数は、状態の遷移に関わるアクションである請求項１乃至請求項１０のいずれか１項に記載の検査モデル生成装置。
【請求項１２】
前記モデル検査プログラムは、モデル検査ツールであるＳＰＩＮ（商標）用である請求項１乃至請求項１１のいずれか１項に記載の検査モデル生成装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明の実施形態は、検査モデル生成装置に関する。
【背景技術】
【０００２】
ソフトウェアが複雑化してきたことにより、ソフトウェア自体のみならずソフトウェア作成の基となるシステム仕様にこれまで以上に誤りが混入しやすくなっている。更に人の手では、システム仕様を網羅した検査が困難になってきている。
【０００３】
その解決法として，形式的手法の一つであるモデル検査が着目されている。 モデル検査によって、人の手では発見しづらい不適合な事例の発見に効果を挙げている。
【０００４】
しかし、モデル検査を行うには検査用のコードを記述する必要がある。検査者がシステム仕様のコード化を手作業で行う場合、時間がかかる上、ミスが混入しやすくなり、検査モデルそのものの信頼性が下がる可能性があった。
【０００５】
一方、システム仕様から機械的に検査モデルを作成すると、検査時に状態爆発が発生し、検査が収束しないことが多いという問題があった。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２００７−１１６０５号公報
【特許文献２】特開２０１０−１４００８４号公報
【特許文献３】特開平３−１９０８６号公報
【発明の概要】
【発明が解決しようとする課題】
【０００７】
本発明が解決しようとする課題は、状態爆発を抑える観点からイベント発生を抑制したモデル検査プログラムを自動生成する検査モデル生成装置を提供することである。
【課題を解決するための手段】
【０００８】
実施形態の検査モデル生成装置は、モデル検査プログラムを生成する際に用いる記述言語の変換ルールを保持する変換ルール部と、ソフトウェアの動作仕様を表し、遷移前状態と遷移後状態とで規定される遷移及びその遷移を起こすイベントを含む状態遷移仕様、前記動作仕様の検査条件を記述する検査式及び外部環境変数を入力し、前記検査式及び外部環境変数を解析して、前記状態遷移仕様に対して縮約処理を施して変換状態遷移仕様に変換するとともに、前記変換ルールを用いて、前記変換状態遷移仕様に基づいてモデル検査プログラムを生成するコード変換器とを備え、前記コード変換器は、前記イベントがランダムに発生し、且つ前記検査式に前記イベントが入っていなければ、前記イベントを全て削除して前記変換状態遷移仕様を生成する。
【図面の簡単な説明】
【０００９】
【図１】一般的なモデル検査器によるモデル検査の概要を模式的に示した図である。
【図２】本発明の実施形態に係る検査モデル生成装置の概略構成を示すブロック図である。
【図３】実施形態に係る検査モデル生成装置におけるモデル検査プログラムの生成処理の流れを示すフローチャートである。
【図４】状態遷移表の一例とイベント削除処理後の変換後の状態遷移表を示す図である。
【図５】状態遷移図の一例とイベント削除処理後の変換後の状態遷移図を示す図である。
【図６】状態遷移表の一例と特定イベント以外を削除処理後の変換後の状態遷移表を示す図である。
【図７】状態遷移図の一例と特定イベント以外を削除処理後の変換後の状態遷移図を示す図である。
【図８】状態遷移表の一例とイベント発生条件を残した変換後の状態遷移表を示す図である。
【図９】状態遷移図の一例とイベント発生条件を残した変換後の状態遷移図を示す図である。
【図１０】検査モデル生成アルゴリズムの流れを示すフローチャートである。
【図１１】本実施形態による縮約を施す前の状態遷移仕様の一例を表す図である。
【図１２】第１の実施形態に係る変換状態遷移仕様を表す図である。
【図１３】第１の実施形態における処理をPromela言語で記述した一例を示す図である。
【図１４】第２の実施形態に係る変換状態遷移仕様を表す図である。
【図１５】第２の実施形態における処理をPromela言語で記述した一例を示す図である。
【図１６】第３の実施形態による縮約を施す前の状態遷移仕様の一例を表す図である。
【図１７】第３の実施形態に係る変換状態遷移仕様を表す図である。
【図１８】第３の実施形態における処理をPromela言語で記述した一例を示す図である。
【図１９】第１の実施形態によって生成したモデル検査プログラムを用いてモデル検査を行った場合の縮約効果を説明する図である。
【発明を実施するための形態】
【００１０】
以下、本発明の一実施の形態について、図面を参照して説明する。尚、各図において同一箇所については同一の符号を付すとともに、重複した説明は省略する。
【００１１】
まず、本実施形態で用いる主要な用語について説明する。
【００１２】
「システム仕様」は、状態遷移モデルとして表現することが可能であり、システムがとりうる状態と、状態を遷移させるイベントやガード条件によって表すことができる。
【００１３】
「イベント」とは、遷移をもたらす外的刺激や内的変化などを表し、入力とも事象とも表現される。一つのイベントは一つの遷移を決定するが、それらはイベント発生時の状態によって変化する。
【００１４】
「アクション」とは、遷移の結果生じる分析が可能な対象物を意味し、出力とも表現される。アクションと遷移後の状態は区別される。
【００１５】
「状態爆発」とは、状態の数が膨大となって検査不能となることである。
【００１６】
図１は、一般的なモデル検査器によるモデル検査の概要を模式的に示した図である。状態遷移モデルは、所定のモデル記述言語によってモデル検査プログラム（モデルデータ）として記述することが可能であり、このモデル検査プログラムが検査対象としてモデル検査器に入力される。
【００１７】
一方、システムの仕様が所定の検査条件を満たすか否かを判定するための検査条件は、所定の言語で記述した検査式としてモデル検査器に入力される。
【００１８】
モデル検査器では、モデル検査プログラムが取りうる総ての状態遷移の組み合わせに対して、検査式を満たすか否かを判定する。検査式を満たさない状態が発見された場合は、その状態が反例としてモデル検査器から出力される。また、その状態へ至る過程もログデータをして出力される。反例を解析することによって、システムの仕様の修正の検討を行い、修正する。
【００１９】
モデル検査では状態遷移の組み合わせをしらみつぶしに網羅的に検索して検査条件を満たすか否かを判定する。
【００２０】
本実施形態においては、検査式に着目し、検査式にイベントが関係していなかったらイベントそのものを削除して状態のみでモデルを作成するものである。検査式にイベントが入っていても縮約可能である。
【００２１】
図２は、本発明の実施形態に係る検査モデル生成装置の概略構成を示すブロック図である。この装置は汎用のコンピュータ（例えばパーソナルコンピュータ（ＰＣ）等）と、同コンピュータ上で動作するソフトウェアとを用いて実現される。コンピュータとしては、ＣＡＤ（Computer Aided Design）やＣＡＥ（Computer Aided Engineering）に好適なエンジニアリングワークステーション（ＥＷＳ）等も含む。本実施形態はこのようなコンピュータに、状態遷移仕様の変換、モデル検査プログラムの生成に係る一連の手続きを実行させるプログラムとして実施することもできる。
【００２２】
図２に示すように、本実施形態に係る検査モデル生成装置は、主として、入力部１１、第１のメモリ１２、コード変換器１３、第２のメモリ１４、変換ルール部１５から構成されている。
【００２３】
入力部１１は、状態遷移仕様（状態遷移モデル）や検査に用いる外部環境変数等の情報、検査式を入力する。入力した状態遷移仕様、外部環境変数及び検査式は、第１のメモリ１２に保持される。第１のメモリ１２に保持した状態遷移仕様、外部環境変数及び検査式はコード変換器１３によって参照される。
【００２４】
コード変換器１３は、検査式及び外部環境変数を解析して、状態遷移仕様に対して縮約処理を施して変換状態遷移仕様に変換する。ここで、変換状態遷移仕様とは、本実施形態に係る検査式中のイベントの有無に着目した縮約処理を施した状態遷移仕様である。イベントの有無に着目した縮約処理の詳細は後述する。変換状態遷移仕様は、一旦、第２のメモリ１４に保持される。
【００２５】
さらに、コード変換器１３は、変換ルール部１５に保持した検査モデル記述言語変換ルールを用いて、変換状態遷移仕様に基づいてモデル検査プログラムを生成する。生成されたモデル検査プログラムは、公知のモデル検査器（図示しない）で実行される。
【００２６】
変換ルール部１５は、変換状態遷移仕様に基づいてモデル検査プログラムを生成する際に用いる記述言語の変換ルールを保持する。この変換ルールは公知のものを利用出来、コード変換器１３にて参照される。
【００２７】
次に、以上のように構成された検査モデル生成装置１００におけるモデル検査プログラムの生成処理の流れについて説明する。
【００２８】
図３は、実施形態に係る検査モデル生成装置１００におけるモデル検査プログラムの生成処理の流れを示すフローチャートである。ここでは、生成処理の概要を述べ、処理の詳細は後述する。
【００２９】
まず、入力部１１を介して、状態遷移、遷移の情報、検査式を入力する（ステップＳ３１）。次いで、イベントがランダムに発生するか否かを判定する（ステップＳ３２）。
【００３０】
イベントがランダムな発生であれば（ステップＳ３２でＹｅｓ）、検査式にイベントが入っているかを判定する（ステップＳ３３）。
【００３１】
イベントがランダムな発生でなければ（ステップＳ３２でＮｏ）、イベントの発生条件を状態遷移表のイベント名欄に付随して記述する（ステップＳ３４）。ここでは、イベントの発生が外部環境変数の状態によって定まるような場合は、外部環境変数のみを残している。イベント発生条件を記述した後、ステップＳ３３に移行する。
【００３２】
検査式にイベントが入っていれば（ステップＳ３３でＹｅｓ）、検査式に入っているイベントの列を左詰めに寄せ、検査式に入っていない残りのイベントの遷移元状態のORを左詰めで書いた変換状態遷移仕様を生成する（ステップＳ３５）。
【００３３】
次いで、変換状態遷移仕様からイベントの入っている列を読み取り、その列の遷移に対して特定のイベントが発生したことを示す検査モデルを作成する（ステップＳ３６）。
【００３４】
次いで、検査式に入っているイベント以外は、イベントにNULLを設定して、遷移元状態をランダムまたはイベント発生条件に従って遷移する検査モデルを作成する（ステップＳ３７）。ステップＳ３５〜Ｓ３７では、検査式にイベントが入っている場合、検査式に入っている全てのイベントを残し、それ以外のイベントを全て削除した検査モデルを作成している。
【００３５】
一方、検査式にイベントが入っていなければ（ステップＳ３３でＮｏ）、イベントを全て削除し、遷移元状態のORを左詰めで書いた変換状態遷移仕様を生成する（ステップＳ３８）。
【００３６】
次いで、変換状態遷移仕様の行を読み取り、遷移元状態から遷移先にランダムまたはイベント発生条件に従って遷移する検査モデルを作成する（ステップＳ３９）。
【００３７】
＜縮約アルゴリズム＞
次に、イベントの削減の場合のアルゴリズムについて詳述する。
【００３８】
図４（ａ）は、状態遷移表の一例を示す図である。状態遷移表の一番左の列には、状態遷移モデルに現れる遷移前の状態が配列される。図４（ａ）の例では、４つの状態Ｓ１、Ｓ２、Ｓ３、Ｓ４が配列されている。
【００３９】
一方、状態遷移表の一番上の行には、状態遷移モデルにおいて遷移を引き起こすイベントが配列される。図４（ａ）の例では、４つのイベントＥ１、Ｅ２、Ｅ３、Ｅ４、Ｅ５が配列されている。
【００４０】
状態遷移表の中央部のマスには遷移後の状態が配列される。また、斜線で示したマスは状態の遷移が起こらないことを示している。いま、状態Ｓｎから状態Ｓｍへの遷移を、（Ｓｎ→Ｓｍ）のように記載すると、図４（ａ）に例示する状態遷移表は、イベントＥ１によって、（Ｓ１→Ｓ４）、（Ｓ２→Ｓ３）、及び（Ｓ４→Ｓ２）の３つの遷移が起こることを示している。
【００４１】
同様に、イベントＥ２によって（Ｓ２→Ｓ１）及び（Ｓ３→Ｓ１）の２つの遷移が起こることを示している。イベントＥ３によって（Ｓ２→Ｓ１）及び（Ｓ３→Ｓ１）の２つの遷移が起こることを示している。イベントＥ４によって（Ｓ１→Ｓ４）及び（Ｓ４→Ｓ２）の２つの遷移が起こることを示している。イベントＥ５によって、（Ｓ２→Ｓ１）、（Ｓ３→Ｓ１）、及び（Ｓ４→Ｓ２）の３つの遷移が起こることを示している。
【００４２】
＜第１の実施形態のアルゴリズム＞
まず、第１の実施形態のアルゴリズムについて説明する。第１の実施形態は、検査式にイベントが入っていない場合の縮約である。
【００４３】
例えば、「いつかS4に到達する」との検査式では、イベントが入っていない。イベントがランダムであるならば、状態が遷移する可能性のある状態にランダムに遷移させても結果は同じである。
【００４４】
そこで、イベントを全て削除し、状態遷移先のOR状態を左詰めで記述した状態遷移表を作成する。モデル検査は、内部的には変数の値の組み合わせで状態の網羅を行うため、イベントによる変数が削減できると内部状態も削減できる。
【００４５】
図４（ｂ）は、図４（ａ）に示す状態遷移表の例に対して、イベント削除処理後の変換後の状態遷移表を示す図である。図４（ｂ）では、イベントとは無関係な遷移（状態Ｓ１→Ｓ４）、遷移（状態Ｓ２→Ｓ３）及び遷移（状態Ｓ２→Ｓ１）、遷移（状態Ｓ３→Ｓ１）、遷移（状態Ｓ４→Ｓ２）に縮約されている。
【００４６】
図５（ａ）は、状態遷移表に対応する状態遷移モデルを状態遷移図の形式で表現したものであり、状態Ｓ１、Ｓ２、Ｓ３、Ｓ４の遷移の方向が、矢印をもつパスで示され、遷移を起こす各イベントＥ１〜Ｅ５が各パスに付されている。
【００４７】
一方、図５（ｂ）は、イベント削除後の状態遷移モデルを状態遷移図の形式で表現したもので、状態のみをランダムに遷移させていくことを示している。
【００４８】
モデル検査において、イベントがランダムに発生し、かつイベントが検査式に入っていないのであれば、状態のみをランダムに遷移させていけばよい。
【００４９】
＜第２の実施形態のアルゴリズム＞
次に、第２の実施形態のアルゴリズムについて説明する。第２の実施形態は、検査式にイベントが入っている場合の縮約である。
【００５０】
図６（ａ）は、状態遷移表の一例を示す図である。図６（ｂ）は、図６（ａ）に示す状態遷移表の例に対して、特定イベント以外を削除処理後の変換後の状態遷移表を示す図である。
【００５１】
例えば、「イベントE1が発生したら、いつかS4に到達する」との検査式では、イベントが入っている。このような場合には、イベントE1の列だけ残し、E1が発生した場合の遷移は通常通り記述する。E1以外のイベントについては削除し、削除したイベントについては、遷移先状態のORをとってランダムに遷移させる。削除したイベントにはNULLを一律設定する。
【００５２】
図７（ａ）は、状態遷移表に対応する状態遷移モデルを状態遷移図の形式で表現したものである。状態Ｓ１、Ｓ２、Ｓ３、Ｓ４の遷移の方向が、矢印をもつパスで示され、遷移を起こす各イベントＥ１〜Ｅ５が各パスに付されている。
【００５３】
一方、図７（ｂ）は、特定イベント以外のイベントを削除後の状態遷移モデルを状態遷移図の形式で表現したものである。イベントE1が発生したことだけがわかればよいので、イベントE1だけ残して、残りの状態をランダムに遷移させていけばよいことを示している。
【００５４】
モデル検査は、内部的には変数の値の組み合わせで状態の網羅を行うため、イベントによる変数が削減できると内部状態も削減できる。
【００５５】
＜第３の実施形態のアルゴリズム＞
次に、第３の実施形態のアルゴリズムについて説明する。第３の実施形態は、イベントが外部変数の状態によって発生する場合の縮約である。
【００５６】
検査式にイベントは入っていないが、イベントが外部変数の状態によって発生する場合には、イベントは全て削除するがイベント発生条件を残す処理をする。
【００５７】
図８（ａ）は、状態遷移表の一例を示す図である。図８（ｂ）は、図８（ａ）に示す状態遷移表の例に対して、イベント発生条件を残した変換後の状態遷移表を示す図である。
【００５８】
図８（ｂ）によれば、発生条件の無い削除イベントに対しては、遷移先状態のORをとってランダムに遷移することを示している。
【００５９】
図９（ａ）は、状態遷移表に対応する状態遷移モデルを状態遷移図の形式で表現したものであり、状態Ｓ１、Ｓ２、Ｓ３、Ｓ４の遷移の方向が、矢印をもつパスで示され、遷移を起こす各イベントＥ１〜Ｅ５が各パスに付されている。
【００６０】
一方、図９（ｂ）は、イベント発生条件を残した状態遷移モデルを状態遷移図の形式で表現したもので、イベント発生条件が存在するので、イベントが発生条件を遷移のガード条件として残し、ガード条件のない遷移をランダムに遷移させていけばよいことを示している。
【００６１】
モデル検査は、内部的には変数の値の組み合わせで状態の網羅を行うため、発生条件を残してイベントによる変数が削減できると内部状態も削減できる。
【００６２】
＜検査モデル生成アルゴリズム＞
次に、変換状態遷移仕様からの検査モデル生成アルゴリズムについて説明する。モデル検査のためのツールとしては、オートマトンベースのモデルチェッカであるＳＰＩＮ（商標）を利用することができる。ＳＰＩＮでは、検査対象と検査式を二つのオートマトンに変換し、この二つのオートマトンに積集合があるか否かを計算する。ＳＰＩＮは、Promelaという専用言語で記述された検査モデルプログラムを実行して検査する。
【００６３】
図１０は、検査モデル生成アルゴリズムの流れを示すフローチャートである。図１０に示すアルゴリズムは、Promelaによる記述によって表している。
【００６４】
まず、[プロセス1 () { if]を記述する（ステップＳ１００１）。
【００６５】
次いで、変換状態遷移仕様から遷移元状態列を読み込む（ステップＳ１００２）。
【００６６】
次に、変換状態遷移仕様から遷移列を読み込む（ステップＳ１００３）。
【００６７】
次いで、遷移列にイベント又はイベント発生条件が定義されているか否かを判定する
（ステップＳ１００４）。
【００６８】
イベント又はイベント発生条件が定義されていなければ（ステップＳ１００４でＮｏ）、イベントが記述されている列以外の遷移行を読み込む（ステップＳ１００５）。
【００６９】
次いで、変換状態遷移仕様上に遷移イベントが１つも定義されていないか否かを判定する（ステップＳ１００６）。
【００７０】
定義されていなければ（ステップＳ１００６でＹｅｓ）、
[::state == 遷移元状態->
atomic () { if]  を記述（ステップＳ１００７）した後、
[::state= 遷移先状態 
アクション;]  を記述する（ステップＳ１００８）。
【００７１】
一方、定義されていれば（ステップＳ１００６でＮｏ）、
[::state == 遷移元状態->
EVENT = NULL
atomic () { if]  を記述（ステップＳ１０１２）した後、ステップＳ１００８に移行する。
【００７２】
ステップＳ１００８の後、遷移行の全ての遷移先を記述したか否かを判定する（ステップＳ１００９）。
【００７３】
遷移行の全ての遷移先を記述したら（ステップＳ１００９でＹｅｓ）、fi;} を記述（ステップＳ１０１０）し、全ての遷移先を読み込んだか否かを判定する（ステップＳ１０１１）。
【００７４】
遷移行の全ての遷移先を記述していなければ（ステップＳ１００９でＮｏ）、ステップＳ１００８に戻る。
【００７５】
全ての遷移先を読み込んでなければ（ステップＳ１０１１でＮｏ）ステップＳ１００５に戻り、全ての遷移先を読み込んでいれば（ステップＳ１０１１でＹｅｓ）ステップＳ１０２１に移行する。
【００７６】
一方、イベント又はイベント発生条件が定義されていれば（ステップＳ１００４でＹｅｓ）、イベントがあるか否かを判定する（ステップＳ１０１３）。イベントがあれば（ステップＳ１０１３でＹｅｓ）、
[::EVENT = イベント名
atomic () {if]を記述する（ステップＳ１０１４）。
【００７７】
次いで、発生条件があるか否かを判定する（ステップＳ１０１５）。尚、イベントがなければ（ステップＳ１０１３でＮｏ）、ステップＳ１０１５に移行する。
【００７８】
発生条件があれば（ステップＳ１０１５でＹｅｓ）、
[:: if   発生条件 ->
Atomic () {if]  を記述する（ステップＳ１０１６）。
【００７９】
次いで、::state== 遷移元状態 ->
アクション;
state = 遷移先;」を記述する（ステップＳ１０１７）。尚、発生条件がなければ（ステップＳ１０１５でＮｏ）、ステップＳ１０１７する。
【００８０】
次に、遷移列の全ての遷移先を記述したか否かを判定する（ステップＳ１０１８）。遷移列の全ての遷移先を記述していれば（ステップＳ１０１８でＹｅｓ）、fi;}  を記述する（ステップＳ１０１９）。遷移列の全ての遷移先を記述していなければ（ステップＳ１０１８でＮｏ）、ステップＳ１０１７に戻る。
【００８１】
次に、全ての遷移列を読み込んだか否かを判定する（ステップＳ１０２０）。全ての遷移列を読み込んでいれば（ステップＳ１０２０でＹｅｓ）、[fi;}]を記述（ステップＳ１０２１）して、検査モデルの生成を終了する。全ての遷移列を読み込んでいなければ（ステップＳ１０２０でＮｏ）、ステップＳ１００３に戻る。
【００８２】
以上を受けて、各実施形態を詳述する。
【００８３】
まず、図１１は、本実施形態による縮約を施す前の状態遷移仕様の一例を表す図である。
【００８４】
図１１に示す状態遷移仕様において、一番左の列には、INIT、HUNGRY、FULL、TIRED、INBEDの各状態が配列されている。また、一番上の行には、遷移を引き起こすEAT1、SLEEP1、PLAY1、WAKE1のイベントが配列されている。
【００８５】
図１１に示す状態遷移仕様によれば、イベントEAT1によって遷移（INIT→FULL）が起こり、イベントSLEEP1によって遷移（INIT→INBED ）が起こり、イベントPLAY1によって遷移（INIT→TIRED ）が起こる。またイベントEAT1によって遷移（HUNGRY →FULL）が起こる。さらに、イベントSLEEP1によって遷移（FULL →INBED ）が起こり、イベントPLAY1によって遷移（FULL →HUNGRY ）が起こる。また、イベントEAT1によって遷移（TIRED →FULL）が起こり、イベントSLEEP1によって遷移（TIRED →INBED ）が起こり、イベントPLAY1によって遷移（TIRED →HUNGRY ）が起こる。さらに、イベントWAKE1によって遷移（INBED →INIT  ）が起こる。
【００８６】
＜第１の実施形態の場合＞
例えば、図１１に示す状態遷移仕様において、検査式が「いつか状態がHUNGRYになるならば、いつか状態がFULLになる」の場合である。第１の実施形態では、イベントを削除して、遷移先状態のORを左詰めで並べた変換状態遷移仕様を作成する。図１２は、第１の実施形態に係る変換状態遷移仕様を表す図である。図１２に示す変換状態遷移仕様によれば、イベント名欄が空白となっており、遷移先が左に詰められている。
【００８７】
図１３は、第１の実施形態における処理をPromela言語で記述した一例を示す図である。図１３では、「いつかプロセス１の状態がHUNGRYになるならば、いつかプロセス１の状態がFULLになる」との検査条件に対応して、生成されるLTL(Linear Temporal logic)式にイベント名が使用されていない。第１の実施形態では、状態遷移表は状態のみで構成され遷移行で展開される結果、状態INITから状態FULL、INBED、 TIREDのいずれかがランダムに起こるルーチンとなっている。
【００８８】
＜第２の実施形態の場合＞
例えば、図１１に示す状態遷移仕様において、検査式が「いつかイベントがEAT1になるならば、いつか状態がFULLになる」の場合である。第２の実施形態では、イベントEAT1の列だけ左詰めで残し、その他の遷移先状態をORで左詰めで並べた変換状態遷移仕様を作成する。図１４は、第２の実施形態に係る変換状態遷移仕様を表す図である。図１４に示す変換状態遷移仕様によれば、イベントEAT1以外のイベント名欄が空白となっており、遷移先が左に詰められている。
【００８９】
図１５は、第２の実施形態における処理をPromela言語で記述した一例を示す図である。図１５では、「いつかプロセス1のイベントがEAT1になるならば、いつかプロセス1の状態がFULLになる」との検査条件に対応して、生成されるLTL式にイベント名が使用されている。第２の実施形態では、状態遷移表に必要なイベントのみを残す結果、検査式に含まれているイベントのみを記述し、遷移列を展開した後、イベント無しの遷移行の状態を展開するルーチンとなっている。
【００９０】
＜第３の実施形態の場合＞
まず、図１６は、第３の実施形態による縮約を施す前の状態遷移仕様の一例を表す図である。図１６に示す状態遷移仕様において、イベントSLEEP1には、イベントSLEEP = flag1 && flag2 という条件で発生するとの条件が付されている。
【００９１】
例えば、図１６に示す状態遷移仕様において、検査式が「いつか状態がHUNGRYになるならばいつか状態がFULLになる」の場合である。第３の実施形態では、イベントSLEEPの列を左詰めで残し、その他の遷移先状態をORで左詰めで並べた変換状態遷移仕様を作成する。図１７は、第３の実施形態に係る変換状態遷移仕様を表す図である。図１７に示す変換状態遷移仕様によれば、発生条件の付いたイベント名欄が左詰めされ、それ以外の遷移先が続いて左に詰められている。
【００９２】
図１８は、第３の実施形態における処理をPromela言語で記述した一例を示す図である。図１８では、「いつかプロセス1のイベントがEAT1になるならば、いつかプロセス1の状態がFULLになる」との検査条件に対応して、生成されるLTL式にはイベントに発生条件が付されている。第３の実施形態では、イベントの外部環境変数の発生条件のみを残す結果、イベントの発生条件を記述して遷移列を展開した後、イベント無しの遷移行の状態を展開するルーチンとなっている。
【００９３】
以上説明したように、本実施形態によれば、イベントの発生を抑制することによりモデル検査時における状態爆発を発生させる可能性を低減し、イベントを削除しても反例を出力することができる。
【００９４】
図１９は、第１の実施形態によって生成したモデル検査プログラムを用いてモデル検査を行った場合の縮約効果を説明する図である。ここでは、比較のため、特許文献３における縮約を“既存縮約”と称している。
【００９５】
図１９に示す例では、縮約前の状態遷移がイベント数：３９個、状態数：７個、遷移数：１５５個であった。イベントを全て削除する縮約の結果、モデル検査実施時の探索範囲とメモリ消費量は、大幅に削減されている。ＳＰＩＮ内の状態数は既存縮約の場合から９８％削減され、探索の深さは既存縮約の場合から９６％削減され、メモリ消費量は既存縮約の場合から９０％削減されている。さらに、モデル検査に要する検査時間も著しく減少している。
【００９６】
本発明のいくつかの実施形態を説明したが、これらの実施形態は、例として提示したものであり、発明の範囲を限定することは意図していない。これら新規な実施形態は、その他の様々な形態で実施されることが可能であり、発明の要旨を逸脱しない範囲で、種々の省略、置き換え、変更を行うことができる。これら実施形態やその変形は、発明の範囲や要旨に含まれるとともに、特許請求の範囲に記載された発明とその均等の範囲に含まれる。
【符号の説明】
【００９７】
１００・・・検査モデル生成装置
１１・・・入力部
１２・・・第１のメモリ
１３・・・コード変換器
１４・・・第２のメモリ
１５・・・変換ルール部
【図１】
2014134965.tif 000003
【図２】
2014134965.tif 000004
【図３】
2014134965.tif 000005
【図４】
2014134965.tif 000006
【図５】
2014134965.tif 000007
【図６】
2014134965.tif 000008
【図７】
2014134965.tif 000009
【図８】
2014134965.tif 000010
【図９】
2014134965.tif 000011
【図１０】
2014134965.tif 000012
【図１１】
2014134965.tif 000013
【図１２】
2014134965.tif 000014
【図１３】
2014134965.tif 000015
【図１４】
2014134965.tif 000016
【図１５】
2014134965.tif 000017
【図１６】
2014134965.tif 000018
【図１７】
2014134965.tif 000019
【図１８】
2014134965.tif 000020
【図１９】
2014134965.tif 000021