(57)【要約】      （修正有）【課題】モデル検査時における状態爆発の発生を低減可能な状態遷移モデルを生成することができる検査モデル生成装置を提供する。【解決手段】状態遷移モデルを入力するモデル入力部２０と、イベントごとに遷移を関連付ける予備遷移リストを生成する予備リスト生成部２１と、予備遷移リストを検索し、異なるイベントであっても、そのイベントによって起こされる遷移が同じ場合には、異なるイベントを１つのイベントグループとして集約し、集約したイベントグループと、そのイベントグループに属するイベントによって起こされる遷移とを関連付ける縮約遷移リストを生成する縮約リスト生成部２２と、縮約遷移リストから検査用モデルコードに変換し、予備リストから直接検査用モデルコードを変換するよりも遷移数の少ない検査用モデルコードを生成するコード変換部２３と、を備える。【選択図】図２
2010140084.tif 000002
【特許請求の範囲】
【請求項１】
遷移前状態と遷移後状態とで規定される遷移、及びその遷移を起こすイベントを少なくとも含む状態遷移モデルを入力するモデル入力部と、
前記イベントごとに前記遷移を関連付ける予備遷移リストを、入力した前記状態遷移モデルから生成する予備リスト生成部と、
前記予備遷移リストを検索し、異なるイベントであっても、そのイベントによって起こされる遷移が同じ場合には、前記異なるイベントを１つのイベントグループとして集約し、集約した前記イベントグループと、そのイベントグループに属するイベントによって起こされる遷移とを関連付ける縮約遷移リストを、前記予備遷移リストから生成する縮約リスト生成部と、
前記縮約遷移リストから検査用モデルコードに変換することにより、前記予備リストから直接検査用モデルコードを変換するよりも遷移数の少ない前記検査用モデルコードを生成するコード変換部と、
を備えたことを特徴とする検査モデル生成装置。
【請求項２】
前記縮約リスト生成部は、
前記予備遷移リストをイベントごとに順次比較し、
比較するイベントに夫々関連付けられる前記遷移が総て一致する場合は、比較する各イベントを１つのイベントグループとして集約し、
前記遷移の一部が一致する場合には、一致する前記遷移に関わる各イベントを１つのイベントグループとして集約し、一致しない前記遷移に関わる各イベントは集約せずに残す、
ことを特徴とする請求項１に記載の検査モデル生成装置。
【請求項３】
前記状態遷移モデルは、
前記遷移に伴って実行するアクションがある場合はそのアクションを含み、
前記予備リスト生成部は、
前記イベントごとに、前記遷移と前記アクションとを関連付ける前記予備遷移リストを生成し、
前記縮約リスト生成部は、
前記アクションを、状態遷移に影響を与えるものとして指定される指定アクションとそれ以外の非指定アクションとに分類し、異なるイベントであっても、（ａ）そのイベントによって起こされる前記遷移とこれに伴う前記指定アクションが同じ場合、（ｂ）そのイベントによって起こされる前記遷移が同じであり、かつ前記遷移に伴う前記アクションが前記非指定アクションである場合、又は、（ｃ）そのイベントによって起こされる前記遷移が同じであり、かつ前記遷移が前記アクションを伴わない場合には、前記異なるイベントを１つのイベントグループとして集約する、
ことを特徴とする請求項１に記載の検査モデル生成装置。
【請求項４】
遷移前状態と遷移後状態とで規定される遷移、及びその遷移を起こすイベントを少なくとも含む状態遷移モデル、及び検査条件が時相論理式によって表現された検査式を入力する入力部と、
前記イベントごとに前記遷移を関連付ける予備遷移リストを、入力した前記状態遷移モデルから生成する予備リスト生成部と、
前記予備遷移リストを検索し、異なるイベントであっても、そのイベントによって起こされる遷移が同じ場合には、前記異なるイベントを１つのイベントグループとして集約し、集約した前記イベントグループと、そのイベントグループに属するイベントによって起こされる遷移とを関連付ける縮約遷移リストを、前記予備遷移リストから生成する縮約リスト生成部と、
前記縮約遷移リストから検査用モデルコードに変換することにより、前記予備リストから直接検査用モデルコードを変換するよりも遷移数の少ない前記検査用モデルコードを生成するコード変換部と、
前記検査用モデルコードにおける状態遷移が前記検査条件を満たすか否かを前記検査式に基づいて検査し、前記状態遷移の中に前記検査条件を満たさない状態遷移を検出した場合は、その状態遷移を反例データとして出力すると共に、その状態遷移へ至る遷移系列をログデータとして出力するモデル検査部と、
を備えたことを特徴とするモデル検査装置。
【請求項５】
前記縮約モデル生成部は、
前記予備遷移リストをイベントごとに順次比較し、
比較するイベントに夫々関連付けられる前記遷移が総て一致する場合は、比較する各イベントを１つのイベントグループとして集約し、
前記遷移の一部が一致する場合には、一致する前記遷移に関わる各イベントを１つのイベントグループとして集約し、一致しない前記遷移に関わる各イベントは集約せずに残す、
ことを特徴とする請求項４に記載のモデル検査装置。
【請求項６】
前記状態遷移モデルは、
前記遷移に伴って実行するアクションがある場合はそのアクションを含み、
前記予備リスト生成部は、
前記イベントごとに、前記遷移と前記アクションとを関連付ける前記予備遷移リストを生成し、
前記縮約リスト生成部は、
前記アクションを、状態遷移に影響を与えるものとして指定される指定アクションとそれ以外の非指定アクションとに分類し、異なるイベントであっても、（ａ）そのイベントによって起こされる前記遷移とこれに伴う前記指定アクションが同じ場合、（ｂ）そのイベントによって起こされる前記遷移が同じであり、かつ前記遷移に伴う前記アクションが前記非指定アクションである場合、又は、（ｃ）そのイベントによって起こされる前記遷移が同じであり、かつ前記遷移が前記アクションを伴わない場合には、前記異なるイベントを１つのイベントグループとして集約する、
ことを特徴とする請求項４に記載のモデル検査装置。
【請求項７】
遷移前状態と遷移後状態とで規定される遷移、及びその遷移を起こすイベントを少なくとも含む状態遷移モデルを入力し、
前記イベントごとに前記遷移を関連付ける予備遷移リストを、入力した前記状態遷移モデルから生成し、
前記予備遷移リストを検索し、異なるイベントであっても、そのイベントによって起こされる遷移が同じ場合には、前記異なるイベントを１つのイベントグループとして集約し、集約した前記イベントグループと、そのイベントグループに属するイベントによって起こされる遷移とを関連付ける縮約遷移リストを、前記予備遷移リストから生成し、
前記縮約遷移リストから検査用モデルコードに変換することにより、前記予備リストから直接検査用モデルコードを変換するよりも遷移数の少ない前記検査用モデルコードを生成する、
ステップを備えたことを特徴とする検査モデル生成方法。
【請求項８】
前記縮約遷移リストを生成するステップでは、
前記予備遷移リストをイベントごとに順次比較し、
比較するイベントに夫々関連付けられる前記遷移が総て一致する場合は、比較する各イベントを１つのイベントグループとして集約し、
前記遷移の一部が一致する場合には、一致する前記遷移に関わる各イベントを１つのイベントグループとして集約し、一致しない前記遷移に関わる各イベントは集約せずに残す、
ことを特徴とする請求項７に記載の検査モデル生成方法。
【請求項９】
前記状態遷移モデルは、
前記遷移に伴って実行するアクションがある場合はそのアクションを含み、
前記予備遷移リストを生成するステップでは、
前記イベントごとに、前記遷移と前記アクションとを関連付ける前記予備遷移リストを生成し、
前記縮約遷移リストを生成するステップでは、
前記アクションを、状態遷移に影響を与えるものとして指定される指定アクションとそれ以外の非指定アクションとに分類し、異なるイベントであっても、（ａ）そのイベントによって起こされる前記遷移とこれに伴う前記指定アクションが同じ場合、（ｂ）そのイベントによって起こされる前記遷移が同じであり、かつ前記遷移に伴う前記アクションが前記非指定アクションである場合、又は、（ｃ）そのイベントによって起こされる前記遷移が同じであり、かつ前記遷移が前記アクションを伴わない場合には、前記異なるイベントを１つのイベントグループとして集約する、
ことを特徴とする請求項７に記載の検査モデル生成方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、検査モデル生成装置、モデル検査装置、及び検査モデル生成方法に係り、特に、状態遷移モデルとして表される検査モデルの生成装置、生成された検査モデルに対して検査を行うモデル検査装置、及び検査モデル生成方法に関する。
【背景技術】
【０００２】
今日、ソフトウェアが複雑化してきたことにより、ソフトウェア自体のみならずソフトウェア作成の基となるシステム仕様に誤りが混入しやすくなってきている。また、システム仕様の複雑化に伴って、人の手では、システム仕様を網羅した検証が困難になってきている。経験や知識のない誤りは発見しづらく、また、後工程で発見された誤りは取り除くために膨大なコストがかかる。このため、システム仕様の誤りを可能な限り人の手を借りずに網羅的に検証し、誤りを早期に取り除くための仕組みが必要不可欠となってきている。
【０００３】
システム仕様を状態遷移モデルで表現すると共に検証条件を論理式で記述し、状態遷移モデルが論理式を満たすかどうかを検証することで仕様の正しさを証明する手法として、モデル検査と呼ばれる手法が知られている（特許文献１，２等）。
【０００４】
また、状態遷移モデルは状態遷移表として表すことができるが、特許文献２には、入力、出力、及び遷移後状態が総て同じであるような遷移前状態を状態遷移表の中でまとめ、これを１つのグループとして状態遷移表に記入することにより、状態遷移表の作成の手間を軽減する技術が開示されている。
【特許文献１】特開２００７−１１６０５号公報
【特許文献２】特開平０３−１９０８６号公報
【発明の開示】
【発明が解決しようとする課題】
【０００５】
モデル検査では、状態遷移モデルとして記述されたシステム仕様と、時相論理式で記述された検査式をモデル検査装置に入力し、状態遷移モデルの動作（即ちシステム仕様）が検査式で表される検証条件を満たすか否かを網羅的に検査する。検証条件を満たさない動作（状態やイベント等）が検出された場合にはその動作は「反例」としてモデル検査装置から出力される。また、反例が検出された場合、その反例に至る直前の一連の動作もログデータとして出力される。モデル検査装置から出力される反例やログデータを人が解析することにより、システム仕様の誤りの発見とその修復を効率よく行うことができる。
【０００６】
一般に、モデル検査では状態遷移の組み合わせをしらみつぶしに網羅的に検索して検査条件を満たすか否かを判定する。このため、システム仕様を機械的に状態遷移モデルに置き換えると、検査時における状態遷移の組み合わせが膨大となり、状態爆発と呼ばれる事象が発生して検査が収束しない事態が発生する場合がある。
【０００７】
本発明は上記事情に鑑みてなされたものであり、モデル検査時における状態爆発の発生を低減可能な状態遷移モデルを生成することができる、検査モデル生成装置、モデル検査装置、及び検査モデル生成方法を提供することを目的とする。
【課題を解決するための手段】
【０００８】
上記課題を解決するため、本発明に係る検査モデル生成装置は、遷移前状態と遷移後状態とで規定される遷移、及びその遷移を起こすイベントを少なくとも含む状態遷移モデルを入力するモデル入力部と、前記イベントごとに前記遷移を関連付ける予備遷移リストを、入力した前記状態遷移モデルから生成する予備リスト生成部と、前記予備遷移リストを検索し、異なるイベントであっても、そのイベントによって起こされる遷移が同じ場合には、前記異なるイベントを１つのイベントグループとして集約し、集約した前記イベントグループと、そのイベントグループに属するイベントによって起こされる遷移とを関連付ける縮約遷移リストを、前記予備遷移リストから生成する縮約リスト生成部と、前記縮約遷移リストから検査用モデルコードに変換することにより、前記予備リストから直接検査用モデルコードを変換するよりも遷移数の少ない前記検査用モデルコードを生成するコード変換部と、を備えたことを特徴とする。
【０００９】
また、本発明に係るモデル検査装置は、遷移前状態と遷移後状態とで規定される遷移、及びその遷移を起こすイベントを少なくとも含む状態遷移モデル、及び検査条件が時相論理式によって表現された検査式を入力する入力部と、前記イベントごとに前記遷移を関連付ける予備遷移リストを、入力した前記状態遷移モデルから生成する予備リスト生成部と、前記予備遷移リストを検索し、異なるイベントであっても、そのイベントによって起こされる遷移が同じ場合には、前記異なるイベントを１つのイベントグループとして集約し、集約した前記イベントグループと、そのイベントグループに属するイベントによって起こされる遷移とを関連付ける縮約遷移リストを、前記予備遷移リストから生成する縮約リスト生成部と、前記縮約遷移リストから検査用モデルコードに変換することにより、前記予備リストから直接検査用モデルコードを変換するよりも遷移数の少ない前記検査用モデルコードを生成するコード変換部と、前記検査用モデルコードにおける状態遷移が前記検査条件を満たすか否かを前記検査式に基づいて検査し、前記状態遷移の中に前記検査条件を満たさない状態遷移を検出した場合は、その状態遷移を反例データとして出力すると共に、その状態遷移へ至る遷移系列をログデータとして出力するモデル検査部と、を備えたことを特徴とする。
【００１０】
また、本発明に係る検査モデル生成方法は、遷移前状態と遷移後状態とで規定される遷移、及びその遷移を起こすイベントを少なくとも含む状態遷移モデルを入力し、前記イベントごとに前記遷移を関連付ける予備遷移リストを、入力した前記状態遷移モデルから生成し、前記予備遷移リストを検索し、異なるイベントであっても、そのイベントによって起こされる遷移が同じ場合には、前記異なるイベントを１つのイベントグループとして集約し、集約した前記イベントグループと、そのイベントグループに属するイベントによって起こされる遷移とを関連付ける縮約遷移リストを、前記予備遷移リストから生成し、前記縮約遷移リストから検査用モデルコードに変換することにより、前記予備リストから直接検査用モデルコードを変換するよりも遷移数の少ない前記検査用モデルコードを生成する、ステップを備えたことを特徴とする。
【発明の効果】
【００１１】
本発明に係る検査モデル生成装置、モデル検査装置、及び検査モデル生成方法によれば、モデル検査時における状態爆発の発生を低減可能な状態遷移モデルを生成することができ、これによりモデル検査の効率を向上させることができる。
【発明を実施するための最良の形態】
【００１２】
本発明に係る検査モデル生成装置、モデル検査装置、及び検査モデル生成方法の実施形態について、添付図面を参照して説明する。
【００１３】
（１）第１の実施形態
図１は、一般的なモデル検査装置の動作概念を模式的に示した図である。システム仕様は状態遷移モデルとして表現することが可能であり、システムがとりうる状態と、状態を遷移させるイベントやガード条件によって表すことができる。状態遷移モデルは、所定のモデル記述言語によってモデルデータとして記述することが可能であり、このモデルデータが検査対象としてモデル検査装置に入力される。
【００１４】
一方、システム仕様が所定の検査条件を満たすか否かを判定するための検査条件は、所定の言語で記述した検査式としてモデル検査装置に入力される。
【００１５】
モデル検査装置では、モデルデータが取りうる総ての状態遷移の組み合わせに対して検査式を満たすか否かを判定する。検査式を満たさない状態が発見された場合は、その状態が反例としてモデル検査装置から出力される。また、その状態へ至る過程もログデータをして出力される。反例やログデータがモデル検査装置の検査結果となる。
【００１６】
前述したように、モデル検査では状態遷移の組み合わせをしらみつぶしに網羅的に検索して検査条件を満たすか否かを判定する。このため、システム仕様を機械的に状態遷移モデルに置き換えると、検査時における状態遷移の組み合わせが膨大となり、状態爆発と呼ばれる事象が発生して検査が収束しない事態が発生する。
【００１７】
本実施形態に係るモデル検査装置１は、このような状態爆発の発生を低減するように構成されている。より具体的には、モデル検査装置１が具備する検査モデル生成装置２によって、入力された状態遷移検査モデル（後述する予備遷移リスト）を解析し、検査の観点から冗長と判断される状態遷移を縮約して遷移数の少ないモデル（後述する縮約遷移リスト）に変換している。そして、遷移数が縮小されたモデルに対してモデル検査を行うことにより状態爆発の発生を低減するようにしている。
【００１８】
図２には、本実施形態に係るモデル検査装置１、及び検査モデル生成装置２の構成例を示すブロック図である。
【００１９】
モデル検査装置１は、検査モデル生成装置２、検査式入力部１０、モデル検査部１１等を備えて構成されている。
【００２０】
また、検査モデル生成装置２は、モデル入力部２０、予備リスト生成部２１、縮約リスト生成部２２、コード変換部２３等を備えて構成されている。
【００２１】
上記のように構成されるモデル検査装置１のうち、まず検査モデル生成装置２の動作について、図３に示すフローチャートに基づいて説明する。
【００２２】
ステップＳＴ１では、状態遷移モデルや検査に用いる変数等を入力する。ここで入力する状態遷移モデルは状態遷移仕様のことであり、状態遷移仕様の表現形式は特に限定するものではない。例えば、表の形式で状態の遷移が表現された状態遷移表の他、遷移前の状態と遷移後の状態が矢印付きのパス等で明示された状態遷移図等、状態遷移で表現できる動作仕様が適宜の言語や書式で表現されているものを入力することができる。
【００２３】
また、検査に用いる変数とは、状態遷移仕様に現れる変数のうち、検査時に用いる状態やイベントに対して割り当てられる変数や状態遷移に直接関わる変数のことである。状態遷移に直接関わる変数とは、例えば、遷移の際にフラグを確認する必要があるような場合において、そのフラグに対して割り当てられる変数である。
【００２４】
状態遷移モデルや検査に用いる変数等は、検査モデル生成装置２のモデル入力部２０から入力される。モデル入力部２０は、例えばコンピュータのユーザインタフェースであり、キーボードやディスプレイ装置といった入出力デバイスを含む装置である。
【００２５】
ステップＳＴ２では、入力された状態遷移モデルや検査に用いる変数から縮約前の状態遷移を表す予備遷移リストを生成する。予備遷移リストは、検査モデル生成装置２の予備リスト生成部２１で生成する。
【００２６】
予備遷移リストは、イベントごとに、イベントとそのイベントによって発生する遷移（遷移前の常態と遷移後の状態の対）とを関連付けるリストである。
【００２７】
図４（ａ）は、状態遷移表の形式で表現された予備遷移リストの一例を示す図である。予備遷移リストの一番上の行には、状態遷移モデルに現れる遷移前の状態が配列される。図４（ａ）の例では、４つの状態Ｓ１、Ｓ２、Ｓ３、Ｓ４が配列されている。
【００２８】
一方、予備遷移リストの一番左の列には、状態遷移モデルにおいて遷移を引き起こすイベントが配列される。図４（ａ）の例では、４つのイベントＥ１、Ｅ２、Ｅ３、Ｅ４、Ｅ５が配列されている。
【００２９】
予備遷移リストの中央部のマスには遷移後の状態が配列される。また、斜線で示したマスは状態の遷移が起こらないことを示している。
【００３０】
いま、状態Ｓｎから状態Ｓｍへの遷移を、（Ｓｎ→Ｓｍ）のように記載すると、図４（ａ）に例示する予備遷移リストは、イベントＥ１によって、（Ｓ１→Ｓ４）、（Ｓ２→Ｓ３）、及び（Ｓ４→Ｓ２）の３つの遷移が起こることを示している。
【００３１】
同様に、イベントＥ２によって（Ｓ２→Ｓ１）及び（Ｓ３→Ｓ１）の２つの遷移が起こり、イベントＥ３によって（Ｓ２→Ｓ１）及び（Ｓ３→Ｓ１）の２つの遷移が起こり、イベントＥ４によって（Ｓ１→Ｓ４）及び（Ｓ４→Ｓ２）の２つの遷移が起こり、イベントＥ５によって、（Ｓ２→Ｓ１）、（Ｓ３→Ｓ１）、及び（Ｓ４→Ｓ２）の３つの遷移が起こることを示している。
【００３２】
このようにして、ステップＳＴ２にて生成された予備遷移リストは、検査モデル生成装置２の縮約リスト生成部２２に入力され、予備遷移リストから縮約遷移リストを生成する。図４（ｂ）は、図４（ａ）の予備遷移リストの例に対応する縮約遷移リストを示す図である。
【００３３】
図４（ａ）と図４（ｂ）を比較すると判るように、縮約遷移リストでは、同じ遷移を起こすイベントが複数ある場合は、これらのイベントを集約してグループ化している。例えば、イベントＥ２、Ｅ３、及びＥ５によって同一遷移（Ｓ２→Ｓ１）と同一遷移（Ｓ３→Ｓ１）とが起こるため、イベントＥ２、Ｅ３、及びＥ５を１つのイベントグループ（Ｅ２、Ｅ３、Ｅ５）に集約している。同様に、イベントＥ１及びイベントＥ４によって同一遷移（Ｓ１→Ｓ４）と同一遷移（Ｓ４→Ｓ２）とが起こるため、イベントＥ１及びイベントＥ４を１つのイベントグループ（Ｅ１、Ｅ４）に集約している。
【００３４】
一方、遷移（Ｓ２→Ｓ３）を起こすイベントはＥ１のみであるため、遷移（Ｓ２→Ｓ３）に対応するイベントＥ１は、遷移（Ｓ２→Ｓ３）のみを関連付けて残している。同様に、遷移（Ｓ４→Ｓ２）を起こすイベントはＥ５のみであるため、遷移（Ｓ４→Ｓ２）に対応するイベントＥ５、遷移（Ｓ４→Ｓ２）のみを関連付けて残している。
【００３５】
フローチャート（図４）のステップＳＴ３からステップＳＴ９は、予備遷移リストから縮約遷移リストを生成する手順の具体例を示している。
【００３６】
ステップＳＴ３では、イベントごとに遷移の一致数を比較する。例えば、まず、イベントＥ１とイベントＥ２との間で、遷移の一致数を比較する。上述したように、イベントＥ１によって起こる遷移は（Ｓ１→Ｓ４）、（Ｓ２→Ｓ３）、及び（Ｓ４→Ｓ２）であり、イベントＥ２によって起こる遷移は、（Ｓ２→Ｓ１）及び（Ｓ３→Ｓ１）であるため、イベントＥ１とイベントＥ２の間での遷移の一致数はゼロである（ステップＳＴ４のＮＯ）。
【００３７】
そこで、ステップＳＴ８を経由してステップＳＴ３に戻り、イベントＥ１と次のイベントＥ３との間で遷移の一致数を比較する。この場合にも、一致する遷移は存在しないため、さらに、イベントＥ１と次のイベントＥ４との間で遷移の一致数をさらに比較する。
【００３８】
イベントＥ４によって起こる遷移は、（Ｓ１→Ｓ４）及び（Ｓ４→Ｓ２）である。これらの２つの遷移は、いずれもイベントＥ１によっても起こる遷移であり、イベントＥ１とイベントＥ４の間での遷移の一致数は２（１以上）となり（ステップＳＴ４のＹＥＳ）、ステップＳＴ５へ進む。
【００３９】
ステップＳＴ５では、イベントＥ１とイベントＥ２との間で総ての遷移が一致するか否かが判定される。今の例では、イベントＥ１で起こる遷移は、（Ｓ１→Ｓ４）、（Ｓ２→Ｓ３）、及び（Ｓ４→Ｓ２）であり、イベントＥ４で起こる遷移は、（Ｓ１→Ｓ４）及び（Ｓ４→Ｓ２）であるため、総ての遷移が一致しているわけではない（ステップＳＴ５のＮＯ）。そこで、ステップＳＴ７へ進む。
【００４０】
ステップＳＴ７では、遷移の一致するイベントをイベントグループとして集約し、一致しないイベントは、一致しない遷移のみを関連付けて残す。
【００４１】
今の例では、遷移（Ｓ１→Ｓ４）と遷移（Ｓ４→Ｓ２）の２つの遷移に関してはイベントＥ１とイベントＥ４とで一致しており、イベントＥ１、Ｅ４をイベントグループ（Ｅ１、Ｅ４）として集約する（ステップＳＴ６）。
【００４２】
一方、イベントＥ１の遷移（Ｓ２→Ｓ３）に関しては、イベントＥ１とイベントＥ４とで一致していないため、遷移（Ｓ２→Ｓ３）のみを関連付けたイベントＥ１を残す。
【００４３】
引き続きこのイベントＥ１と次のイベントＥ５との間で遷移の一致数を比較するが、一致する遷移は存在しないためイベントを集約することなく、次のイベント比較に進む。
【００４４】
次のイベント比較では、イベントＥ２とイベントＥ３、イベントＥ２とイベントＥ４、イベントＥ２とイベントＥ５とを順次比較していく。
【００４５】
イベントＥ２とイベントＥ３との間では、イベントＥ２によって起こる遷移（Ｓ２→Ｓ１）及び（Ｓ３→Ｓ１）と、イベントＥ３によって起こる遷移（Ｓ２→Ｓ１）及び（Ｓ３→Ｓ１）の一致数は２であり（ステップＳＴ４のＹＥＳ）、かつ、総ての遷移が一致している（ステップＳＴ５のＹＥＳ）。そこで、遷移（Ｓ２→Ｓ１）及び（Ｓ３→Ｓ１）に関してイベントＥ２とイベントＥ３をイベントグループ（Ｅ２、Ｅ３）として集約する。
【００４６】
イベントＥ２とイベントＥ４との間では一致する遷移は存在しない。一方、イベントＥ２とイベントＥ５との間では、総ての遷移（（Ｓ２→Ｓ１）、（Ｓ３→Ｓ１））が一致しており、イベントＥ２とイベントＥ５をイベントグループ（Ｅ２、Ｅ５）として集約することができる。さらに、イベントグループ（Ｅ２、Ｅ３）とイベントグループ（Ｅ２、Ｅ５）との間においても、総ての遷移（（Ｓ２→Ｓ１）、（Ｓ３→Ｓ１））が一致しているため、これら３つのイベントＥ２、Ｅ３、Ｅ５を１つのイベントグループ（Ｅ２、Ｅ３、Ｅ５）として集約する。
【００４７】
このような処理を、イベントの比較が総て完了するまで繰り返す（ステップＳＴ８）。この結果、同じ遷移を起こすイベントが複数ある場合は、これらのイベントがグループ化されて集約され、遷移数の縮約された縮約遷移リスト（図４（ｂ））が生成される（ステップＳＴ９）。
【００４８】
予備遷移リスト（図４（ａ））と、縮約遷移リスト（図４（ｂ））とを比較すると、遷移数が１２から６に大幅に減少していることがわかる。
【００４９】
生成された縮約遷移リストは、検査モデル生成装置２のコード変換部２３に出力される。コード変換部２３では、公知の検査モデル記述言語変換ツールを用いて、縮約遷移リストをモデル検査用記述言語（縮約された検査用モデルコード）に変換する（ステップＳＴ１０）。
【００５０】
また、縮約遷移リストを、縮約された状態遷移表として、モデル検査装置１が具備するディスプレイ装置や外部のプリンタ等に出力するようにしてもよい。
【００５１】
縮約された検査用モデルコードは、モデル検査装置１のモデル検査部１１に入力される。一方、検査用モデルコードが所定の検査条件を満たすか否かを検査するための検査式は、モデル検査装置１の検査式入力部１０から入力され、さらにモデル検査部１１に入力される。モデル検査部１１では、縮約された検査用モデルコードにおける状態遷移が検査条件を満たすか否かを検査式に基づいて検査し、状態遷移の中に検査条件を満たさない状態遷移を検出した場合は、その状態遷移を反例データとして出力すると共に、その状態遷移へ至る遷移系列をログデータとして出力する。
【００５２】
図５（ａ）は、予備遷移リストに対応する縮約前の状態遷移モデルを状態遷移図の形式で表現したものであり、状態Ｓ１、Ｓ２、Ｓ３、Ｓ４の遷移の方向が、矢印をもつパスで示され、遷移を起こす各イベントＥ１〜Ｅ５が各パスに付されている。
【００５３】
一方、図５（ｂ）は、縮約遷移リストに対応する縮約後の状態遷移モデルを状態遷移図の形式で表現したものである。集約されたイベントグループ（Ｅ１、Ｅ４）、（Ｅ２、Ｅ３、Ｅ５）に対しては夫々１つのパスが対応しており、パス数（即ち遷移数）が図５（ａ）と比べて１２から６に減少している。
【００５４】
図５（ａ）に示す縮約前の状態遷移モデルでは、同じ遷移（例えば、遷移（Ｓ３→Ｓ１））に対してもイベントの異なる複数のパスが割り付けられているのに対して、図５（ｂ）に示す縮約後の状態遷移モデルでは、同じ遷移（例えば、遷移（Ｓ３→Ｓ１））遷移に対しては、集約されたイベントグループ（例えば、イベントグループ（Ｅ２、Ｅ３、Ｅ５））の１つのパスが割り付けられている。
【００５５】
一般に、モデル検査においては、同じ遷移を異なるパスで検査することにあまり意味はなく、検査するパスが増えれば増えるほど、検査に必要となるデータの記憶量や検査に要する時間が長くなる。
【００５６】
図６（ａ）及び（ｂ）は、状態遷移モデルに対してモデル検査を行うときの状態数を、適宜の検査用モデルコードで示した一例である。
【００５７】
縮約前の検査用モデルコード（図６（ａ））では、例えば、イベントＥ２、イベントＥ３、イベントＥ５ごとに場合分けして分岐させ、各イベントで起こりうる総ての状態の遷移について網羅的に検査していく。従って、分岐数（即ちイベント数）が多くなると、検査すべき状態数も急激に増加していくことになり、場合によっては状態爆発の事象が発生してモデル検査の実行が事実上不可能になってしまうこともある。
【００５８】
これに対して、縮約された検査用モデルコード（図６（ｂ））では、イベントＥ２、イベントＥ３、及びイベントＥ５が集約された１つのイベントグループ（Ｅ２、Ｅ３，Ｅ５）に対して、イベントグループ（Ｅ２、Ｅ３，Ｅ５）で起こりうる状態の遷移についてのみ検査すればよいため、検査すべき状態の数は大幅に減少し、この結果、状態爆発の発生を抑制することが可能となる。
【００５９】
縮約された検査用モデルコードに対してモデル検査を行うことは、上記の状態爆発の抑制という利点のほか、モデル検査によって得られる反例の解析効率が向上するという利点も得られる。
【００６０】
縮約前の検査用モデルコードに対してモデル検査を行った場合、図７（ａ）に例示したように、イベントＡ、イベントＢ、イベントＣごとに反例が出力される。このため、同じ遷移に対する同じ反例であっても、夫々別の反例として出力される。その結果、総ての反例が出力されるまでに要する時間が長くなる。また、ユーザは出力された夫々の反例を確認して解析することになるため、解析に要する時間も長くなってしまう。
【００６１】
これに対して、縮約された検査用モデルコードに対してモデル検査を行うと、図７（ｂ）に例示したように、集約された１つのイベントグループ（Ａ、Ｂ、Ｃ）に対しては１つの反例が出力される。この結果、反例が出力されるまでの時間は短縮され、さらに反例の解析時間も短縮されることになる。
【００６２】
（２）第２の実施形態
状態の遷移はイベントの発生によって引き起こされるが、このとき何らかのアクションも同時に引き起こされる場合がある。アクションの種類は特に限定するものではないが、状態の遷移自体に影響を与えるアクションと、影響を与えないアクションとに大別される。以下では、状態の遷移に影響を与えるアクションを「指定アクション」と呼び、影響を与えないアクションを「非指定アクション」と呼ぶものとする。
【００６３】
第１の実施形態では、異なる複数のイベントであっても、それらのイベントによって引き起こされる遷移が同じ場合、異なる複数のイベントを１つのイベントグループとして集約することによって、縮約された状態遷移モデル（縮約遷移リスト）を生成している。
【００６４】
これに対して、第２の実施形態では、イベントによる状態遷移の際に引き起こされるアクションを考慮して縮約された状態遷移モデル（縮約遷移リスト）を生成するようにしている。具体的には、第２の実施形態では、（ａ）そのイベントによって起こされる遷移とこれに伴う指定アクションが同じ場合、（ｂ）そのイベントによって起こされる遷移が同じであり、かつ遷移に伴うアクションが非指定アクションである場合、又は、（ｃ）そのイベントによって起こされる遷移が同じであり、かつ遷移がアクションを伴わない場合には、複数の異なるイベントを１つのイベントグループとして集約して、縮約された状態遷移モデル（縮約遷移リスト）を生成している。
【００６５】
図８（ａ）は、第２の実施形態において生成される予備遷移リストの一例を示す図である。
【００６６】
第２の実施形態における予備遷移リストは、イベントごとに、そのイベントで起こる遷移とこの遷移に伴うアクションとが関連付けられている。図８（ａ）の例示では、イベントごとに、そのイベントで起こる遷移とこの遷移に伴うアクションとを上下２段のマスに示される変数によって関連付けている。
【００６７】
また各アクションの変数は、遷移に影響を与える指定アクションの変数と、遷移に影響を与えない非指定アクションの変数とが識別できるようになっている。図８（ａ）の例示では、Ｂ１、Ｂ２、及びＢ３が指定アクションに該当し、Ａ１、Ａ２、及びＡ３が非指定アクションに該当する。また、アクションを伴わない遷移も存在するが、図８（ａ）では、アクションを伴わない遷移であることを下段のマスの斜線で示している。
【００６８】
一方、図８（ｂ）は、この予備遷移リストから生成される縮約遷移リストを示す図である。第２の実施形態では、遷移が指定アクションを伴う場合、遷移と指定アクションの双方に着目し、遷移と指定アクションの双方が同じイベント同士を、その遷移と指定アクションに関して集約し、１つのイベントグループとする。
【００６９】
一方、遷移が非指定アクションを伴う場合や、アクションを伴わない場合には、遷移のみに着目し、遷移が同じイベント同士を、その遷移に関して集約し、１つのイベントグループとする。
【００７０】
図８（ａ）の例示する予備遷移リストでは、イベントＥ３とイベントＥ６の間で、遷移（Ｓ２→Ｓ３）と指定アクションＢ３が同じであり、また、アクションを伴わない遷移（Ｓ３→Ｓ１）が同じである。そこで、図８（ｂ）に示す縮約遷移リストでは、イベントＥ３とイベントＥ６を集約して、１つのイベントグループ（Ｅ３、Ｅ６）としている。但し、イベントＥ６における遷移（Ｓ４→Ｓ２）及び指定アクションＢ２は、イベントＥ３には存在しないため、遷移（Ｓ４→Ｓ２）及び指定アクションＢ２に関してはイベントＥ６をそのまま残している。
【００７１】
また、図８（ａ）の例示する予備遷移リストでは、イベントＥ２とイベントＥ５の間で、遷移（Ｓ２→Ｓ１）と遷移（Ｓ３→Ｓ１）とがいずれも同じである。そこで、図８（ｂ）に示す縮約遷移リストでは、イベントＥ２とイベントＥ５を集約して、１つのイベントグループ（Ｅ２、Ｅ５）としている。この場合、これらの遷移に伴うアクションはいずれも非指定アクション（Ａ１、Ａ２、Ａ３）であるため、これらの非指定アクションを無視して遷移のみで同一性を判断している。但し、イベントＥ５における遷移（Ｓ４→Ｓ２）及び指定アクションＢ１は、イベントＥ２には存在しないため、遷移（Ｓ４→Ｓ２）及び指定アクションＢ１のみが関連付けられたイベントＥ５を残している。
【００７２】
同様に、イベントＥ１とイベントＥ４の間では、遷移（Ｓ１→Ｓ４）と遷移（Ｓ４→Ｓ２）とがいずれも同じである。そこで、図８（ｂ）に示す縮約遷移リストでは、イベントＥ１とイベントＥ４を集約して、１つのイベントグループ（Ｅ１、Ｅ４）としている。但し、この場合にも、イベントＥ１における遷移（Ｓ２→Ｓ３）及び指定アクションＢ１は、イベントＥ４には存在しないため、遷移（Ｓ２→Ｓ３）及び指定アクションＢ１のみが関連付けられたイベントＥ１を残している。
【００７３】
このようなイベントの集約によって、縮約遷移リストにおける状態の遷移数は、１６から９まで減少されている。
【００７４】
図９は、第２の実施形態における検査モデル生成装置２の動作例を示すフローチャートである。
【００７５】
ステップＳＴ２１では、状態遷移モデルや状態、イベントの変数の他、遷移に伴うアクションに割り当てられた変数も入力する。
【００７６】
ステップＳＴ２２では、入力した状態遷移モデルや変数から図８（ａ）に該当する予備遷移リストを生成する。第２の実施形態に係る予備遷移リストでは、イベントごとに、そのイベントと遷移、及びアクションが関連付けられている。また、アクションは遷移に影響を与える指定アクションと影響を与えない非指定アクションとが識別されている。
【００７７】
ステップＳＴ２３からステップＳＴ２９は、予備遷移リストから縮約遷移リストを生成する処理であり、基本的な処理の内容は、第１の実施形態と同じ（図３のステップＳＴ３からステップＳＴ９）であるため、詳細な説明は省略する。但し、図９に示すフローチャートでは、指定アクションを伴う遷移を「アクション付き遷移」として表記し、非指定アクションを伴う遷移やアクションを伴わない遷移をいずれも単に「遷移」として表記している。そして、第１の実施形態が遷移の同一性のみに着目してイベントを集約していたのに対して、第２の実施形態では、イベントによる状態遷移の際に引き起こされるアクションを考慮して縮約された状態遷移モデル（縮約遷移リスト）を生成するようにしている。具体的には、第２の実施形態では、（ａ）そのイベントによって起こされる遷移とこれに伴う指定アクションが同じ場合（「アクション付き遷移」が同じ場合）、（ｂ）そのイベントによって起こされる遷移が同じであり、かつ遷移に伴うアクションが非指定アクションである場合（「遷移」が同じ場合）、又は、（ｃ）そのイベントによって起こされる遷移が同じであり、かつ遷移がアクションを伴わない場合（「遷移」が同じ場合）には、複数の異なるイベントを１つのイベントグループとして集約して、縮約された状態遷移モデル（縮約遷移リスト）を生成している。
【００７８】
第２の実施形態に係る検査モデル生成装置２では、第１の実施形態と同様に状態爆発を抑制し、反例解析の効率を向上させる検査用モデルコードを生成することが可能であり、さらに、遷移にアクションが伴う場合であっても、そのアクションによる遷移への影響が考慮された検査用モデルコードを生成することができる。
【００７９】
なお、本発明は上記の実施形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化できる。また、上記実施形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成できる。例えば、実施形態に示される全構成要素から幾つかの構成要素を削除してもよい。さらに、異なる実施形態にわたる構成要素を適宜組み合わせても良い。
【図面の簡単な説明】
【００８０】
【図１】モデル検査装置の一般的動作概念を示す図。
【図２】本発明の実施形態に係る検査モデル生成装置、及びモデル検査装置の構成例を示すブロック図。
【図３】第１の実施形態に係る検査用モデルコードの生成手順の一例を示すフローチャート。
【図４】第１の実施形態における予備遷移リストと縮約遷移リストの一例を示す図。
【図５】縮約前の状態遷移モデルと縮約後の状態遷移モデルの一例を状態遷移図として示す図。
【図６】縮約前の状態遷移モデルと縮約後の状態遷移モデルの一例を検査用モデルコードとして示す図。
【図７】縮約前と縮約後の状態遷移モデルに対してモデル検査を行った場合の反例の出力例を示す図。
【図８】第２の実施形態における予備遷移リストと縮約遷移リストの一例を示す図。
【図９】第２の実施形態に係る検査用モデルコードの生成手順の一例を示すフローチャート。
【符号の説明】
【００８１】
１  モデル検査装置
２  検査モデル生成装置
１０  検査式入力部
１１  モデル検査部
２０  モデル入力部
２１  予備リスト生成部
２２  縮約リスト生成部
２３  コード変換部
【図１】
2010140084.tif 000003
【図２】
2010140084.tif 000004
【図３】
2010140084.tif 000005
【図４】
2010140084.tif 000006
【図５】
2010140084.tif 000007
【図６】
2010140084.tif 000008
【図７】
2010140084.tif 000009
【図８】
2010140084.tif 000010
【図９】
2010140084.tif 000011