(57)【要約】【課題】状態遷移モデルと検査条件とから、モデル検査時における状態爆発の発生を低減し、検査条件に応じた最適な状態遷移モデルを生成可能なモデル検査装置を提供する。【解決手段】本発明に係るモデル検査装置は、検査対象コードを入力するコード入力部と、検査変数が記述される検査式を入力する検査式入力部と、処理コードの実行によって検査変数の値を変化させない場合は、その処理コードを除去し、処理コードが検査変数を求めるコードである場合は、その処理コードをそのまま残し、処理コードが検査変数の値を変化させる検査依存変数を求めるコードである場合は、その処理コードを実行非検査コードとし、連続する実行非検査コードを一括で実行させると共に実行非検査コードごとの検査を省略させる不可分命令を付加する、ことにより、検査対象コードを最適検査コードに変換する最適化コード変換部とを備えたことを特徴とする。【選択図】  図４
2010140335.tif 000002
【特許請求の範囲】
【請求項１】
変数に対する一連の処理が処理コードの一連の系列として記述されるプロセスのコードを検査対象コードとして入力するコード入力部と、
前記検査対象コードに対する検査条件と検査の対象となる検査変数とが記述される検査式を入力する検査式入力部と、
（ａ）前記処理コードの実行によって前記検査変数の値を変化させない場合は、その処理コードを前記検査対象コードから除去し、
（ｂ）前記処理コードが、前記検査変数を求めるコードである場合は、その処理コードを実行検査コードとして前記検査対象コードにそのまま残し、
（ｃ）前記検査変数以外の変数であって、いずれかの処理コードの実行によって前記検査変数の値を変化させる変数を検査依存変数とし、前記処理コードが前記検査依存変数を求めるコードである場合は、その処理コードを実行非検査コードとし、連続する前記実行非検査コードを一括で実行させると共に前記実行非検査コードごとの検査を省略させる不可分命令を付加する、
ことにより、前記検査対象コードを最適検査コードに変換する最適化コード変換部と、
前記最適検査コードに対して前記検査式によるモデル検査を行うモデル検査部と、
を備えたことを特徴とするモデル検査装置。
【請求項２】
前記検査対象コードに含まれる変数の値が、その変数以外の他の変数によって変化する場合は、前記他の変数を前記変数に対する依存変数とし、前記検査対象コードに含まれる各変数に対して前記依存変数を関連付けた依存変数リスト、を生成するリスト生成部、
をさらに備え、
前記最適化コード変換部は、
前記検査式入力部から入力される前記検査式から前記検査変数を特定する一方、前記依存変数リストを参照し、特定した前記検査変数に関連付けられている前記依存変数を前記検査依存変数とする、
ことを特徴とする請求項１に記載のモデル検査装置。
【請求項３】
前記最適化コード変換部は、
前記実行非検査コードが、その実行非検査コードで求める検査依存変数を含む前記検査実行コードよりも前にあり、かつ、その実行非検査コードで求める検査依存変数を含まない前記検査実行コードよりも後にある場合は、その実行非検査コードを、前記検査依存変数を含まない前記検査実行コードよりも前に移動させる、
ことを特徴とする請求項１に記載のモデル検査装置。
【請求項４】
前記コード入力部は、実行順序が不定の複数のプロセスのコードを含む検査対象コードを入力し、
前記最適化コード変換部は、
（ａ）前記複数のプロセスのコードの中のどの処理コードの実行によっても前記検査変数の値を変化させない場合は、その処理コードを前記検査対象コードから除去し、
（ｂ）前記検査変数以外の変数であって、前記検査変数の値を変化させる変数を検査依存変数とするとき、ある１つのプロセス内の処理コードにおいて求める前記検査依存変数の値が他のプロセスの処理コードよって変化しない場合は、その検査依存変数を求める当該プロセス内の処理コードを実行非検査コードとし、連続する前記実行非検査コードを一括で実行させると共に前記実行非検査コードごとの検査を省略させる不可分命令を付加し、
（ｃ）ある１つのプロセス内の処理コードにおいて求めようとする前記検査依存変数の値が他のプロセスの処理コードよって変化する場合はその検査依存変数を特定検査依存変数とし、前記特定検査依存変数を求める当該プロセス内の処理コードも前記実行検査コードとして、前記検査対象コードにそのまま残す、
ことを特徴とする請求項１に記載のモデル検査装置。
【請求項５】
前記検査対象コードに含まれる変数の値が、その変数以外の他の変数によって変化する場合は、前記他の変数を前記変数に対する依存変数とし、前記検査対象コードに含まれる各変数に対して、少なくとも前記各変数に対する依存変数及び前記各変数を求めるプロセスとを関連付けた依存変数リスト、を生成するリスト生成部、
をさらに備え、
前記最適化コード変換部は、
前記検査式入力部から入力される前記検査式から前記検査変数を特定する一方、前記依存変数リストを参照して前記検査変数に対する前記依存変数を特定し、
特定した前記依存変数を求めるプロセスと異なる他のプロセスの処理コードによって、前記依存変数の値が変化しない場合は、その依存変数を前記検査依存変数とし、
特定した前記依存変数を求めるプロセスと異なる他のプロセスの処理コードによって、前記依存変数の値が変化する場合は、その依存変数を前記特定検査依存変数とする、
ことを特徴とする請求項４に記載のモデル検査装置。
【請求項６】
前記検査対象コードは、モデル検査ツールＳＰＩＮに対応する言語で記述されるコードである、
ことを特徴とする請求項１に記載のモデル検査装置。
【請求項７】
変数に対する一連の処理が処理コードの一連の系列として記述されるプロセスのコードを検査対象コードとし、
前記検査対象コードに対する検査条件と検査の対象となる検査変数とが記述される検査式を入力し、
（ａ）前記処理コードの実行によって前記検査変数の値を変化させない場合は、その処理コードを前記検査対象コードから除去し、
（ｂ）前記処理コードが、前記検査変数を求めるコードである場合は、その処理コードを実行検査コードとして前記検査対象コードにそのまま残し、
（ｃ）前記検査変数以外の変数であって、いずれかの処理コードの実行によって前記検査変数の値を変化させる変数を検査依存変数とし、
（ｄ）前記処理コードが前記検査依存変数を求めるコードである場合は、その処理コードを実行非検査コードとし、
（ｅ）連続する前記実行非検査コードを一括で実行させると共に前記実行非検査コードごとの検査を省略させる不可分命令を付加する、
という上記（ａ）から（ｅ）のステップにより、前記検査対象コードを最適検査コードに変換し、
前記最適検査コードに対して前記検査式によるモデル検査を行う、
ステップを備えたことを特徴とするモデル検査方法。
【請求項８】
前記検査対象コードに含まれる変数の値が、その変数以外の他の変数によって変化する場合は、前記他の変数を前記変数に対する依存変数とし、前記検査対象コードに含まれる各変数に対して前記依存変数を関連付けた依存変数リスト、を生成する、
ステップをさらに備え、
前記最適検査コードに変換するステップは、
前記検査式入力部から入力される前記検査式から前記検査変数を特定する一方、前記依存変数リストを参照し、特定した前記検査変数に関連付けられている前記依存変数を前記検査依存変数とする、
ステップをさらに備えることを特徴とする請求項７に記載のモデル検査方法。
【請求項９】
前記最適検査コードに変換するステップは、
前記実行非検査コードが、その実行非検査コードで求める検査依存変数を含む前記検査実行コードよりも前にあり、かつ、その実行非検査コードで求める検査依存変数を含まない前記検査実行コードよりも後にある場合は、その実行非検査コードを、前記検査依存変数を含まない前記検査実行コードよりも前に移動させる、
ステップをさらに備えることを特徴とする請求項７に記載のモデル検査方法。
【請求項１０】
前記検査対象コードを入力するステップでは、実行順序が不定の複数のプロセスのコードを含む検査対象コードを入力し、
前記最適検査コードに変換するステップでは、
（ａ）前記複数のプロセスのコードの中のどの処理コードの実行によっても前記検査変数の値を変化させない場合は、その処理コードを前記検査対象コードから除去し、
（ｂ）前記検査変数以外の変数であって、前記検査変数の値を変化させる変数を検査依存変数とするとき、ある１つのプロセス内の処理コードにおいて求める前記検査依存変数の値が他のプロセスの処理コードよって変化しない場合は、その検査依存変数を求める当該プロセス内の処理コードを実行非検査コードとし、連続する前記実行非検査コードを一括で実行させると共に前記実行非検査コードごとの検査を省略させる不可分命令を付加し、
（ｃ）ある１つのプロセス内の処理コードにおいて求める前記検査依存変数の値が他のプロセスの処理コードよって変化する場合はその検査依存変数を特定検査依存変数とし、前記特定検査依存変数を求める当該プロセス内の処理コードも前記実行検査コードとして、前記検査対象コードにそのまま残す、
ことを特徴とする請求項７に記載のモデル検査方法。
【請求項１１】
前記検査対象コードに含まれる変数の値が、その変数以外の他の変数によって変化する場合は、前記他の変数を前記変数に対する依存変数とし、前記検査対象コードに含まれる各変数に対して、少なくとも前記各変数に対する依存変数及び前記各変数を求めるプロセスとを関連付けた依存変数リスト、を生成する、
ステップをさらに備え、
前記最適検査コードに変換するステップでは、
前記検査式入力部から入力される前記検査式から前記検査変数を特定する一方、前記依存変数リストを参照して前記検査変数に対する前記依存変数を特定し、
特定した前記依存変数を求めるプロセスと異なる他のプロセスの処理コードによって、前記依存変数の値が変化しない場合は、その依存変数を前記検査依存変数とし、
特定した前記依存変数を求めるプロセスと異なる他のプロセスの処理コードによって、前記依存変数の値が変化する場合は、その依存変数を前記特定検査依存変数とする、
ことを特徴とする請求項１０に記載のモデル検査方法。
【請求項１２】
前記検査対象コードは、モデル検査ツールのＳＰＩＮに対応する言語で記述されるコードである、
ことを特徴とする請求項７に記載のモデル検査方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検査装置、及びモデル検査方法に係り、特に、状態遷移モデルとして表現可能な検査モデルを検査するモデル検査装置、及びモデル検査方法に関する。
【背景技術】
【０００２】
今日、ソフトウェア組み込み機器においては、ハードウェアの技術革新により、より複雑な制御や機能をもつソフトウェアを組み込もうとするニーズが高まってきている。組み込み機器においては、複数の機器が協調して動作する必要があり、各機器の状態とその遷移系列で表現されるシステム仕様に誤りや矛盾がないかを確認してシステムを構築する必要がある。
【０００３】
このような複雑な制御仕様において、記述したシステム仕様の正しさを検査するための方法として、モデル検査と呼ばれる手法がある。モデル検査では、システム仕様を状態遷移モデルとしてとらえ、考えうる総ての実行系列に対して、デッドロックの有無や、特定の条件下における到達状態や未到達状態の検査を行うことができる（特許文献１、２等参照）。
【特許文献１】特開昭６１−７１７５０号公報
【特許文献２】特開平０４−３６９９４９号公報
【発明の開示】
【発明が解決しようとする課題】
【０００４】
モデル検査の対象となる状態遷移モデルは、通常、仕様記述言語と呼ばれる特定のプログラム言語を用いた検査用コードとして作成される。作成された検査用コードは、検査時に状態探索木に展開されて検査の評価対象となる。この評価対象に対して所定の検査条件を満たすか否かが検査され、検査条件を満たさない場合には、そのときの具体的なふるまいを反例として出力する。出力された反例は通常人によって解析され、解析結果からシステム仕様の誤りを発見して訂正する。
【０００５】
しかしながら、モデル検査では総ての変数の変化を状態として取り扱うため、検査用コードが複雑で規模が大きい場合、状態探索木が膨大な大きさとなり、実質的に探索不可能となることがある。このような事象を状態爆発と呼んでいる。
【０００６】
また、複数のプロセスが平行して動作するシステムでは、プロセス間のステップ実行の任意の組み合わせも状態として考慮されるため、状態探索木はさらに大きくなり、状態爆発の問題はなかなか解消されない。
【０００７】
本発明は、上記事情に鑑みてなされたものであり、入力された状態遷移モデルと検査条件とから、モデル検査時における状態爆発の発生を低減し、検査条件に応じた最適な状態遷移モデルを生成することができるモデル検査装置、及びモデル検査方法を提供することを目的とする。
【課題を解決するための手段】
【０００８】
上記課題を解決するため、本発明に係るモデル検査装置は、変数に対する一連の処理が処理コードの一連の系列として記述されるプロセスのコードを検査対象コードとして入力するコード入力部と、前記検査対象コードに対する検査条件と検査の対象となる検査変数とが記述される検査式を入力する検査式入力部と、（ａ）前記処理コードの実行によって前記検査変数の値を変化させない場合は、その処理コードを前記検査対象コードから除去し、（ｂ）前記処理コードが、前記検査変数を求めるコードである場合は、その処理コードを実行検査コードとして前記検査対象コードにそのまま残し、（ｃ）前記検査変数以外の変数であって、いずれかの処理コードの実行によって前記検査変数の値を変化させる変数を検査依存変数とし、前記処理コードが前記検査依存変数を求めるコードである場合は、その処理コードを実行非検査コードとし、連続する前記実行非検査コードを一括で実行させると共に前記実行非検査コードごとの検査を省略させる不可分命令を付加する、ことにより、前記検査対象コードを最適検査コードに変換する最適化コード変換部と、前記最適検査コードに対して前記検査式によるモデル検査を行うモデル検査部と、を備えたことを特徴とする。
【０００９】
また、上記課題を解決するため、本発明に係るモデル検査方法は、変数に対する一連の処理が処理コードの一連の系列として記述されるプロセスのコードを検査対象コードとし、前記検査対象コードに対する検査条件と検査の対象となる検査変数とが記述される検査式を入力し、（ａ）前記処理コードの実行によって前記検査変数の値を変化させない場合は、その処理コードを前記検査対象コードから除去し、（ｂ）前記処理コードが、前記検査変数を求めるコードである場合は、その処理コードを実行検査コードとして前記検査対象コードにそのまま残し、（ｃ）前記検査変数以外の変数であって、いずれかの処理コードの実行によって前記検査変数の値を変化させる変数を検査依存変数とし、（ｄ）前記処理コードが前記検査依存変数を求めるコードである場合は、その処理コードを実行非検査コードとし、（ｅ）連続する前記実行非検査コードを一括で実行させると共に前記実行非検査コードごとの検査を省略させる不可分命令を付加する、という上記（ａ）から（ｅ）のステップにより、前記検査対象コードを最適検査コードに変換し、前記最適検査コードに対して前記検査式によるモデル検査を行う、ステップを備えたことを特徴とする。
【発明の効果】
【００１０】
本発明に係るモデル検査装置、及びモデル検査方法によれば、入力された状態遷移モデルと検査条件とから、モデル検査時における状態爆発の発生を低減し、検査条件に応じた最適な状態遷移モデルを生成することができる。
【発明を実施するための最良の形態】
【００１１】
本発明に係るモデル検査装置、及びモデル検査方法の実施形態について、添付図面を参照して説明する。
【００１２】
（１）概要
図１は、一般的なモデル検査装置の動作概念を模式的に示した図である。システム仕様は状態遷移モデルとして表現することが可能であり、システムがとりうる状態と、状態を変化させる（遷移させる）イベントによって表すことができる。状態遷移モデルは、所定のモデル記述言語によって検査対象コード（モデルデータ）として記述することが可能であり、この検査対象コード（モデルデータ）が検査対象としてモデル検査装置に入力される。
【００１３】
一方、システム仕様が所定の検査条件を満たすか否かを判定するための検査条件は、所定の言語で記述した検査式としてモデル検査装置に入力される。
【００１４】
モデル検査装置では、検査対象コードが取りうる総ての状態を状態探索木として展開し、検査式を満たさない状態の存在を検証する。検査式を満たさない状態が発見された場合は、その状態が反例としてモデル検査装置から出力される。また、その状態へ至る過程もログデータをして出力される。反例やログデータがモデル検査装置の検査結果となる。
【００１５】
図２（ａ）は、モデル検査装置に入力される検査対象コードの一例を示す図であり、図２（ｂ）は、この検査対象コードを状態遷移図（状態探索木）によって表現した図である。なお、図２（ａ）に例示する検査対象コードは、ＳＰＩＮと呼ばれるモデル検査ツールの記述言語を用いているコードである。以下の説明も主にＳＰＩＮの記述言語に基づいているが、本願発明に係る検査対象コードはＳＰＩＮの記述言語に限定されるものではない。
【００１６】
検査対象コードは、変数ｘ、ｙの宣言文と、プロセスコードを有している。プロセスコードは、変数ｘ、ｙに対する一連の処理に対応する一連の処理コードで記述されている。この場合、変数ｘ、ｙの値の組み合わせが状態であり、変数ｘ、ｙの値を変化させる処理コード（例えば、ｘ＝ｘ＋１等の演算式）の実行がイベントとなる。
【００１７】
本例では、変数ｘ、ｙの値の判定を行う処理コード（例えば、ｘ＜３等）もイベントとして扱っており、この判定処理によっても状態遷移が起こるものとして取り扱っている。
【００１８】
図２は、変数ｘ、ｙの初期値をゼロとし、変数ｘが３よりも小さいときは変数ｘに１を加算し続け、同様に変数ｙが２よりも小さいときは変数ｙに１を加算し続けるという簡単なプロセス１を例示している。
【００１９】
このプロセス１の場合、単純にそのまま状態遷移図に展開すると、図２（ｂ）に示したように状態数は１４となり、遷移数も１４となる。
【００２０】
ところで、一般に状態遷移モデル（或いは検査対象コード）を検査する場合、ある特定の変数に注目し、この変数の振る舞いが所定の検査条件を満たすか否かを判定することがほとんどである。この場合、検査の対象となる変数（以下、検査変数という）の値の変化だけを検査すれば十分である。
【００２１】
図３は、上記の考え方に基づいて状態遷移モデルが縮小される様子を示している。ここでは、検査条件として変数ｙの値を検査する検査式が与えられたと仮定している（即ち、検査変数はｙ）。検査変数がｙの場合、変数ｘが検査変数ｙに影響を与えないのであれば、変数ｘの状態遷移の状況をいちいち検査しても意味がない。
【００２２】
このような場合、変数ｘに関する複数の処理をまとめて一括で実行させ、この一括実行を１つの状態遷移と捉えるとすると、状態と遷移の数を削減することができる。モデル記述言語の多くは、個々の処理コードによる状態遷移を発生させることなく複数の処理コードを一括で実行させるための命令を有しており、ここではこの命令を不可分命令と呼ぶものとする。
【００２３】
例えば、ＳＰＩＮでは、atomic命令と呼ばれる不可分命令をもっている。”atomic {“と、”}”とで囲った中にある複数の処理コードは一括で実行されるが、各処理コードが個々の状態遷移に展開されることはない。
【００２４】
不可分命令の対象となる各処理コード（例えば、図３（ａ）における、ｘ＝ｘ＋１）は、実行のみが行われ、状態遷移に展開しての検査は行われないため、以下、「実行非検査コード」と呼ぶものとする。
【００２５】
これに対して、図３（ａ）における、ｙ＝ｙ＋１のような処理コードは、実行されると共に、変数ｙの変化毎に状態遷移に展開されて検査される処理コードであり、以下、「実行検査コード」と呼ぶものとする。
【００２６】
本実施形態に係るモデル検査方法では、検査式に含まれる検査変数に応じて、入力された検査対象コードを上記の「実行非検査コード」と「実行検査コード」に分類して最適検査コードを生成している。最適検査コードでは、「実行非検査コード」は実行はされるが状態遷移に展開しての検査を行わないため、検査対象となる状態遷移数が削減され、上述した状態爆発の発生を低減することができる。
【００２７】
図４は、本実施形態に係るモデル検査装置１の構成例を示す図である。
【００２８】
モデル検査装置１は、コード入力部１０、検査式入力部１１、リスト生成部１２、最適化コード変換部１３、及びモデル検査部１４を備えて構成される。
【００２９】
コード入力部１０は、状態遷移モデルに展開可能な検査対象コードを入力する。検査対象コードは、本装置での検査対象であり、前述したＳＰＩＮ等のモデル記述言語で記述されているコードである。
【００３０】
一方、検査式入力部１１は、検査対象コードに対する検査条件が記述される検査式を入力する。検査式は検査変数を含む一方、時相論理式等で表現される検査条件が検査対象コードと同様にＳＰＩＮ等のモデル記述言語で記述されている。
【００３１】
入力された検査対象コードは、リスト生成部１２と最適コード変換部１３に出力される。リスト生成部１２では、検査対象コードから検査依存変数リスト及び特定検査依存変数リストを生成する。最適コード変換部１３では、検査依存変数リスト及び特定検査依存変数リストを参照して、入力した検査対象コードを検査式に応じて最適化し、最適化した検査対象コードをモデル検査部１４に出力する。リスト生成部１２と最適コード変換部１３の動作については、より詳細に後述する。
【００３２】
モデル検査部１４では、最適化された検査対象コードを検査式に基づいて検査し、反例が検出された場合はその反例とログデータを外部に出力する。
【００３３】
（２）最適化手法の概念
次に、本実施形態に係るモデル検査装置１のうち、特に最適コード変換部１３における検査対象コードの最適化手法の概念について説明する。
【００３４】
図５（ａ）、（ｂ）は、以下の説明で使用する検査対象コード（最適化前）の一例を示す図である。今日、多くのシステムでは、複数のプロセスが組み合わされて同時並列的に処理される。この場合、各プロセスの実行順序は不定である。図５（ａ）、（ｂ）は、そのような複数プロセスの例として、２つのプロセス（プロセス１とプロセス２）が同時並列的に処理されるシステムの検査対象コードの一例を示している。
【００３５】
検査対象コードは、３つの変数ｘ、ｙ、ｇを定義しており、プロセス１には、処理コード（ａ）（ｘ＝ｘ＋４）と処理コード（ｂ）（ｇ＝ｇ＋１）が含まれている。また、プロセス２には、処理コード（ｃ）（ｙ＝ｙ＋１）と処理コード（ｄ）（ｇ＝ｇ＊１）が含まれている。
【００３６】
プロセス１とプロセス２の呼び出し順序は不定であり、処理コード（ａ）、（ｂ）、（ｃ）、及び（ｄ）の実行順序は次の６通りがありうる。第１の順序は、（ａ）、（ｂ）、（ｃ）、（ｄ）、第２の順序は、（ａ）、（ｃ）、（ｂ）、（ｄ）、第３の順序は、（ａ）、（ｃ）、（ｄ）、（ｂ）、第４の順序は、（ｃ）、（ａ）、（ｂ）、（ｄ）、第５の順序は、（ｃ）、（ａ）、（ｄ）、（ｂ）、第６の順序は、（ｃ）、（ｄ）、（ａ）、（ｂ）、である。
【００３７】
従来のモデル検査では、総ての状態の組み合わせに対して検査している。複数のプロセスを含む（本例では２つのプロセス）検査対象コードでは、状態遷移の組合わせとして上記の第１の順序から第６の順序を総て含む組み合わせとして展開するため、状態数や遷移数は図５（ｂ）に示すように多くなる（状態数は１３、遷移数は１５）。
【００３８】
これに対して、本実施形態に係るモデル検査方法では、以下に説明する４つのルール（ルール１からルール４）を、入力した検査対象コードに適用して検査対象コードの最適化を行っている。ここでの最適化とは、検査式で指定される検査を行うために必要な状態の遷移は省略することなく残し、検査式で指定される検査に影響を与えない状態は可能な限り除去し、これにより全体の状態遷移の数を低減することを意味している。
【００３９】
４つのルールは、必ずしも総てを同時に適用するというものではなく、入力した検査対象コードと検査式の内容に応じて適用可能なルールが定まる。４つのルールが総て適用できる場合もあれば、４つのルールの中のいずれかは適用できない場合もある。
【００４０】
まず、ルール１は、「『検査変数の値を変化させない処理コード』を検査対象コードから取り除く。検査変数を求める処理コードは、『実行検査コード』としてそのまま残す」といるルールである。なお、「検査変数の値を変化させない処理コード」は、検査対象コードに含まれる処理コードのうち、上記の「実行検査コード」ではなく、かつ後述するルール２やルール３における「実行非検査コード」や「実行検査コード」でもない処理コードに該当するするコードである。
【００４１】
図６（ａ）、（ｂ）は、ルール１の説明図であり、検査変数がｙであることを前提としている。
【００４２】
図６（ａ）に示す検査対象コードの中で、処理コード（ａ）及び（ｂ）は、検査変数ｙを一切含んでいないため、『検査変数の値を変化させない処理コード』に該当する。また、処理コード（ｄ）は、検査変数ｙを含んではいるものの、求める変数はｇであり、処理コード（ｄ）の実行によって検査変数ｙは変化しない。したがって処理コード（ｄ）も『検査変数の値を変化させない処理コード』に該当する。ルール１の前段の適用により、処理コード（ａ）、（ｂ）、（ｄ）は、検査対象コードから取り除かれる。
【００４３】
一方、処理コード（ｃ）は、検査変数ｙそのものを求めるコードであり、通常は処理コード（ｃ）の実行によって検査変数ｙは変化する。前述したように、検査変数を求める処理コードは「実行検査コード」であり、図６（ａ）では、処理コード（ｃ）が「実行検査コード」に該当する。ルール１の後段の適用により、「実行検査コード」はそのまま残す。
【００４４】
結局、最適化された検査対象コードでは、処理コード（ａ）、（ｂ）、（ｄ）が最適化前の検査対象コードから取り除かれ、処理コード（ｃ）のみが残る。
【００４５】
図７は、ルール１を適用したときの最適化前と最適化後における状態遷移図を示している。図７から、最適化前の状態遷移図（図７（ａ））では、状態数１３、遷移数１５であってものが、最適化後の状態遷移図（図７（ｂ））では、状態数２、遷移数２にまで削減されている様子がわかる。
【００４６】
ちなみに、最適化前の状態遷移図の末端における（ｘ、ｙ、ｇ）の状態は、（４、１、４）、（４、１、２）、及び（４、１、２）となっており、検査変数ｙに着目すると、いずれも１となっている。このことは、最適化後の状態遷移図の末端において、検査変数ｙの値が１となっていることに符合しており、状態遷移数を削減した最適化後の状態遷移図においても、検査変数ｙの検査に関しては影響を与えていないことを示している。
【００４７】
ルール２は、「検査変数以外の変数であって、検査変数の値を変化させる変数を検査依存変数とするとき、その検査依存変数を求める処理コードを『実行非検査コード』とする。連続する『実行非検査コード』に対しては、一括実行させかつ処理コード毎の検査は行わせないようにするための不可分命令を付加する」、というルールである。ルール２は、検査対象コードの中にプロセスが１つしか存在しない場合や、複数のプロセスが存在したとしても、各プロセスで求める変数が、他のプロセスの処理によって影響を受けないような場合にはそのまま適用することができる。
【００４８】
一方、ルール３は、検査対象コードの中に複数のプロセスが存在し、かつそれらの複数のプロセスが同時並列的に実行され、各プロセスで求める変数が、他のプロセスの処理によって影響を受ける可能性がある場合に適用されるルールである。ルール３は、ルール２を拡張しつつ、ルール２の例外をも含めて規定するルールである。
【００４９】
ルール３は、「検査変数以外の変数であって、検査変数の値を変化させる変数を検査依存変数とするとき、ある１つのプロセス内の処理コードにおいて求めようとする検査依存変数の値が他のプロセスの処理コードよって変化しない場合は、その検査依存変数を求める当該プロセス内の処理コードを『実行非検査コード』とし、連続する『実行非検査コード』に対しては、一括実行させかつ処理コード毎の検査は行わせないようにするための不可分命令を付加する。一方、ある１つのプロセス内の処理コードにおいて求めようとする検査依存変数の値が他のプロセスの処理コードよって変化する場合はその検査依存変数を特定検査依存変数とし、特定検査依存変数を求める当該プロセス内の処理コードを『実行検査コード』として、そのまま残す。」というルールである。上記における「他のプロセス」とは、当該プロセスと異なるプロセスであり、当該プロセスと「他のプロセス」との互いの実行順序が不定であり、このため実行順序によって検査依存変数の値が異なることがあるような場合における他のプロセスのことである。
【００５０】
図８（ａ）、（ｂ）は、ルール２（或いはルール３の前段部分）を主に説明する図である。説明の都合上、図８（ａ）、（ｂ）における検査対象コードは図６と多少異なっており、検査変数もｙではなくｇとしている。
【００５１】
図８（ａ）において、プロセス１の処理コード（ａ）は、変数ｘのみを含むコードである。変数ｘは、プロセス１及びプロセス２のどの処理コードによっても検査変数ｇの値を変化させない変数である。従って、処理コード（ａ）はルール１の適用によって検査対象コードから取り除かれる。
【００５２】
一方、変数ｙは、プロセス２の処理コード（ｄ）によって検査変数ｇの値を変化させる変数であるから、変数ｙは検査依存変数である。また、処理コード（ｂ）及び（ｃ）で求める検査依存変数ｙの値は、プロセス１（他のプロセス）の処理コードによって変化しないため、処理コード（ｂ）及び（ｃ）は、「実行非検査コード」に該当する。そこで、ルール２の適用により、処理コード（ｂ）及び（ｃ）に対しては、不可分命令を付加する。具体的には、図８（ｂ）に示すように、ＳＰＩＮにおける不可分命令であるatomic命令を付加し、”atomic {“と、”}”とで処理コード（ｂ）及び（ｃ）を囲むようにしている。この結果、処理コード（ｂ）と処理コード（ｃ）は一括で実行され、処理コード毎の検査を行われないようになる。
【００５３】
処理コード（ｄ）は、検査変数ｙを求めるコードであるから、「検査実行コード」に該当し、ルール１の後段の適用によりそのまま残す。
【００５４】
図９（ａ）、（ｂ）は、ルール１及びルール２を、図８（ａ）に示す検査対象コードに適用したときの最適化前と最適化後における状態遷移図を示している。図９（ａ）、（ｂ）から、最適化前の状態遷移図（図９（ａ））では、状態数１０、遷移数１２であったものが、最適化後の状態遷移図（図９（ｂ））では、状態数３、遷移数３にまで削減されている様子がわかる。
【００５５】
他方、図１０（ａ）、（ｂ）は、ルール３の後段部分を主に説明する図である。ここでも説明の都合上、図１０（ａ）、（ｂ）における検査対象コードは図６や図８と多少異なっている。また、検査変数はｙとしている。
【００５６】
図１０（ａ）において、プロセス１の処理コード（ａ）は、変数ｘのみを含むコードであり、変数ｘはプロセス１及びプロセス２のどの処理コードによっても検査変数ｙの値を変化させない変数である。従って、処理コード（ａ）はルール１の適用によって検査対象コードから取り除かれる。
【００５７】
一方、変数ｇは、プロセス２の処理コード（ｃ）によって、検査変数ｙの値を変化させる変数であるから、変数ｇは検査依存変数である。さらに、プロセス１の検査依存変数ｇは、プロセス２（他のプロセス）の処理コード（ｄ）によって値が変化する。同様にプロセス２の検査依存変数ｇも、プロセス１（他のプロセス）の処理コード（ｂ）によって値が変化する。従って、検査依存変数ｇは特定検査依存変数であり、特定検査依存変数ｇを求める処理コード（ｂ）、（ｄ）はいずれも「検査実行コード」である。そこで、最適化後の検査対象コードにいても、処理コード（ｂ）、（ｄ）はそのまま残す。
【００５８】
また、処理コード（ｃ）は、検査変数ｙを求めるコードであり、ルール１の後段の適用により、「検査実行コード」としてそのまま残す。
【００５９】
結局、最適化後の検査対象コードには、処理コード（ｂ）、（ｃ）、及び（ｄ）が残される。
【００６０】
図１１（ａ）、（ｂ）は、ルール１及びルール３の後段を、図１０（ａ）に示す検査対象コードに適用したときの最適化前と最適化後における状態遷移図を示している。図１１（ａ）、（ｂ）から、最適化前の状態遷移図（図１１（ａ））では、状態数１３、遷移数１５であってものが、最適化後の状態遷移図（図１１（ｂ））では、状態数９、遷移数９まで削減されている様子がわかる。
【００６１】
最後に、ルール４は、「実行非検査コードが、その実行非検査コードで求める検査依存変数を含む前記検査実行コードよりも前にあり、かつ、その実行非検査コードで求める検査依存変数を含まない検査実行コードよりも後にある場合は、その実行非検査コードを、検査依存変数を含まない検査実行コードよりも前に移動させる」というルールである。
【００６２】
図１２（ａ）乃至（ｃ）は、ルール１及びルール２に加えて、ルール４も適用した場合の処理を説明する図である。本例では、検査変数がｇであると想定している。
【００６３】
図１２（ａ）に処理コードのうち、処理コード（ｃ）及び（ｆ）は、検査変数ｇを求めるコードでありこれらは実行検査コードに該当する。そこで、ルール１の後段を適用して、図１２（ｂ）では実行検査コード処理コード（ｃ）及び（ｆ）をそのまま残している。
【００６４】
一方、変数ｙは、処理コード（ｆ）において検査変数ｇの値を変化させる変数であるから、検査依存変数である。従って、検査依存変数ｙを求める処理コード（ａ）、（ｂ）、（ｄ）、（ｅ）はいずれも実行非検査コードに該当する。
【００６５】
そこで、ルール２を適用し、連続する実行非検査コード（ａ）、（ｂ）に対して不可分命令(atomic命令)を付加し、一括実行させるようにする。同様に、実行非検査コード（ｄ）、（ｅ）に対しても不可分命令(atomic命令)を付加し、一括実行させるようにする。
【００６６】
最適化前の検査対象コードに対して、ルール１とルール２を適用した結果が図１２（ｂ）に示す準最適化された検査対象コードである。
【００６７】
準最適化された検査対象コードに対して、さらに上述したルール４を適用する。実行非検査コード（ｄ）、（ｅ）は、検査依存変数ｙを含む実行検査コード（ｆ）よりも前にあり、検査依存変数ｙを含まない実行検査コード（ｃ）よりも後にある。従って、ルール４を適用することが可能であり、実行非検査コード（ｄ）、（ｅ）を、実行検査コード（ｃ）の直前に移動させる。この移動によって、実行非検査コード（ｄ）、（ｅ）は、実行非検査コード（ａ）、（ｂ）と連続するようになり、ルール２の適用によって、４つの実行非検査コード（ａ）、（ｂ）、（ｄ）、（ｅ）を不可分命令(atomic命令)によって１つにまとめ、一括実行させることが可能となる。
【００６８】
移動によって、実行非検査コード（ｄ）、（ｅ）と実行検査コード（ｃ）の順序が入れ替わるが、実行検査コード（ｃ）は検査依存変数ｙを含んでいないため、これらの順序を入れ替えても検査変数ｇの値が変わることはなく、検査に影響を与えない。
【００６９】
図１３（ａ）乃至図１３（ｃ）は、最適化前の状態遷移図、ルール１及び２を適用して準最適化した状態遷移図、及びルール４をさらに適用して最適化した状態遷移図を夫々示す図である。状態及び遷移の数が、７から５へ、さらに５から４へと低減されていく様子がこれらの図からわかる。
【００７０】
ここまで説明してきたように、本実施形態に係るモデル検査方法では、入力した検査対象コードに対して、検査変数に基づく４つのルール（ルール１からルール４）を適用することのよって状態遷移の数を削減し、状態爆発が発生する事態を低減している。
【００７１】
（３）最適化検査対象コードを生成する具体的手順
次に、入力された検査対象コードと検査式から、最適化された検査対象コード（最適検査コード）に変換する具体的な手順について、フローチャートに基づいて説明する。
【００７２】
最適化された検査対象コードを生成する手順は、大きく２つの手順に分けられる。第１の手順は、入力した検査対象コードから、依存変数リストと特定依存変数リストとを、検査式を入力する前に予め作成し保存する手順である。第２の手順は、入力した検査対象コードと検査式、及び保存した依存変数リストと特定依存変数リストとから、最適化された検査対象コードを作成する手順である。
【００７３】
図１４は、第１の手順の処理例を示す基本フローチャートであり、図１５及び図１６は、第１の手順の説明図である。図１７は、第１の手順のより詳細な処理例を示す詳細フローチャートである。
【００７４】
ステップＳＴ１では、検査対象コードを入力する。モデル検査装置１のコード入力部１０が検査対象コードの入力を行う。図１５（ａ）及び図１６（ａ）に説明例としての検査対象コードを示している。いずれの例の検査対象コードも、２つのプロセス（プロセスｐ１とプロセスｐ２）を含んでおり、プロセスｐ１とプロセスｐ２の実行順序は不定であるものとしている。図１５（ａ）の検査対象コードと図１６（ａ）の検査対象コードは、６行目のみが異なっており、他の行は総て同じである。図１５（ａ）の検査対象コードの６行目が「ｇ＝ｇ＋１」となっているのに対して、図１６（ａ）の検査対象コードの６行目では「ｙ＝ｙ＋１」となっている。
【００７５】
ステップＳＴ２では、入力した検査対象コード内の処理コードを順次解析し、ある変数数と他の変数との依存関係を求める。具体的には、変数ごとに、その変数を求める処理コードの行数とプロセス名、その変数に対する依存変数及びその依存変数によってその変数の値が変化する処理コードの行数等をリストアップして依存変数リストを生成し、保存する。図１５（ｂ）及び図１５（ｂ）に生成する依存変数リストの一例を示す。
【００７６】
依存変数とは、対象とする変数以外の変数であって、対象とする変数の値を変化させる変数のことである。例えば、図１５（ａ）に示す検査対象コードにおいて、注目する変数をｇとするとき、検査対象コードの１３行に「ｇ＝ｇ＊ｙ」という処理コードが存在する。この処理コードにおいて、変数ｙは変数ｇの値を変化させるため、変数ｙは、変数ｇに対する依存変数となる。そこで、依存変数リスト（図１５（ｂ））の「依存変数」欄に、依存変数ｙと、この依存変数ｙによって注目する変数ｇの値を変化させる処理コードの行数を、[ｙ，１３]のようにリストアップする。
【００７７】
また、「行とプロセス」欄には、注目する変数ｇを求める処理コードの行数とその処理コードが存在するプロセス名を、[１，ｐ１]、［６，ｐ１］、［１１，ｐ２］、［１３，ｐ２］のように、リストアップする。さらに、「プロセス」欄に、処理コードが存在するプロセス名のみをｐ１、ｐ２のようにリストアップしてもよい。
【００７８】
変数ｘ、変数ｙに対しては、これらの変数を変化させる他の変数（即ち、依存変数）は存在しないので、「依存変数」の欄は「−」としている。「行とプロセス」欄及び「プロセス」欄には、変数ｘ、変数ｙを求める処理コードの行数とプロセス名を同様にリストアップしている。「プロセス」欄を参照すれば、変数ｘを求める処理コードはプロセス１にのみに存在し、変数ｙを求める処理コードはプロセス２にのみ存在することが直ちにわかる。
【００７９】
ステップＳＴ２では、依存変数リストに加えて、特定依存変数リストも生成している。図１５（ｃ）及び図１６（ｃ）は、特定依存変数リストの一例を示す図である。
【００８０】
ここで、特定依存変数とは、あるプロセス内で求めようとする依存変数の値が、他のプロセスの処理コードによって変化する場合、その依存変数を特定依存変数とするものである。
【００８１】
例えば、図１５（ａ）に示す検査対象コードにおいて、変数ｇに対する依存変数ｙは、プロセス２の１０行目と１２行目で求められているが、プロセス１（他のプロセス）には、依存変数ｙの値を変化させる処理コードは存在しない。従って、変数ｙは、変数ｇに対する依存変数ではあるが、特定依存変数ではない。
【００８２】
一方、図１６（ａ）に示す検査対象コードにおいては、プロセス１（他のプロセス）の６行目に、依存変数ｙの値を変化させる処理コード（「ｙ＝ｙ＋１」）が存在する。従って、変数ｙは、変数ｇに対する依存変数であると共に、特定依存変数である。
【００８３】
特定依存変数リストは、依存変数リストの「変数」欄と「依存変数」欄とに対応するリストであり、「依存変数」欄を「特定依存変数」欄に置き換えたリストである。該当する変数に対して特定依存変数が存在する場合には「特定依存変数」欄にその特定依存変数をリストアップし、特定依存変数が存在しない場合には「特定依存変数」欄を「−」としている。
【００８４】
ステップＳＴ３では、上記のように作成した依存変数リストと特定依存変数リストとを適宜の記憶媒体に保存する。
【００８５】
図１７は、図１４におけるステップＳＴ２の処理（依存変数リストと特定依存変数リストを作成する処理）の細部手順の一例を示すフローチャートである。
【００８６】
ステップＳＴ１００では、入力した検査対象コードの先頭側からコードを１行取得する。ステップＳＴ１０１で取得したコードが変数宣言文か否かを判定し、変数宣言文の場合は、さらにステップＳＴ１０２で、依存変数リストに登録済みか否かを判定する。
【００８７】
未登録の場合は、変数宣言文で宣言している変数を依存変数リストの「変数」欄に登録する。登録済みの場合は、ステップＳＴ１０７からステップＳＴ１００へ戻り、次の変数宣言文を取得し、その変数を依存変数リストに登録する。
【００８８】
通常の検査対象コードでは、その中で使用される変数が総て変数宣言文で宣言され、その後に演算式（処理コード）が続く。従って、ステップＳＴ１０１で「ＮＯ」の判定がなされた時点で、依存変数リストの「変数」欄には、検査対象コードで使用される変数がすべて登録されることになる。
【００８９】
変数の登録が終了すると、ステップＳＴ１００で取得するコードはコメント文等を除き、主に処理コード（演算式）となる。
【００９０】
ステップＳＴ１０４では、取得したコードが演算式であるか否かを判定し、演算式の場合には、ステップＳＴ１０５にて、その演算式で求める変数（代入演算子の左辺の変数）と、依存変数（代入演算子の右辺に含まれる変数）が存在する場合にはその依存変数を特定する。
【００９１】
ステップＳＴ１０６では、特定した変数を依存変数リストの「変数」欄から検索し、依存変数がある場合には、該当する変数の「依存変数」欄に、その依存変数と取得した処理コードの行を［依存変数、行番号］として登録する。また、該当する変数の「行とプロセス」欄に、取得した処理コードの行とその処理コードが存在するプロセスを［行番号、プロセス名］として登録する。
【００９２】
総ての処理コードに対して、ステップＳＴ１０５、１０６の処理が終了した時点で依存変数リストの作成が終了する。
【００９３】
ステップＳＴ１０８では、依存変数リスト内の依存変数のうち、他のプロセスの処理コード入力よって値が変化する依存変数を特定依存変数として抽出し、特定依存変数リストを作成する。
【００９４】
このようにして、第１の手順では、検査対象コードから依存変数リスト及び特定依存変数リストを予め作成し、保存しておく。
【００９５】
検査対象コードから依存変数リスト及び特定依存変数リストを予め作成し、保存する処理は、モデル検査装置１のリスト生成部１２（図４参照）で行う。
【００９６】
次に、入力した検査対象コードと検査式、及び保存した依存変数リストと特定依存変数リストとから、最適化された検査対象コードを作成する第２の手順について説明する。
【００９７】
図１８は、第２の手順の基本的な処理例を示す基本フローチャートであり、図１９及び図２０は、第２の手順の説明図である。また、図２１及び図２２は、第２の手順のより詳細な処理例を示す詳細フローチャートである。
【００９８】
まず、ステップＳＴ１０（図１８のフローチャート）で、図１９（ａ）に示す検査対象コードを入力する。この検査対象コードは、図１５（ａ）に示した検査対象コードと同じものである。
【００９９】
また、ステップＳＴ１１で、図１９（ｂ）に例示するような検査式を入力し、検査式から検査変数を特定する。検査式の入力はモデル検査装置１の検査式入力部１１によって入力する。
【０１００】
検査式は、通常時相論理式を用いて記述され、本例では、「[](p)、#define p g>0」と記述される。この検査式は、変数ｇに対して、「ｇ＞０が常に成立する。」という意味をもつ。一般的に、１つの検査式では１つの変数を検査の対象としており、検査の対象となる変数を検査式から特定することができる。本例の場合、上記の検査式から、検査変数はｇであることが特定される。
【０１０１】
検査変数が特定されると、依存変数リスト及び特定依存変数リストを参照することにより、検査対象コードの中の処理コードを、「実行非検査コード」、「実行検査コード」、及びこれら以外のコードの３種類に区分することができる。
【０１０２】
依存変数リスト（図１９（ｂ））を参照すると、変数ｇに対する依存変数はｙである。従って、検査変数ｇに対する検査依存変数はｙであることが判る。さらに特定依存変数リスト（図１９（ｃ））を参照すると、変数ｇには特定依存変数が存在しない。従って、変数ｙは、検査変数ｇに対する検査依存変数ではあるが、特定検査依存変数ではないことが判る。
【０１０３】
前述したように、検査依存変数を求める処理コードが「実行非検査コード」である。また、特定検査依存変数を求める処理コードと、検査変数を求める処理コードが「実行検査コード」である。従って、検査変数、検査依存変数、及び特定検査依存変数が判れば、検査対象コードの中の処理コードを、「実行非検査コード」、「実行検査コード」、及びこれら以外のコードの３種類に区分することができる。
【０１０４】
ステップＳＴ１２では、上述した方法によって検査対象コードを「実行非検査コード」、「実行検査コード」、及びこれら以外のコードに区分し、その上で前述したルール１及びルール４を適用する。
【０１０５】
まず、検査変数を変化させない処理コード（即ち、「実行非検査コード」でも「実行検査コード」でもない処理コード）に対してルール１を適用し、検査対象コード（最適化前）から削除する。
【０１０６】
また、「実行非検査コード」に、前述したルール４を適用して並び替えを行う。具体的には、検査依存変数を含む「実行検査コード」よりも前にあり、検査依存変数を含まない「実行検査コード」よりも後にある「実行非検査コード」を、検査依存変数を含まない「実行検査コード」よりも前に並び替える。これにより、検査結果に影響を与えることのない範囲で「実行非検査コード」を一箇所にまとめることが可能となる。
【０１０７】
図１９（ｅ）は、ステップＳＴ１２による削除、並べ替えを終えたあとの検査対象コード（中間コード）を示す図である。検査対象コード（最適化前）の５行目にあった処理コード（ｘ＝ｘ＋４）が削除されている。また、１２行目にあった「実行非検査コード」（ｙ＝ｙ＋４）が検査依存変数を含まない「実行検査コード」（ｇ＝ｇ＋１）の前に並び替えられ、２つの「実行非検査コード」（ｙ＝ｙ＋１、とｙ＝ｙ＋４）が連続して配列されている。
【０１０８】
ステップＳＴ１３では、削除、並び替えの行われた検査対象コード（中間コード）に基づいて、各変数を求める処理コードを検索し、その処理コードの行番号を、特定依存変数リストに付加する。図２０（ｂ）が、処理コードの行番号が付加された特定依存変数リストを示す図である。なお、変数ｘを求める処理コードは削除されて存在しないため、行番号を０としている。
【０１０９】
次のステップＳＴ１４では、削除、並び替えの行われた検査対象コード（中間コード）に対して、ルール２（複数のプロセスが存在する場合はルール３）を適用する。即ち、連続する「実行非検査コード」に対して不可分命令（atomic命令）を付加し、不可分命令の対象となる複数の「実行非検査コード」を一括実行させかつ処理コード毎の検査を行わせないようにする。ステップＳＴ１４の処理によって得られる検査対象コードが最適化された検査対象コードとなる。
【０１１０】
ステップＳＴ１０からステップＳＴ１４までの処理は、モデル検査装置１の最適化コード変換部１３によって行われる。最適化された検査対象コードは、モデル検査部１４に入力され、検査式に基づく検査が実行される。検査の結果は、反例としてモデル検査装置１から出力される。
【０１１１】
図２１は、ステップＳＴ１２のより詳細な処理例を示すフローチャートである。
【０１１２】
ステップＳＴ２００では、依存変数リストと特定依存変数リストを参照し、検査変数に対する検査依存変数と特定検査依存変数を求める。
【０１１３】
ステップＳＴ２０１では、検査対象コード（最適化前）の先頭から順に処理コードを1行取得する。
【０１１４】
ステップＳＴ２０２とステップＳＴ２０３は、取得した処理コードを「実行検査コード」、「実行非検査コード」、及びそれ以外のコードに区分する処理である。取得した処理コードが、検査変数を求めるコード、又は特定検査依存変数を求めるコードの場合はその処理コードを「実行検査コード」とする（ステップＳＴ２０２）。また、取得した処理コードが、検査依存変数を求めるコードの場合はその処理コードを「実行非検査コード」とする（ステップＳＴ２０３）。
【０１１５】
ステップＳＴ２０４では、取得した処理コードが「実行検査コード」又は「実行非検査コード」であるか否かを判定し、「実行検査コード」でも「実行非検査コード」でもない場合には、何もせずにステップＳＴ２０１に戻って次の処理コードを取得する。ステップＳＴ２０４の処理によって、「実行検査コード」と「実行非検査コード」以外の処理コードは、検査対象コードから除去されることになる。
【０１１６】
ステップＳＴ２０５では、取得した処理コードが「実行検査コード」であるか否かが判定され、「実行検査コード」である場合には、ステップＳＴ２０８へ進み、「実行検査コード」をそのまま残す。
【０１１７】
一方、取得した処理コードが「実行検査コード」でない場合、即ち「実行非検査コード」の場合には、ステップＳＴ２０６に進み、「実行非検査コード」の位置を判定する。
【０１１８】
「実行非検査コード」が、検査依存変数を含む「実行検査コード」よりも前にあり、かつ、検査依存変数を含まない「実行検査コード」よりも後にある場合は、その「実行非検査コード」を、検査依存変数を含まない「実行検査コード」の前の行に挿入する。それ以外の場合（ステップＳＴ２０６のＮＯ）は、「実行非検査コード」の並べ替えを行うと検査結果に影響を与える虞があるため、「実行非検査コード」を並べ替えることなくそのまま残す。これらの処理を、総ての処理コードが終了するまで繰り返す（ステップＳＴ２０９）。
【０１１９】
以上のステップＳＴ２００からステップＳＴ２０９までの処理によって、削除、並べ替えの行われた検査対象コード（中間コード）が生成される。
【０１２０】
図２２は、図１８のステップＳＴ１４のより詳細な処理例を示すフローチャートである。
【０１２１】
ステップＳＴ３００で、削除、並び替えの行われた検査対象コード（中間コード）から処理コードを１行取得する。
【０１２２】
ステップＳＴ３０１では、取得した処理コードの位置に不可分命令が挿入可能であるか否かを判定する。モデル記述言語の種類によっては、不可分命令の挿入が禁止されている位置があるからである。例えば、ＳＰＩＮの記述言語では、ＩＦ文の直下にatomic命令（不可分命令）を挿入することが禁止されている。不可分命令の挿入が禁止されている場合には、次の行の処理コードを取得する。
【０１２３】
不可分命令の挿入が禁止されていない場合は、コード行が追加された特定依存変数リストを参照し、検査依存変数を求める処理コード（実行非検査コード）の行番号を不可分命令挿入の対象コード行として抽出する（ステップＳＴ３０２）。
【０１２４】
取得した処理コードの行番号が抽出した対象コード行に一致する場合には（即ち、取得した処理コードが「実行非検査コード」の場合には）（ステップＳＴ３０３のＹＥＳ）、さらに、不可分命令が既に開始されているか否かを判定する（ステップＳＴ３０４）。
【０１２５】
不可分命令が開始されていない場合には、不可分命令の開始コード（ＳＰＩＮの場合には、”atomic {“）を、取得した処理コードの前に挿入する（ステップＳＴ３０５）。
【０１２６】
不可分命令が既に開始されている場合には、ステップＳＴ３００に戻って、次の処理コードを取得する。
【０１２７】
一方、取得した処理コードの行番号が抽出した対象コード行と異なる場合には（即ち、取得した処理コードが「実行検査コード」の場合には）（ステップＳＴ３０３のＮＯ）、ステップＳＴ３０６にて、不可分命令が開始されているか否かを判定する。
【０１２８】
不可分命令が既に開始されており（ステップＳＴ３０６のＹＥＳ）、取得した処理コードが不可分命令の開始後の最初の「実行検査コード」の場合には（ステップＳＴ３０７のＹＥＳ）、不可分命令の終了コード（ＳＰＩＮの場合には、”}”）を、取得した処理コードの前に挿入する。
【０１２９】
他方、取得した処理コード（「実行検査コード」）の前ですでに不可分命令が終了している場合（ステップＳＴ３０６のＹＥＳ）や、不可分命令の開始後の最初の「実行検査コード」ではない場合（ステップＳＴ３０７のＮＯ）には、ステップＳＴ３００に戻って次の処理コードを取得する。
【０１３０】
以上の処理を全処理コードが終了するまで繰り返す（ステップＳＴ３０９）ことにより、連続する「実行非検査コード」の前後に、不可分命令の開始コード”atomic {“と、終了コード”}”を付加することができる。
【０１３１】
以上説明してきたように、本実施形態に係るモデル検査装置１、及びも出る検査方法によれば、入力された検査対象コードを検査式に応じて最適化し、検査時における状態遷移数を低減することが可能であり、この結果従来のモデル検査において問題となっていた状態爆発の発生を低減することができる。
【０１３２】
なお、本発明は上記の実施形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化できる。また、上記実施形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成できる。例えば、実施形態に示される全構成要素から幾つかの構成要素を削除してもよい。さらに、異なる実施形態にわたる構成要素を適宜組み合わせても良い。
【図面の簡単な説明】
【０１３３】
【図１】モデル検査の一般的概念を示す図。
【図２】検査対象コードと状態遷移図との対応関係を示す図。
【図３】不可分命令により、状態遷移数が削減できることを示す図。
【図４】本発明の実施形態に係るモデル検査装置の構成例を示す図。
【図５】複数のプロセスを含む検査対象コードと状態遷移図の対応関係を示す図。
【図６】本実施形態に係るモデル検査方法において、ルール１を適用して最適検査対象コードを得る方法の説明図。
【図７】ルール１の適用による、状態遷移数の変化を示す図。
【図８】本実施形態に係るモデル検査方法において、ルール２を適用して最適検査対象コードを得る方法の説明図。
【図９】ルール２の適用による、状態遷移数の変化を示す図。
【図１０】本実施形態に係るモデル検査方法において、ルール３を適用して最適検査対象コードを得る方法の説明図。
【図１１】ルール３の適用による、状態遷移数の変化を示す図。
【図１２】本実施形態に係るモデル検査方法において、ルール４を適用して最適検査対象コードを得る方法の説明図。
【図１３】ルール４の適用による、状態遷移数の変化を示す図。
【図１４】本発明に係るモデル検査方法における第１の手順の処理例を示す基本フローチャート。
【図１５】本発明に係るモデル検査方法における第１の手順の第１説明図。
【図１６】本発明に係るモデル検査方法における第１の手順の第２説明図。
【図１７】本発明に係るモデル検査方法における第１の手順の処理例を示す詳細フローチャート。
【図１８】本発明に係るモデル検査方法における第２の手順の処理例を示す基本フローチャート。
【図１９】本発明に係るモデル検査方法における第２の手順の第１説明図。
【図２０】本発明に係るモデル検査方法における第２の手順の第２説明図。
【図２１】本発明に係るモデル検査方法における第２の手順の処理例を示す第１詳細フローチャート。
【図２２】本発明に係るモデル検査方法における第２の手順の処理例を示す第２詳細フローチャート。
【符号の説明】
【０１３４】
１  モデル検査装置
１０  コード入力部
１１  検査式入力部
１２  リスト生成部
１３  最適化コード生成部
１４  モデル検査部
【図１】
2010140335.tif 000003
【図２】
2010140335.tif 000004
【図３】
2010140335.tif 000005
【図４】
2010140335.tif 000006
【図５】
2010140335.tif 000007
【図６】
2010140335.tif 000008
【図７】
2010140335.tif 000009
【図８】
2010140335.tif 000010
【図９】
2010140335.tif 000011
【図１０】
2010140335.tif 000012
【図１１】
2010140335.tif 000013
【図１２】
2010140335.tif 000014
【図１３】
2010140335.tif 000015
【図１４】
2010140335.tif 000016
【図１５】
2010140335.tif 000017
【図１６】
2010140335.tif 000018
【図１７】
2010140335.tif 000019
【図１８】
2010140335.tif 000020
【図１９】
2010140335.tif 000021
【図２０】
2010140335.tif 000022
【図２１】
2010140335.tif 000023
【図２２】
2010140335.tif 000024