(57)【要約】【課題】外部環境変数の値による不要な遷移の組み合わせを削除して状態数の増加を抑制した外部環境統合モデルを生成する検査モデル生成装置を提供する。【解決手段】モデル検査器の入力となるプログラムであってイベントの発生により状態から状態への遷移を行う検査用モデルと、検査対象に影響を与える外部環境変数の変数名と値候補の組を保持する外部環境変数リストを入力し、検査用モデル及び外部環境変数リストを解析して、検査用モデル内の外部環境変数の利用個所を抽出するモデル解析部と、非決定的に外部環境変数の値候補を選択する処理を外部環境変数の利用箇所の前に注入して、外部環境統合モデルを生成する最適化モデル生成部とを、備えた検査モデル生成装置。【選択図】図２
2015022692.tif 000002
【特許請求の範囲】
【請求項１】
モデル検査器の入力となるプログラムであってイベントの発生により状態から状態への遷移を行う検査用モデルと、検査対象に影響を与える外部環境変数の変数名とその変数が取り得る値候補の組を保持する外部環境変数リストを入力し、前記検査用モデル及び外部環境変数リストを解析して、前記検査用モデル内の前記外部環境変数の利用個所を抽出するモデル解析部と、
非決定的に前記外部環境変数の値候補を選択する処理を前記外部環境変数の利用箇所の前に注入して、外部環境統合モデルを生成する最適化モデル生成部とを、
備えた検査モデル生成装置。
【請求項２】
前記検査用モデル及び前記外部環境変数リストを入力する入力部と、
入力した前記検査用モデル、前記外部環境変数リスト及び前記外部環境変数の利用個所のデータを保持するメモリとを備える請求項１記載の検査モデル生成装置。
【請求項３】
非決定的に前記外部環境変数の値候補を選択する処理は、外部環境の情報の範囲を削減するもので、システムの振る舞いに影響を与える値のみを外部環境の取りうる値として選択して定義する外部環境の静的抽象化であり、
前記外部環境変数の利用箇所の前に注入する処理は、外部環境の情報の変化に制約を設けるもので、システムの振る舞いに影響を与える箇所でのみ、外部環境の値を変動させる外部環境の動的抽象化である請求項１又は請求項２記載の検査モデル生成装置。
【請求項４】
前記システムの振る舞いに影響を与える値は、閾値あるいは代表値である請求項３記載の検査モデル生成装置。
【請求項５】
前記外部環境を統合する際の抽象化処理は、繰り返し処理あるいは逐次処理のいずれかである請求項３記載の検査モデル生成装置。
【請求項６】
前記外部環境変数の利用個所は、イベント発生条件、ガード条件及びアクションによって抽出する請求項１乃至請求項５のいずれか1項に記載の検査モデル生成装置。
【請求項７】
前記外部環境変数の変数名と値候補は、前記検査用モデル内のイベント発生条件、ガード条件及びアクションにおいて変数として現れる請求項１乃至請求項５のいずれか1項に記載の検査モデル生成装置。
【請求項８】
前記外部環境変数の利用箇所の探索は、アトミックな操作・処理の範囲で行う請求項１乃至請求項５のいずれか1項に記載の検査モデル生成装置。
【請求項９】
前記外部環境変数が外部環境変数リストに記載された値候補のいずれかを非決定的に選択する処理を前記アトミックな範囲内に注入する請求項８記載の検査モデル生成装置。
【請求項１０】
前記外部環境統合モデルは、モデル検査ツールであるＳＰＩＮ（商標）用である請求項１乃至請求項９のいずれか１項に記載の検査モデル生成装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明の実施形態は、検査モデル生成装置に関する。
【背景技術】
【０００２】
ソフトウェアが複雑化してきたことにより、ソフトウェア自体のみならずソフトウェア作成の基となるシステム仕様にこれまで以上に誤りが混入しやすくなっている。更に人の手では、システム仕様を網羅した検査が困難になってきている。
【０００３】
その解決法として、形式的手法の一つであるモデル検査が着目されている。 モデル検査によって、人の手では発見しづらい不適合な事例の発見に効果を挙げている。
【０００４】
モデル検査では、検査対象のモデル化だけでなく、検査対象に影響を与える外部環境もモデル化する必要がある。
【０００５】
従来のモデル検査において、外部環境は検査対象のプロセスと並行に実行されるプロセスとしてモデル化され、状態遷移規模が大きくなり、状態爆発が起きやすくなるという問題があった。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２０１０−２０５５５号公報
【非特許文献】
【０００７】
【非特許文献１】第17回 ZIPCユーザーズカンファレンス「ZIPCを活用したモデル検査ツール開発への取り組み」
【非特許文献２】JaSST'08 Tokyo「ModellCheckiing技術の専門性の排除とその効用」
【発明の概要】
【発明が解決しようとする課題】
【０００８】
本発明が解決しようとする課題は、外部環境変数の値による不要な遷移の組み合わせを削除して状態数の増加を抑制した外部環境統合モデルを生成する検査モデル生成装置を提供することである。
【課題を解決するための手段】
【０００９】
実施形態の検査モデル生成装置は、モデル検査器の入力となるプログラムであってイベントの発生により状態から状態への遷移を行う検査用モデルと、検査対象に影響を与える外部環境変数の変数名と値候補の組を保持する外部環境変数リストを入力し、前記検査用モデル及び外部環境変数リストを解析して、前記検査用モデル内の前記外部環境変数の利用個所を抽出するモデル解析部と、非決定的に前記外部環境変数の値候補を選択する処理を前記外部環境変数の利用箇所の前に注入して、外部環境統合モデルを生成する最適化モデル生成部とを、備える。
【図面の簡単な説明】
【００１０】
【図１】一般的なモデル検査器によるモデル検査の概要を模式的に示した図である。
【図２】本発明の実施形態に係る検査モデル生成装置の概略構成を示すブロック図である。
【図３】外部環境変数リストの一例を示す図である。
【図４】実施形態に係る検査モデル生成装置における外部環境統合モデルの生成処理の流れを示すフローチャートである。
【図５】繰り返し処理による抽象化処理の流れを示すフローチャートである。
【図６】逐次処理による抽象化処理の流れを示すフローチャートである。
【図７】アトミックな範囲内・範囲外における変動処理の注入を対比する図である。
【図８】従来手法Ａによる探査空間及び状態数と本実施形態による探査空間及び状態数を例示した図である。
【図９】従来手法Ｂによる検査用モデルを例示した図である。
【図１０】本実施形態による検査用モデルを例示した図である。
【図１１】モデル検査器ＳＰＩＮで各検査用モデルについてモデル検査を実行した比較表である。
【図１２】検査用モデルの構造の一例を示す図である。
【図１３】Promela言語で記述した検査用モデルから外部環境統合モデルが生成される流れを示す図である。
【図１４】Promela言語で記述した検査用モデルから外部環境統合モデルが生成される流れを示す図である。
【図１５】Promela言語で記述した検査用モデルから外部環境統合モデルが生成される流れを示す図である。
【図１６】アトミックな範囲の検索の流れを示したフローチャートである。
【発明を実施するための形態】
【００１１】
以下、本発明の一実施の形態について、図面を参照して説明する。尚、各図において同一箇所については同一の符号を付すとともに、重複した説明は省略する。
【００１２】
まず、本実施形態で用いる主要な用語について説明する。
【００１３】
「モデル検査」とは、動作仕様がとりうる全ての状態を網羅的に探索し、制約条件に反する不適合が発生するか否かの検査をいう。
【００１４】
「外部環境」とは、モデル検査における検査対象（検査したい機能やプロセス）以外の、検査対象に影響を与える外部要因をいう。例えば、サーバへのアクセス、センシングで得られた値等である。
【００１５】
「アトミックな操作・処理」とは、単一で不可分な一連の操作・処理をいう。処理の途中で他プロセスからの割り込みを発生させない。状態遷移モデルにおいては、遷移時アクションおよび状態遷移はアトミックな処理になる。
【００１６】
「非決定的な選択」とは、モデル検査では、複数の命令文が同時に実行可能であり、次の処理を一意に決定できない非決定性を保持する場合、任意の方法で（乱数を使ってランダムに、あるいは順序立てて）選択し、全網羅探索を行うことをいう。
【００１７】
「システム仕様」は、状態遷移モデルとして表現することが可能であり、システムがとりうる状態と、状態を遷移させるイベントやガード条件によって表すことができる。
【００１８】
「イベント」とは、遷移をもたらす外的刺激や内的変化などを表し、入力とも事象とも表現される。一つのイベントは一つの遷移を決定するが、それらはイベント発生時の状態によって変化する。
【００１９】
「アクション」とは、遷移の結果生じる分析が可能な対象物を意味し、出力とも表現される。アクションと遷移後の状態は区別される。
【００２０】
「状態爆発」とは、状態の数が膨大となって検査不能となることである。
【００２１】
図１は、一般的なモデル検査器によるモデル検査の概要を模式的に示した図である。状態遷移モデルは、所定のモデル記述言語によってモデル検査プログラム（モデルデータ）として記述することが可能であり、このモデル検査プログラムが検査対象としてモデル検査器に入力される。
【００２２】
一方、システムの仕様が所定の検査条件を満たすか否かを判定するための検査条件は、所定の言語で記述した検査式としてモデル検査器に入力される。
【００２３】
モデル検査器では、モデル検査プログラムが取りうる総ての状態遷移の組み合わせに対して、検査式を満たすか否かを判定する。検査式を満たさない状態が発見された場合は、その状態が反例としてモデル検査器から出力される。また、その状態へ至る過程もログデータとして出力される。反例を解析することによって、システムの仕様の修正の検討を行い、修正する。
【００２４】
モデル検査では状態遷移の組み合わせをしらみつぶしに網羅的に検索して検査条件を満たすか否かを判定する。
【００２５】
本実施形態においては、検査用モデルがアクションやガード条件で外部環境変数を利用するものであっても、外部環境変数を利用する箇所でのみ外部環境変数の値の変化を行うことにより、状態数の増加を最小限に抑える。
【００２６】
図２は、本発明の実施形態に係る検査モデル生成装置の概略構成を示すブロック図である。この装置は汎用のコンピュータ（例えばパーソナルコンピュータ（ＰＣ）等）と、同コンピュータ上で動作するソフトウェアとを用いて実現される。コンピュータとしては、ＣＡＤ（Computer Aided Design）やＣＡＥ（Computer Aided Engineering）に好適なエンジニアリングワークステーション（ＥＷＳ）等も含む。本実施形態はこのようなコンピュータに、検査用モデル及び外部環境変数リストに基づいた検査用モデル内の外部環境変数の利用個所の抽出、外部環境変数の値候補を非決定的に選択する処理を外部環境変数の利用箇所の前に注入した外部環境統合モデルの生成に係る一連の手続きを実行させるプログラムとして実施することもできる。
【００２７】
図２に示すように、本実施形態に係る検査モデル生成装置は、主として、入力部１１、モデル解析部１２、最適化モデル生成部１３から構成されている。
【００２８】
入力部１１は、検査対象である検査用モデル及び外部環境変数リストを入力する。検査用モデルは、イベントの発生により状態から状態への遷移を行う、モデル検査器の入力となるプログラムである。外部環境変数リストは、検査用モデル内のイベント発生条件、ガード条件及びアクションに、変数として現れている“外部環境変数の変数名”と“値候補”の組を保持するリストである。図３は、外部環境変数リストの一例を示す図である。図３に示す例では、外部環境変数名“ExternalFlag”は、“true”又は“false”の値をとり、外部環境変数名“ExternalValue”は、１又は５の値をとることを示している。入力した検査用モデル及び外部環境変数リストは、モデル解析部１２によって参照される。尚、入力部１１で入力した検査用モデル及び外部環境変数リストは、一旦、メモリ（図示しない）に保持してもよい。
【００２９】
モデル解析部１２は、検査用モデル及び外部環境変数リストを解析して、検査用モデル内の“外部環境変数の利用個所”を抽出する。外部環境変数の利用個所の詳細は後述する。外部環境変数の利用個所は、一旦、メモリ（図示しない）に保持してもよい。抽出した外部環境変数の利用個所は、最適化モデル生成部１３によって参照される。
【００３０】
最適化モデル生成部１３は、外部環境変数の値候補を非決定的に選択する処理を外部環境変数の利用箇所の前に注入して、外部環境統合モデルを生成する。外部環境統合モデルは、外部環境の静的抽象化，動的抽象化を行った検査用モデルである。外部環境の静的抽象化は、外部環境の情報の範囲を削減するものであって、システムの振る舞いに影響を与える値（閾値、代表値など）のみを、外部環境の取りうる値として与えるものである。具体的には、外部環境変数リストの値候補として、システムの振る舞いに影響を与える値のみを選択して定義することである。外部環境の動的抽象化は、外部環境の情報の変化に制約を設けるものであって、システムの振る舞いに影響を与える箇所でのみ、外部環境の値を変動させるものである。具体的には、非決定的に外部環境変数の値候補を選択する処理を外部環境変数の利用箇所の前に注入することである。外部環境の抽象化の詳細は、後述する。
【００３１】
生成された外部環境統合モデルは、公知のモデル検査器（図示しない）で実行される。
【００３２】
次に、以上のように構成された検査モデル生成装置１００におけるモデル検査プログラムである外部環境統合モデルの生成処理の流れについて説明する。
【００３３】
図４は、実施形態に係る検査モデル生成装置１００における外部環境統合モデルの生成処理の流れを示すフローチャートである。ここでは、生成処理の概要を述べ、処理の詳細は後述する。
【００３４】
まず、入力部１１を介して、検査用モデル及び外部環境変数リストを入力する（ステップＳ４１）。
【００３５】
次いで、モデル解析部１２で検査用モデルを解析し、外部環境変数の利用箇所（イベント発生条件、ガード条件、アクション）を抽出する（ステップＳ４２）。
【００３６】
次に、最適化モデル生成部１３で、外部環境変数の利用箇所の前に外部環境変数の値を非決定的に選択する処理を注入する（ステップＳ４３）。上記した、外部環境を統合する際の抽象化処理は、繰り返し処理あるいは逐次処理のいずれでもよい。
【００３７】
次いで、外部環境統合モデルを生成する（ステップＳ４４）。
【００３８】
＜繰り返し処理による抽象化＞
次に、繰り返し処理による抽象化について詳述する。図５は、繰り返し処理による抽象化処理の流れを示すフローチャートである。
【００３９】
まず、検査用モデル内を任意の方法で探索する（ステップＳ５１）。
【００４０】
次に、検査用モデルにおいて、イベント発生条件、ガード条件、アクションに外部環境変数を利用しているかを判定する（ステップＳ５２）。
【００４１】
ステップＳ５２でＹｅｓであれば、利用箇所、利用される外部環境変数を抽出する（ステップＳ５３）。
【００４２】
次いで、外部環境変数の利用箇所を含むアトミックな範囲を検索する（ステップＳ５４）。ここで、アトミックな範囲とは、アトミックな操作・処理の範囲をいう。
【００４３】
次に、アトミックな範囲の先頭に利用される外部環境変数の変動処理を注入する（ステップＳ５５）。
【００４４】
次いで、利用される全外部環境変数の変動処理を注入したか否かを判定する（ステップＳ５６）。ここで、変動処理とは、外部環境変数が外部環境変数リストに記載された値候補のいずれかを非決定的に選択する処理をいう。
【００４５】
ステップＳ５６でＮｏであればステップＳ５５に戻り、一方、ステップＳ５６でＹｅｓであれば、検査用モデル内を全て探索したか否かを判定する（ステップＳ５７）。
【００４６】
上記ステップＳ５２でＮｏであればステップＳ５７に移行する。
【００４７】
ステップＳ５７でＮｏであればステップＳ５２に戻り、一方、ステップＳ５７でＹｅｓであれば、処理を終了する。
【００４８】
＜逐次処理による抽象化＞
次に、逐次処理による抽象化について詳述する。図６は、逐次処理による抽象化処理の流れを示すフローチャートである。
【００４９】
まず、検査用モデルの先頭から外部環境変数の変数名で探索する（ステップＳ６１）。
【００５０】
次に、変数名が見つかったか否かを判定する（ステップＳ６２）。
【００５１】
ステップＳ６２でＹｅｓであれば、見つけた変数名の位置を含むアトミックな範囲の先頭位置を探索する（ステップＳ６３）。ここで、アトミックな範囲とは、アトミックな操作・処理の範囲をいう。
【００５２】
次いで、先頭位置と変数名のペアを、注入リスト（図示しない）に記録する（ステップＳ６４）。ここで、注入リストは、逐次処理を実行するための都合上、内部的に作成する一時的データを保持するものである。
【００５３】
次に、見つけた変数名の位置の次から外部環境変数の変数名で探索（ステップＳ６５）した後、ステップＳ６２に戻る。
【００５４】
一方、ステップＳ６２でＮｏであれば、注入リストを読み込む（ステップＳ６６）。
【００５５】
次に、未処理の先頭位置と変数名のペアがあるか否かを判定する（ステップＳ６７）。
【００５６】
ステップＳ６７でＹｅｓであれば、注入リストから先頭位置と変数名のペアを取り出す（ステップＳ６８）。
【００５７】
次いで、先頭位置に、変数名が示す外部環境変数の変動処理を注入（ステップＳ６９）した後、ステップＳ６７に戻る。ここで、変動処理とは、外部環境変数が外部環境変数リストに記載された値候補のいずれかを非決定的に選択する処理をいう。
【００５８】
一方、ステップＳ６７でＮｏであれば、処理を終了する。
【００５９】
＜アトミックな範囲での変動処理＞
ここで、アトミックな範囲内に変動処理を注入する理由について説明する。図７は、アトミックな範囲内・範囲外における変動処理の注入を対比する図である。
【００６０】
図７（ａ）に示すように、アトミックな範囲外に変動処理を注入すると、他プロセスからの外部環境変数Exの変動処理の割り込みが発生する可能性がある。そのため、プロセスAの外部環境変数Exの変動処理が無駄になり、必要のない状態を増やす原因になる。
【００６１】
一方、図７（ｂ）に示すように、アトミックな範囲内に変動処理を注入すると、他プロセスからの外部環境変数Exの変動処理の割り込みが発生しない。
【００６２】
＜検査用モデルの比較＞
本実施形態によって生成される検査用モデルと、従来手法Ａ，Ｂによる検査用モデルとを状態数の観点から対比する。従来手法Ａは、検査用モデルの状態遷移モデルと、外部環境の状態遷移モデルを並行実行するものである。図８は、従来手法Ａによる探査空間及び状態数と本実施形態による探査空間及び状態数を例示した図である。図８（ａ）では、従来手法Ａによる検査対象である検査用モデルと外部環境が状態遷移表で表されている。状態遷移表の一番左の列には、状態遷移モデルに現れる遷移前の状態が配列される。図８（ａ）に示す検査用モデルの例では、３つの状態Ｓ１、Ｓ２、Ｓ３が配列されている。一方、状態遷移表の一番上の行には、状態遷移モデルにおいて遷移を引き起こすイベントが配列される。図８（ａ）の検査用モデルでは、４つのイベントＥ１、Ｅ２、Ｅ３、Ｅ４が配列されている。状態遷移表の中央部のマスには遷移後の状態が配列される。また、斜線で示したマスは状態の遷移が起こらないことを示している。いま、状態Ｓｎから状態Ｓｍへの遷移を、（Ｓｎ→Ｓｍ）のように記載すると、図８（ａ）に例示する検査用モデルの状態遷移表は、イベントＥ１によって、（Ｓ１→Ｓ２）及び（Ｓ３→Ｓ２）の２つの遷移が起こることを示している。同様に、イベントＥ２によって（Ｓ２→Ｓ３）の遷移が起こる際に、遷移時アクションとしてローカル変数αへ外部環境変数Exの値を代入することを示している。イベントＥ３によって（Ｓ２→Ｓ１）の１つの遷移が起こることを示している。イベントＥ４によって（Ｓ１→Ｓ３）、（Ｓ２→Ｓ１）及び（Ｓ３→Ｓ１）の３つの遷移が起こる際に、遷移時アクションとしてローカル変数αへ外部環境変数Exの値を代入することを示している。
【００６３】
さらに、図８（ａ）に示す外部環境の例では、２つの状態Ex＝１、Ex＝５が配列されている。状態Ex＝１とは外部環境変数Exの値が１である状態を示し、状態Ex＝５とは外部環境変数Exの値が５である状態を示している。一方、図８（ａ）の外部環境の例では、状態遷移モデルにおいて遷移を引き起こす３つのイベントＥ５、Ｅ６、Ｅ７が配列されている。イベントＥ５によって外部環境変数Exの値が１に書き換えられ、イベントＥ６によって外部環境変数Exの値が５に書き換えられ、イベントＥ７によって外部環境変数Exの値が１の場合には５に書き換えられ、さらに外部環境変数Exの値が５の場合には１に書き換えられることを示している。
【００６４】
図８（ｂ）では、状態遷移表で表された検査用モデルと外部環境が、本実施形態に係る外部環境統合モデルとして状態遷移表で示されている。状態遷移表の意味するところは、上記と同様である。
【００６５】
図８（ａ）に示すように、従来手法Ａでは、検査対象による探索空間と外部環境による探索空間との積となるから、探索空間は大きく、状態数も大きくなっている。これに対して、図８（ｂ）に示すように、本実施形態によれば、探索空間は小さく、状態数も小さくなっている。
【００６６】
従来手法Ｂは、検査用モデルと外部環境を同一の状態遷移モデルで実行するものである。図９は、従来手法Ｂによる検査用モデルを例示した図で、探索空間のノードを簡略化している。状態遷移を示す箇所のカッコ内は、それぞれ、“状態”、“変数aの値”、“外部環境変数Exの値”を表している。図９に示すように、従来手法Ｂでは、イベントの発生に伴って生じる外部環境の値の変化を記述し，検査対象の検査用モデル内のイベント発生部にて作用させるものである。そのため、外部環境変数Exの値だけが変化しているだけで、モデル検査に直接関係のない状態遷移が含まれている。また、最終的に達するノードは同じだが、外部環境変数Exの値変化のタイミングによってパスが分岐している。
【００６７】
図１０は、本実施形態による検査用モデルを例示した図で、探索空間のノードを簡略化している。状態遷移を示す箇所のカッコ内は、それぞれ、“状態”、“変数aの値”、“外部環境変数Exの値”を表している。図１０に示すように、外部環境変数Exの値だけが変化するパスは削減するので、外部環境変数Exの値変化のタイミングは、検査対象に影響を与える箇所の直前だけに限定し、分岐するパスを削減している。
【００６８】
図１１は、モデル検査器ＳＰＩＮ（商標）で各検査用モデルについてモデル検査を実行した比較表である。図１１に示す例では、検査対象の規模に関しては、状態数：10、イベント数：14、遷移数:467、変数数：11とし、外部環境の規模に関しては、状態数：2、イベント数：3、遷移数：3、変数数：1としている。図１１から明らかなように、本実施形態によれば、従来手法Ａ，Ｂに比べて状態数が圧倒的に少ないので、メモリ使用量も少なくてすみ、モデル検査に要する実行時間も著しく減少している。
【００６９】
（実施例）
＜外部環境統合モデル生成アルゴリズム＞
次に、外部環境統合モデル生成アルゴリズムについて説明する。モデル検査のためのツールとしては、オートマトンベースのモデルチェッカであるＳＰＩＮ（商標）を利用することができる。ＳＰＩＮ（商標）では、検査対象と検査式を二つのオートマトンに変換し、この二つのオートマトンに積集合があるか否かを計算する。ＳＰＩＮ（商標）は、Promelaという専用言語で記述された外部環境統合モデル（プログラム）を実行して検査する。
【００７０】
図１２は、検査用モデルの構造の一例を示す図である。図１２に示すように、検査用モデルは、変数定義部とプロセスから成り、プロセスはイベント発生部と状態遷移部から成っている。変数定義部において、“状態”、“イベント”、“外部環境変数”が、それぞれ定義されている。イベント発生部では、各イベントの発生条件が定義されている。状態遷移部では、各イベントに対応したガード条件、アクションが定義されている。
【００７１】
図１３から図１５は、Promela言語で記述した検査用モデルから外部環境統合モデルが生成される流れを示したものである。
【００７２】
外部環境変数の値候補は、状態遷移モデルの構文解析から、条件式における定数との比較演算が抽出できれば、その値が候補となる。例えば、条件式１<Ex、１>=Exがあれば、Exの候補値は１以下の値あるいは１より大きい値になる。尚、外部環境に詳しい開発者から適切な閾値や代表値を入手することも好適である。
【００７３】
図１６は、アトミックな範囲の検索の流れを示したフローチャートである。
【００７４】
Promelaでは、「atomic{」「}」で囲まれた範囲がアトミックなので、「atomic{」「}」をキーワードとして、構文解析を行い、囲まれた範囲を検索する（ステップＳ１６０１）。
【００７５】
次に、外部環境変数の利用箇所(コード1行分)を含んでいるか否かを判定する（ステップＳ１６０２）。
【００７６】
ステップＳ１６０２でＮｏであれば、利用箇所から制御記号によって、外部環境変数の式を抽出する（ステップＳ１６０３）。Promelaでは、上記以外に、1つの式（文）がアトミック「;」「->」「::」「od」「fi」などの制御記号で区切られた式もアトミックである。
【００７７】
次いで、外部環境変数の式を「atomic{}」で囲む（ステップＳ１６０４）。
【００７８】
これにより、アトミックな範囲(「atomic{}」で囲まれた場所)が特定され（ステップＳ１６０５）、アトミックな範囲の検索を終了する。
【００７９】
一方、ステップＳ１６０２でＹｅｓであれば、ステップＳ１６０５に移行した後、アトミックな範囲の検索を終了する。
【００８０】
以上説明したように、本実施形態によれば、検査用モデルがアクションやガード条件で外部環境変数を利用するものであっても、外部環境変数を利用する箇所でのみ外部環境変数の値の変化を行うことにより、外部環境変数の値による不要な遷移の組合せを削除することができる。
【００８１】
本発明のいくつかの実施形態を説明したが、これらの実施形態は、例として提示したものであり、発明の範囲を限定することは意図していない。これら新規な実施形態は、その他の様々な形態で実施されることが可能であり、発明の要旨を逸脱しない範囲で、種々の省略、置き換え、変更を行うことができる。これら実施形態やその変形は、発明の範囲や要旨に含まれるとともに、特許請求の範囲に記載された発明とその均等の範囲に含まれる。
【符号の説明】
【００８２】
１００・・・検査モデル生成装置
１１・・・入力部
１２・・・モデル解析部
１３・・・最適化モデル生成部
【図１】
2015022692.tif 000003
【図２】
2015022692.tif 000004
【図３】
2015022692.tif 000005
【図４】
2015022692.tif 000006
【図５】
2015022692.tif 000007
【図６】
2015022692.tif 000008
【図７】
2015022692.tif 000009
【図８】
2015022692.tif 000010
【図９】
2015022692.tif 000011
【図１０】
2015022692.tif 000012
【図１１】
2015022692.tif 000013
【図１２】
2015022692.tif 000014
【図１３】
2015022692.tif 000015
【図１４】
2015022692.tif 000016
【図１５】
2015022692.tif 000017
【図１６】
2015022692.tif 000018