(57)【特許請求の範囲】
【請求項１】
モデル検査を実行して得た検証結果である反例に含まれる問題候補箇所を出力する反例解析支援装置であって、
モデル検査をした結果、検証条件を満たさなかった状態とイベントの遷移系列である反例を記憶する反例記憶手段と、
他状態に相関のある項目のリストであって、他状態を検出して発生するイベントである検出イベントと、この検出イベントの発生有無を決定する状態である被検出状態とを対応づけたリストである関連項目リストを記憶する関連項目リスト記憶手段と、
前記反例と、前記関連項目リストを用いて、反例の中から問題点である可能性のある箇所である問題候補箇所を出力する探索手段と
を有し、
前記探索手段は、
前記反例に含まれる状態が前記被検出状態であるか否かを判定し、
前記反例に含まれる状態が被検出状態である場合に、その被検出状態が次の状態に遷移する前に、関連項目リストに対応した検出イベントが発生しているか否かを判定し、その検出イベントが発生していないと判定した場合には、問題候補箇所の出力を行う
ことを特徴とする反例解析支援装置。
【請求項２】
前記探索手段は、前記被検出状態が次の状態に遷移する前に自状態側の遷移が完了しているか否かを判定し、前記自状態側の遷移が完了していないと判定した場合には、問題候補箇所の出力を行うことを特徴とする、請求項１に記載の反例解析支援装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、反例解析支援装置に関し、より詳しくはモデル検査を実行して得た検証結果である反例において、問題候補箇所を抽出する反例解析支援装置に関する。
【背景技術】
【０００２】
ソフトウェアが複雑化してきたことでこれまで以上に誤りが混入しやすくなり、さらに人の手では仕様を網羅した検証が困難になってきている。また、システムの設計段階で誤りが混入すると、経験や知識にない誤りは発見しづらい上に、後工程で発見されたものは取り除くために膨大なコストがかかる。そのため、仕様の誤りの早期発見及び仕様を網羅的に検証できる取り組みが必要不可欠になってきている。
【０００３】
このような問題を解決する手段として、組み込みシステムなど装置制御を主な目的とするソフトウェアを対象に、上流工程で不具合を早期発見する方法として、形式的手法の一つであるモデル検査が着目されている。
【０００４】
[モデル検査]
モデル検査とはシステムの仕様を状態遷移モデルで表現し、システムが満たすべき性質（検証条件）を論理式で記述し、状態遷移モデルが論理式を満たすかどうかを検証することで仕様の正しさを証明する手法である（例えば、特許文献１）。設計者が状態遷移モデルの作成を行い、必要な検証条件を洗い出した上でモデル検査を実行するとモデル検査器が網羅的にかつ自動的に検証し、検証条件を満たしているかどうかを検証する。もし、状態遷移モデルが検証条件を満たしていなければ、モデル検査器は、その状態に至る状態遷移系列を反例として出力する。この反例を解析し、モデルが検証条件を満たさない原因を突き止めることで仕様の不備を発見することが可能である。
【特許文献１】特開2002-324098号公開公報
【発明の開示】
【発明が解決しようとする課題】
【０００５】
上記の特許文献１では、ハードウェア記述言語で記述したソースを元に条件判定式に関係する情報を抜き出し、それを満たす集合と満たさない集合に分けてモデル検査を行う。この従来技術では、集合を分けることによりモデル検査で検証する回数も増加するため、複数の反例の発見の可能性が高まるとともに、検証対象を狭めているため反例に相当する箇所がどこであるか限定できるため開発者が理解しやすく見直しが容易になっている。
【０００６】
ただし、ハードウェア記述言語で既にソースが記述してあることが前提となっている。また、反例が出力される範囲は絞られるが反例の出力される内容は冗長であり、複数の条件分岐が影響する反例について検証ができない。
【０００７】
一般的に、反例の解析を人手により行う場合では、出力された反例を1ステップずつ辿り状態モデルや仕様と照らし合わせながら反例が出力された原因を探していくため
時間がかかるという問題がある。これは、辿る必要のない箇所もチェックする必要がある、検証条件を満たしていない箇所のすぐ近くに原因があるとは限らない、という特殊性があったためである。
【０００８】
本発明の目的は、状態モデルが設計されていれば検証可能であるとともに、冗長な反例においても反例内に含まれている状態遷移モデルで発生する問題点、問題候補箇所を抽出して検証作業を行うユーザの反例解読を支援する技術を提供することにある。
【課題を解決するための手段】
【０００９】
上記課題を解決するための手段として、本発明は以下の特徴を有している。  
本発明は、モデル検査を実行して得た検証結果である反例に含まれる問題候補箇所を出力する反例解析支援装置として提案される。
この反例解析支援装置は、モデル検査をした結果、検証条件を満たさなかった状態とイベントの遷移系列である反例を記憶する反例記憶手段と、他状態に相関のある項目のリストであって、他状態を検出して発生するイベントである検出イベントと、この検出イベントの発生有無を決定する状態である被検出状態とを対応づけたリストである関連項目リストを記憶する関連項目リスト記憶手段と、反例と、関連項目リストを用いて、反例の中から問題点である可能性のある箇所である問題候補箇所を出力する探索手段とを有し、探索手段は反例に含まれる状態が被検出状態であるか否かを判定し、反例に含まれる状態が被検出状態である場合に、その被検出状態が次の状態に遷移する前に、関連項目リストに対応した検出イベントが発生しているか否かを判定し、その検出イベントが発生していないと判定した場合には、問題候補箇所の出力を行うことを特徴としている。
【発明の効果】
【００１０】
本発明によれば、状態遷移モデルが設計されていればシステムの検証が可能であるとともに、冗長な反例においても反例内に含まれている、状態遷移モデルで発生する問題点である問題候補箇所を抽出して検証作業を行うユーザの反例解読を支援することができる。
【発明を実施するための最良の形態】
【００１１】
以下、図面を参照しながら本発明の実施の形態を説明する。  
［１．モデル検査］
まず、本実施の形態にかかる反例解析支援装置の処理対象となる反例、及びその反例を生成する処理であるモデル検査について説明する。
「モデル検査」とは、システムの仕様を状態遷移モデルで表現し、検証条件を論理式で記述し、状態遷移モデルが論理式を満たすかどうかを検証することで仕様の正しさを証明する手法である。設計者は状態遷移モデルの作成及び必要な検証条件を洗い出す必要がある。ここにいう「検証条件」とはシステムが満たすべき要求仕様である。
【００１２】
モデル検査を実行すると、モデル検査器が網羅的にかつ自動的に検証し、検証条件を満たしているかどうかを検証する。もし、状態遷移モデルが検証条件を満たしていなければ、モデル検査器は、その状態に至る状態遷移系列を反例として出力する。この反例を解析し、状態遷移モデルが検証条件を満たさない原因を突き止めることで、状態遷移モデルで表されたシステムの仕様の不備を発見することが可能となる。
【００１３】
図１は、モデル検査の流れを示す図である。モデル検査を実行する場合、モデル検証者は状態遷移モデル１０１を作成して、これをモデル検査器１０２に入力するとともに、検証条件１０３を作成し、これもモデル検査器１０２に入力する。モデル検査器１０２は、状態遷移モデル１０１に基づいて、このモデルの状態の遷移及びイベントの発生などを実行する装置であって、例えば、モデル検査を実行するプログラムがインストールされたコンピュータなどである。検証条件は、この状態遷移モデルで表されたシステムが満たさなければならない条件であって、例えば「プロセスＰ１とプロセスＰ２が同時に状態Ｓ５，Ｓ４にならない」という条件である。
【００１４】
モデル検査器１０２は、入力された状態遷移モデル１０１及び検証条件１０３に基づいて、モデル検査処理を実行し、検査結果１０４、及び検証条件が満たされない場合に反例１０５を出力する。
【００１５】
図２に、モデル検査器１０２が出力する反例１０５の出力例を示す。この反例１０５の出力例は、上部に検証条件１０３が示されており、その下に反例１０５の内容である状態、イベントの遷移系列が表示されている。
【００１６】
「反例」とは、モデル検査をした結果、検証条件を満たさなかった状態やイベントの遷移系列をログとして出力したものをいう。反例１０５は、「検証条件を満たさない」という事実を示す具体例を出力しているため、モデル検証者は、反例１０５が出力された原因（修正すべき箇所）を探し出す必要がある。反例１０５は、状態やイベントの遷移系列をシーケンシャルに出力したものであるため、可読性が低いので反例１０５から原因を探し出す処理を人手で行うと作業時間を要する。具体的には、モデル検証者は、必要な作業として、反例１０５が出力された根本的な原因を反例１０５から探し出し、その後原因となる箇所に対しどのように仕様を修正するか検討し、その検討結果に基づいて仕様を修正し再度モデル検査を実行するという作業を行う。
【００１７】
検査対象の状態遷移モデルにおいて、複数のプロセスが並行動作をするとき、実行タイミングのズレにより整合性がなくなる場合がある。このような場合には、プロセス単独の遷移をみた場合問題がないことが多く、問題原因箇所の発見に時間がかかる。
【００１８】
図３に、並行動作する複数のプロセスのプログラム例を示す。この例において、検証条件１０３は、プロセスＰ１の状態「Ｓｔａｔｅ＿ｐ１」及びプロセスＰ２の状態「Ｓｔａｔｅ＿ｐ２」が両方「Ａ」になってはならない、という内容であるものとする。図４は、上記の検証条件１０３が満たされるか検査するため、図３に示した２つのプロセスを並行動作させた場合、それぞれのプロセスの状態の遷移を示したテーブルである。図４のテーブルは、左列がプロセスのステップの実行順序を示し、中列がプロセスＰ１の状態を示し、右列がプロセスＰ２の状態を示している。
【００１９】
以下、図３，図４を参照しながらこの例におけるプロセスＰ１、プロセスＰ２の状態遷移を説明する。まず、プロセスＰ２のステップａが実行される。ステップａでは、プロセスＰ２の状態「Ｓｔａｔｅ＿ｐ２」に値”Ｓ”が代入され、状態「Ｓｔａｔｅ＿ｐ２」は”Ｓ”となる。このときプロセスＰ１の状態「Ｓｔａｔｅ＿ｐ１」は”Ｓ”である。
【００２０】
次に、プロセスＰ１のステップ１が実行される。すなわち、プロセスＰ１はプロセスＰ２の状態「Ｓｔａｔｅ＿ｐ２」の値を取得する。取得した状態「Ｓｔａｔｅ＿ｐ２」の値は”Ｓ”である。このときプロセスＰ１の状態「Ｓｔａｔｅ＿ｐ１」、プロセスＰ２の状態「Ｓｔａｔｅ＿ｐ１」はともに”Ｓ”のままである。
【００２１】
次に、プロセスＰ１のステップ２が実行される。具体的にはプロセス１は、プロセスＰ２の状態「Ｓｔａｔｅ＿ｐ２」が”Ｓ”であるか判断する。このときプロセスＰ１の状態「Ｓｔａｔｅ＿ｐ１」、プロセスＰ２の状態「Ｓｔａｔｅ＿ｐ２」はともに”Ｓ”のままである。
【００２２】
次に、プロセスＰ２のステップｂが実行される。具体的には、プロセスＰ２は、変数Ｘの値が"true"であるか判断する。このときプロセスＰ１の状態「Ｓｔａｔｅ＿ｐ１」、プロセスＰ２の状態「Ｓｔａｔｅ＿ｐ２」はともに”Ｓ”のままである。
【００２３】
次に、プロセスＰ１のステップ３が実行される。具体的には、プロセスＰ１の状態「Ｓｔａｔｅ＿ｐ１」に”Ａ”を代入する。このときプロセスＰ１の状態「Ｓｔａｔｅ＿ｐ１」は”Ａ”に遷移し、プロセスＰ２の状態「Ｓｔａｔｅ＿ｐ１」は”Ｓ”のままである。
【００２４】
次に、プロセスＰ２のステップｃが実行される。具体的には、プロセスＰ２はプロセスＰ２の状態「Ｓｔａｔｅ＿ｐ２」に”Ａ”を代入する。このときプロセスＰ１の状態「Ｓｔａｔｅ＿ｐ１」は”Ａ”であり、プロセスＰ２の状態「Ｓｔａｔｅ＿ｐ２」は”Ａ”に遷移する。従って検証条件１０３である、『プロセスＰ１の状態「Ｓｔａｔｅ＿ｐ１」及びプロセスＰ２の状態「Ｓｔａｔｅ＿ｐ２」が両方”Ａ”になってはならない』という条件に反した状態が発生している。この問題の発生原因は、プロセスＰ１が状態「Ｓｔａｔｅ＿ｐ２」を取得した後、状態「Ｓｔａｔｅ＿ｐ２」が変化しているという、実行タイミングのズレが発生しているためである。しかし、このような実行タイミングのズレを反例１０５から読み取ることは容易でなく、経験の乏しいモデル検証者が問題原因箇所を探すのは容易ではなかった。
【００２５】
［２．反例解析支援装置］
本実施の形態は、上記の反例１０５を解析し、反例１０５に含まれている問題候補箇所（問題の原因となっていると推測される箇所をいう）を提示し、反例解析の効率を向上させる装置である反例解析支援装置として提案される。なお、検証対象が複数の独立したモジュールであり、相関があること（並行プロセスなど）が、本実施の形態が適用できるための前提条件である。
【００２６】
反例解析支援装置は、演算処理装置（ＣＰＵ）、主メモリ（ＲＡＭ）、読出し専用メモリ（ＲＯＭ）、入出力装置（Ｉ／Ｏ）、必要な場合にはハードディスク装置等の外部記憶装置を具備している情報処理装置であって、例えばコンピュータ、ワークステーションなどの装置、あるいはマイクロコンピュータ（マイクロプロセッサ）などである。前記ＲＯＭ、若しくはハードディスク装置などに、情報処理装置を反例解析支援装置として機能させるプログラムが記憶されており、このプログラムを主メモリ上に載せ、ＣＰＵがこれを実行することにより反例解析支援装置が実現される。
【００２７】
図５に、反例解析支援装置の構成例を示す機能ブロック図を示す。図５に示した反例解析支援装置１は、本発明の反例記憶手段に相当する反例記憶部２と、本発明の関連項目リスト記憶手段に相当する関連項目リスト記憶部３と、反例記憶部２及び関連項目リスト記憶部３に接続された問題候補箇所探索部４（本発明の探索手段に相当する）と、問題候補箇所探索部４に接続された出力部５とを有している。なお、上記の問題候補箇所探索部４は、ＣＰＵがプログラムを実行することにより実現される構成要素であり、個別の回路や装置に相当しなくともかまわない。また、ここで「接続される」とは、データの受け渡しが行われる状態にあることを含む意味で用い、物理的な接続が行われることのみを意味しているのではない。
【００２８】
また、本実施の形態では、モデル検査器１０２と反例解析支援装置１とは別の装置として説明するが、同一のコンピュータがモデル検査器１０２及び反例解析支援装置１として機能する構成としてもかまわない。
【００２９】
以下、反例解析支援装置１の上記構成要素それぞれについて詳述する。
［２．１．反例記憶部］
反例記憶部２は、前述のモデル検査器１０２から出力された反例１０５を、問題候補箇所探索部４が読み取り可能なデータとして記憶する機能を有する。反例記憶部２は、主としてメモリやハードディスク記憶装置のような記憶装置によって構成されるが、反例１０５のデータを記憶した記憶媒体（ＣＤ，ＵＳＢメモリなど）であってもかまわない。
【００３０】
［２．２．関連項目リスト記憶部］
関連項目リスト記憶部３は、主としてメモリやハードディスク記憶装置のような記憶装置によって構成されるが、関連項目リストを記憶した記憶媒体（ＣＤ，ＵＳＢメモリなど）であってもかまわない。関連項目リスト記憶部３は、状態遷移表（状態遷移モデル１０１に対応する）から抜き出した、他状態に相関のある項目のリストである、関連項目リストを記憶する機能を有する。ここにいう「他状態」とは、複数のプロセスのうちあるプロセス（自プロセスと呼ぶ）とは別のプロセス（他プロセスと呼ぶ）の状態をいう。
【００３１】
関連項目リストは、状態遷移モデル１０１に対応する状態遷移表に基づいて、モデル検証者などによって作成される。
関連項目リストに納められる「他状態に相関のある項目」とは、以下の４つの項目である。
（１）他状態を検出して発生するイベント（以下、「検出イベント」と呼ぶ）
（２）そのイベントの発生有無を決定する状態（以下、「被検出状態」と呼ぶ）
（３）他状態に相関のあるイベント、すなわち検出イベントが発生する可能性のある自プロセスの状態（以下、「自状態と呼ぶ」）
（４）他状態に相関のあるイベント、すなわち検出イベントが発生した際に自プロセスの遷移先の状態（以下、「自状態遷移先」と呼ぶ）
次に、関連項目リストの作成方法について述べる。
【００３２】
図６は、状態遷移モデル１０１に基づいて作成される状態遷移表の一例を示す図である。「状態遷移表」とは、システムの振る舞いをイベントと状態の組み合わせにより表形式で表現したものをいい、イベントと状態のそれぞれの組み合わせに対して、動作(＝アクション)と状態の遷移先を記述する。
【００３３】
図６に示す状態遷移表は、３種類の状態「Ｓｔａｔｅ  Ａ」、「Ｓｔａｔｅ  Ｂ」、「Ｓｔａｔｅ  Ｃ」と３種類のイベント「異常発生」、「他プロセスの状態がＳｔａｔｅ  Ｘ」、「スイッチ切替」とで構成される表形式のデータである。３種類の状態６０１ー１から６０１ー３は３つの行に対応し、３種類のイベント６０２ー１から６０２−３は３つの列に対応する。
【００３４】
この状態遷移表は３行３列の計９個のセルを有する。「セル」とは、状態遷移表のマスをいう。各セルは、一つのイベントと一つの状態の組み合わせに対応する。各セルは、そのセルが含まれる行に対応する状態においてそのセルが含まれる列に対応するイベントが発生した場合の遷移先の状態及び／又は発生するアクションを格納している。ただし、状態の遷移が起こらない場合、及び／又はなんらのアクションも発生しない場合には、データは格納されない（このような場合は図において記号「-」で示した）。
【００３５】
モデル検証者は、状態遷移表から前述の「他状態に相関のある項目」を抽出する。図６に示した例では、被検出状態は、「Ｓｔａｔｅ  Ｘ」（図中参照符号６０３）に相当する。検出イベントはイベント６０２−２である「他プロセスの状態がＳｔａｔｅ  Ｘ」に相当する。自状態は、状態「Ｓｔａｔｅ  Ａ」（参照符号６０１−１）、及び状態「Ｓｔａｔｅ  Ｃ」（参照符号６０１−３）に相当する。また、自状態遷移先は、状態「Ｓｔａｔｅ  Ｄ」（参照符号６０４−１）、及び状態「Ｓｔａｔｅ  Ａ」（参照符号６０４−２）に相当する。
【００３６】
上記の「他状態に相関のある項目」のデータ表現が関連項目リストである。図７に、図６に示した状態遷移表から作成される関連項目リストの例を示す。図７に示すように、関連項目リストは、複数のレコード７００を有し、各レコード７００は、ＩＤ７０１、被検出状態７０２、検出イベント７０３、自状態７０４、自状態遷移先７０５という項目（フィールド）を有する。なおＩＤは他状態に相関のある項目のリスト番号である。
【００３７】
上記の関連項目リストはデータとして、関連項目リスト記憶部３に記憶され、問題候補箇所探索部４が問題候補箇所を探索する際に、問題候補箇所探索部４によって参照される。
【００３８】
［２．３．問題候補箇所探索部］
問題候補箇所探索部４は、反例記憶部２に記憶されている反例１０５と、関連項目リスト記憶部３に記憶されている関連項目リストを用いて、反例１０５の中から問題点である可能性のある箇所（問題候補箇所）を探索し、反例１０５と関連項目リストから解析した結果、問題原因の候補箇所として該当した部分である問題候補箇所を指摘するデータ（問題候補箇所指摘データと呼ぶ）を生成し、出力する。問題候補箇所探索部４の動作内容については、後述する。
【００３９】
［２．４．出力部］
出力部５は、前述の問題候補箇所探索部４が出力した問題候補箇所指摘データを、モデル検証者などのユーザ、オペレータが反例中の問題原因箇所を認識できる形態で出力する機能を有する。出力形態は、表示、印字、印刷、データ出力などどのようなものであってもかまわない。
【００４０】
出力部５による出力は、どのような表示形態であってもかまわないが、例えば、問題候補箇所探索部４が探索により特定した問題候補箇所を特定する情報を元に、解析結果として問題候補箇所に対応する反例の行番号を提示したレポートとして提供される。あるいは、反例の問題候補箇所に記号（例えば、＊）を付したものであってもかまわない。出力部５は、例えば、液晶ディスプレイ装置、プリンタ、記憶媒体への書き込み装置などである。
【００４１】
［３．反例解析支援装置の動作例］
次に、上記の反例解析支援装置１の動作例について説明する。
［３．１．設計者・システムの作業手順］
まず、反例解析支援装置１が問題候補箇所を出力するまでの処理の概略を説明する。  
（１）モデル検証者（システム設計者など）は、検証対象となるシステムの状態遷移モデル１０１及び検証条件１０３を作成し、モデル検査器１０２に入力する。モデル検査器１０２は、モデル検査を実行し、反例１０５を出力する。
（２）モデル検証者は、状態遷移モデル１０１から他状態に相関のある項目を抜き出して関連項目リストを作成する。
（３）モデル検証者は、反例１０５と「関連項目リスト」をそれぞれ反例解析支援装置１の反例記憶部２及び関連項目リスト記憶部３に記憶させる。
（４）モデル検証者は、反例解析支援装置１に反例における問題候補箇所の探索処理を実行させる。反例解析支援装置１は、反例と「関連項目リスト」を用いて問題候補箇所探索部４で問題候補箇所を探索する。
（５）反例解析支援装置１は、得られた問題候補箇所を指摘するレポート、例えば、得られた問題候補箇所に対応する反例テキストの該当行を出力する。
（６）モデル検証者は、反例解析支援装置１の出力したレポートに基づいて、状態遷移モデルの修正などを行う。
【００４２】
［３．２．問題候補箇所探索処理のアルゴリズム］
図８に、反例解析支援装置１の動作例に相当する反例解析処理の一例のフローチャートを掲げる。以下、図８を参照しながら反例解析支援装置１、より詳しくは問題候補箇所探索部４の動作例である反例解析処理について説明する。
【００４３】
まず、問題候補箇所探索部４は、反例記憶部２に記憶された反例１０５の1ステップずつ辿り、状態が変化するステップまで移動する（Ｓ１０）。この移動先のステップを検証対象ステップと呼ぶこととする。
【００４４】
次に、問題候補箇所探索部４は、検証対象ステップが示す状態が関連項目リストの被検出状態であるかを判断する（Ｓ２０）。検証対象ステップが示す状態が被検出状態でなければ（Ｓ２０，Ｎｏ）、反例１０５中の次のステップに移動する（Ｓ６０）。
【００４５】
次のステップに移動後、問題候補箇所探索部４は、反例１０５にそれ以降のステップがなく、反例探索が終了したか否かを判定する（Ｓ７０）。反例探索終了と判定した場合（Ｓ７０，Ｙｅｓ）は、問題候補箇所探索部４は問題候補箇所探索を終了する。一方、反例探索終了ではないと判定した場合（Ｓ７０，Ｎｏ）、問題候補箇所探索部４はＳ２０に戻り、移動先のステップを新たな検証対象ステップとし、その検証対象ステップの示す状態が被検出状態か否かの判定を行う（Ｓ２０）。
【００４６】
一方、Ｓ２０において、そのステップが示す状態が被検出状態であると判定した場合（Ｓ２０、Ｙｅｓ）、問題候補箇所探索部４は、その被検出状態が次の状態に遷移する前に、関連項目リストに対応したイベントが自状態側（自プロセス側）で発生しているか否かを判定する（Ｓ３０）。
【００４７】
そのようなイベントが発生していない場合は、状態の検出ができていないという問題があると考えられる。また、イベントが発生しているが関連項目リストに対応したイベントでない場合には、検出のタイミングがずれているという問題があると考えられる。
【００４８】
Ｓ３０において、関連項目リストに対応したイベントが自状態側（自プロセス側）で発生していなかったと判定した場合には、問題候補箇所探索部４は反例１０５のその箇所（ステップ）を問題候補箇所として記録する（Ｓ５０）。
【００４９】
一方、Ｓ３０において、関連項目リストに対応したイベントが自状態側（自プロセス側）で発生していたと判定した場合（Ｓ３０，Ｙｅｓ）、問題候補箇所探索部４は、被検出状態が次状態に遷移する前に自状態側の遷移が完了しているかを判定する（Ｓ４０）。自状態側（自プロセス側）の遷移が終わる前に他状態が別の状態に遷移している場合には、プロセス間の整合性が取れていないという問題があると考えられる。
【００５０】
さて、被検出状態が次の状態に遷移する前に自状態側（自プロセス側）の遷移が完了していると判定した場合（Ｓ４０、Ｙｅｓ）、問題候補箇所探索部４は、反例１０５中の次のステップに移動する（Ｓ６０）。
【００５１】
一方、Ｓ４０において、被検出状態が次状態に遷移する前に自状態側（自プロセス側）の遷移が完了していない、すなわち自状態の遷移が完了する前に被検出状態が次の状態に遷移していたと判定した場合（Ｓ４０、Ｎｏ）、問題候補箇所探索部４は、その箇所（ステップ）を問題候補箇所として記録し（Ｓ５０）、その後Ｓ６０に進む。
【００５２】
反例解析支援装置１は上記のＳ１０からＳ７０を繰り返し行い、反例中のすべてのステップについて問題候補箇所であるか否かを判定し、問題候補箇所と判定したステップについては、記録しておき、それら記録したステップについて出力部５に問題候補箇所としてレポートに出力させることになる。
【００５３】
［３．３．反例解析処理の具体例］
次に、上記図８を用いて説明した反例解析処理の具体例を、図９を参照しながら説明する。図９は反例解析処理のより具体的な処理内容を示すフローチャートである。
まず、問題候補箇所探索部４は、反例記憶部２に記憶された反例１０５の1ステップずつ辿り、状態が変化するステップまで移動する（Ｓ１１０）。この処理は図８のＳ１０に相当する。
【００５４】
次に、問題候補箇所探索部４は、検証対象ステップが示す状態が関連項目リストの被検出状態であるかを判断する（Ｓ１２０）。これは図８のＳ２０に相当する。検証対象ステップが示す状態が被検出状態でなければ（Ｓ１２０，Ｎｏ）、問題候補箇所探索部４は反例１０５中の次のステップに移動する（Ｓ１８０）。次のステップに移動後、問題候補箇所探索部４は、反例１０５にそれ以降のステップがなく、反例探索が終了したか否かを判定する（Ｓ１９０）。反例探索終了と判定した場合（Ｓ１９０，Ｙｅｓ）は、問題候補箇所探索部４は問題候補箇所探索を終了する。一方、反例探索終了ではないと判定した場合（Ｓ１９０，Ｎｏ）、問題候補箇所探索部４はＳ１２０に戻り、移動先のステップを新たな検証対象ステップとし、その検証対象ステップの示す状態が、関連項目リストに含まれる被検出状態のいずれかと一致するか否かの判定を行う（Ｓ２０）。
【００５５】
一方、Ｓ１２０において検証対象ステップが示す状態が被検出状態であると判定した場合（Ｓ１２０，Ｙｅｓ）、問題候補箇所探索部４は、検出した「被検出状態」に該当するプロセス側を他プロセスとし、他方あるいは別のプロセスを自プロセスとし、他プロセスの状態が「被検出状態」であり、かつ自プロセスの状態が「自状態」となっている関連項目リストの「ＩＤ」を絞り込んで特定する（Ｓ１３０）。
【００５６】
次に、問題候補箇所探索部４は、仕様で意図したイベントが発生しているかどうか調べるため、自プロセスにおいて次に発生しているイベントが、Ｓ１３０において特定したＩＤに対応する「検出イベント」と同一であるか判定する（Ｓ１４０）。特定したＩＤに対応する「検出イベント」と同一でないと判定した場合（Ｓ１４０，Ｎｏ）は、問題候補箇所探索部４は反例１０５のその箇所（ステップ）を問題候補箇所として記録し（Ｓ１７０）、その後Ｓ１８０，Ｓ１９０に進む。
【００５７】
一方、Ｓ１４０において、自プロセスにおいて次に発生しているイベントがＳ１３０において特定したＩＤに対応する「検出イベント」と同一であると判定した場合（Ｓ１４０，Ｙｅｓ）、適切なタイミングでイベントが発生しているかどうか調べるため、問題候補箇所探索部４は、関連項目リストの該当ＩＤに対応する「検出イベント」の発生時の他状態が「被検出状態」のままか否か、すなわち他状態が変化していないかどうかを判定する（Ｓ１５０）。Ｓ１５０の判定において、「検出イベント」発生時の他状態が「被検出状態」のままではないと判定した場合（Ｓ１５０、Ｎｏ）、問題候補箇所探索部４は反例１０５のその箇所（ステップ）を問題候補箇所として記録し（Ｓ１７０）、その後Ｓ１８０，Ｓ１９０に進む。
【００５８】
一方、Ｓ１５０において、「検出イベント」発生時の他状態が「被検出状態」のままであると判定した場合（Ｓ１５０、Ｙｅｓ）、自状態の遷移完了の際に他状態との整合性が取れているかどうか調べるため、問題候補箇所探索部４は、自プロセスが関連項目リストの該当ＩＤにおける「自状態遷移先」に遷移した時点での他状態が「被検出状態」かどうかを判定する（Ｓ１６０）。このとき、該当ＩＤにおける「自状態遷移先」に遷移した時点での他状態が「被検出状態」でないと判定した場合（Ｓ１６０，Ｎｏ）、問題候補箇所探索部４は反例１０５のその箇所（ステップ）を問題候補箇所として記録し（Ｓ１７０）、その後Ｓ１８０，Ｓ１９０に進む。
【００５９】
一方、Ｓ１６０において該当ＩＤにおける「自状態遷移先」に遷移した時点での他状態が「被検出状態」であると判定した場合（Ｓ１６０，Ｙｅｓ）、問題候補箇所探索部４は反例１０５中の次のステップに移動する（Ｓ１８０）し、その後前述のＳ１９０に進む。
【００６０】
反例解析支援装置１は上記のＳ１１０からＳ１９０を繰り返し行い、問題項目リストを参照しながら、反例中のすべてのステップについて問題候補箇所であるか否かを判定し、問題候補箇所と判定したステップについては、記録しておき、それら記録したステップについて出力部５に問題候補箇所としてレポートに出力させることになる。
【００６１】
次に、図１０，図１１を参照しながら図９に示した反例解析処理（反例解析支援装置１の動作）のさらに具体的な一例を説明する。図１０は、ある状態遷移モデルについてモデル検査器１０２が出力した反例１０５の内容を図解したシーケンス図であり、図１１は、図１０の反例１０５に対応する状態遷移モデルから作成された関連項目リストの例を示す図である。なお、反例１０５の前提となる検証条件１０３は「複数のプロセスで同時に状態”Ａｃｔｉｖｅ”にならない」であるものとする。
【００６２】
図１０に示す反例１０５では、２つのプロセスＰ１，Ｐ２が検証されている。
プロセスＰ１では、イベント「起動」が発生した後、状態が「Ｗａｋｅｕｐ」、「Ａｃｔｉｖｅ」、「Ｈａｌｔ」、「Ａｃｔｉｖｅ」の順に遷移している。また、このプロセスＰ１において、状態「Ｈａｌｔ」の後、検出イベント「他のプロセスの状態が”Ｓｔａｎｄｂｙ」が発生している。
【００６３】
一方、プロセスＰ２では、イベント「起動」が発生した後、状態が「Ｗａｋｅｕｐ」、「Ｓｔａｎｄｂｙ」、「Ａｃｔｉｖｅ」の順に遷移している。また、このプロセスＰ２において、状態「Ｗａｋｅｕｐ」の後、検出イベント「他のプロセスの状態が”Ａｃｔｉｖｅ”」が発生し、かつ状態「Ｓｔａｎｄｂｙ」の後、検出イベント「他のプロセスの状態が”Ｈａｌｔ”」が発生している。なお、これら状態の遷移、検出イベントの発生のタイミングや前後関係は図１０に示したとおりになっているものとする。
【００６４】
さて、反例解析支援装置１、より詳しくは問題候補箇所探索部４は、図９に示す反例解析処理を開始すると、まずプロセスＰ１の状態「Ｗａｋｅｕｐ」が、図１１に示す問題項目リスト中のいずれかの「被検出状態」の項目内容に該当するか否かを判定する（図９，Ｓ１２０参照）。図１１に示す問題項目リスト中の「被検出状態」には「Ｗａｋｅｕｐ」を含むレコードはないので、反例解析支援装置１、より詳しくは問題候補箇所探索部４は、次の状態であるプロセスＰ２の状態「Ｗａｋｅｕｐ」に移動する。
【００６５】
反例解析支援装置１、より詳しくは問題候補箇所探索部４は、プロセスＰ２の状態「Ｗａｋｅｕｐ」に移動し、プロセスＰ２の状態「Ｗａｋｅｕｐ」が、図１１に示す問題項目リスト中のいずれかの「被検出状態」の項目内容に該当するか否かを判定する（図９，Ｓ１２０参照）。先のプロセスＰ１の「Ｗａｋｅｕｐ」と同様に、図１１に示す問題項目リスト中の「被検出状態」には「Ｗａｋｅｕｐ」を含むレコードはないので、反例解析支援装置１、より詳しくは問題候補箇所探索部４は、次の状態であるプロセスＰ１の状態「Ａｃｔｉｖｅ」に移動する。
【００６６】
反例解析支援装置１、より詳しくは問題候補箇所探索部４は、プロセスＰ１の状態「Ａｃｔｉｖｅ」に移動し、これが図１１に示す問題項目リスト中のいずれかの「被検出状態」の項目内容に該当するか否かを判定する（図９，Ｓ１２０参照）。
【００６７】
関連項目リストの項目「被検出状態」が「Ａｃｔｉｖｅ」であるのは、ＩＤ「２」と「３」の２つのレコードがある。この場合反例解析支援装置１、より詳しくは問題候補箇所探索部４はいずれか一つのレコードに特定するため、自状態を調べる。図１０の例では、自状態はプロセスＰ２の状態に相当し、この場合は「Ｗａｋｅｕｐ」であるので、反例解析支援装置１、より詳しくは問題候補箇所探索部４は、項目「自状態」が「Ｗａｋｅｕｐ」であるＩＤ「２」のレコードを特定する（図９，Ｓ１３０参照）。
【００６８】
次に、反例解析支援装置１、より詳しくは問題候補箇所探索部４は自プロセスであるプロセスＰ２での検出イベントが、上記ＩＤ「２」の「検出イベント」に一致するか否かを判定する。図１０の例では、プロセスＰ２での検出イベント「他のプロセスの状態がＡｃｔｉｖｅ」がＩＤ「２」の「検出イベント」に一致すると判定する（図９，Ｓ１４０参照）。
【００６９】
次に、反例解析支援装置１、より詳しくは問題候補箇所探索部４は「検出イベント」発生時の他状態が「被検出状態」であるか否かをチェックする（図９，Ｓ１５０参照）。図１０の例では、プロセスＰ２における検出イベント「他のプロセスの状態がＡｃｔｉｖｅ」の発生時、プロセスＰ１の状態は「Ａｃｔｉｖｅ」であるので、反例解析支援装置１、より詳しくは問題候補箇所探索部４は次の判定に進む。
【００７０】
次に、反例解析支援装置１、より詳しくは問題候補箇所探索部４は、自プロセスであるプロセスＰ２が「自状態遷移先」に遷移したときの他状態が「被検出状態」であるかをチェックする（図９，Ｓ１６０参照）。この例では、プロセスＰ２が「自状態遷移先」である状態「Ｓｔａｎｄｂｙ」に遷移した時点において、他状態であるプロセスＰ１の状態は「Ａｃｔｉｖｅ」であり、これはＩＤ「２」における「被検出状態」に一致する。
【００７１】
よって反例解析支援装置１、より詳しくは問題候補箇所探索部４は、プロセスＰ１における状態「Ａｃｔｉｖｅ」、プロセスＰ２における検出イベント「他のプロセスの状態がＡｃｔｉｖｅ」、自状態遷移先であるプロセスＰ２での状態「Ｓｔａｎｄｂｙ」はいずれも問題箇所と判定せず、これらを問題候補箇所として記憶しない。
【００７２】
次に、反例解析支援装置１、より詳しくは問題候補箇所探索部４は反例１０５中の次のステップとなるプロセスＰ２の「Ｓｔａｎｄｂｙ」に移動し（図９，Ｓ１８０参照）、これが図１１に示す問題項目リスト中のいずれかの「被検出状態」の項目内容に該当するか否かを判定する（図９，Ｓ１２０参照）。関連項目リストの被検出状態が「Ｓｔａｎｄｂｙ」であるものはないので、なにもせずそのまま反例１０５中の次のステップとなるプロセスＰ１の「Ｈａｌｔ」に移動する。
【００７３】
反例解析支援装置１、より詳しくは問題候補箇所探索部４は、プロセスＰ１の「Ｈａｌｔ」が図１１に示す問題項目リスト中のいずれかの「被検出状態」の項目内容に該当するか否かを判定する（図９，Ｓ１２０参照）。関連項目リストの項目「被検出状態」が「Ｈａｌｔ」であるのは、ＩＤ「１」のレコードである。次に、反例解析支援装置１、より詳しくは問題候補箇所探索部４は自状態を調べる。図１０の例では、自状態はプロセスＰ２の状態に相当し、この場合は「Ｓｔａｎｄｂｙ」であるので、反例解析支援装置１、より詳しくは問題候補箇所探索部４は、ＩＤ「１」のレコードを特定する（図９，Ｓ１３０参照）。
【００７４】
次に、反例解析支援装置１、より詳しくは問題候補箇所探索部４は自プロセスであるプロセスＰ２での検出イベントが、上記ＩＤ「１」の「検出イベント」に一致するか否かを判定する。図１０に示した例では、プロセスＰ２での検出イベントは、「他のプロセスの状態がＨａｌｔ」である。反例解析支援装置１、より詳しくは問題候補箇所探索部４はプロセスＰ２での検出イベント「他のプロセスの状態がＨａｌｔ」は、ＩＤ「１」の「検出イベント」に一致すると判定する（図９，Ｓ１４０参照）。
【００７５】
次に、反例解析支援装置１、より詳しくは問題候補箇所探索部４は「検出イベント」発生時の他状態が「被検出状態」であるか否かをチェックする（図９，Ｓ１５０参照）。図１０の例では、プロセスＰ２における検出イベント「他のプロセスの状態がＨａｌｔ」の発生時、プロセスＰ１の状態は「Ｈａｌｔ」であるので、反例解析支援装置１、より詳しくは問題候補箇所探索部４は判定条件を満たすと判定し、次の判定に進む。
【００７６】
次に、反例解析支援装置１、より詳しくは問題候補箇所探索部４は、「自状態遷移先」に遷移したときの他状態が「被検出状態」であるかをチェックする（図９，Ｓ１６０参照）。この例では、プロセスＰ２が「自状態遷移先」である状態「Ａｃｔｉｖｅ」に遷移した時点において、他状態であるプロセスＰ１の状態は「Ｈａｌｔ」であり、これはＩＤ「１」における「被検出状態」に一致する。
【００７７】
よって反例解析支援装置１、より詳しくは問題候補箇所探索部４は、プロセスＰ１における状態「Ａｃｔｉｖｅ」、プロセスＰ２における検出イベント「他のプロセスの状態がＡｃｔｉｖｅ」、自状態遷移先であるプロセスＰ２での状態「Ｓｔａｎｄｂｙ」はいずれも問題候補箇所とは判定せず、これらを問題候補箇所として記憶しない。
【００７８】
次に、反例解析支援装置１、より詳しくは問題候補箇所探索部４は、次の状態であるプロセスＰ２の状態「Ａｃｔｉｖｅ」に移動する。
関連項目リストの項目「被検出状態」が「Ａｃｔｉｖｅ」であるのは、ＩＤ「２」と「３」の２つのレコードがある。この場合反例解析支援装置１、より詳しくは問題候補箇所探索部４は自状態に相当するプロセスＰ１の状態を調べる。図１０の例では、自状態であるプロセスＰ１の状態は「Ｈａｌｔ」であるので、反例解析支援装置１、より詳しくは問題候補箇所探索部４は、ＩＤ「３」のレコードを特定する（図９，Ｓ１３０参照）。
【００７９】
次に、反例解析支援装置１、より詳しくは問題候補箇所探索部４は他プロセスであるプロセスＰ１での検出イベントが、上記ＩＤ「３」の「検出イベント」に一致するか否かを判定するが、プロセスＰ１では上記ＩＤ「３」の「検出イベント」に一致する「他プロセスの状態がＡｃｔｉｖｅ」という検出イベントは発生していない。その代わりに「他のプロセスの状態がＳｔａｎｄｂｙ」という検出イベントが発生している。これは、プロセスＰ１における相手状態の検出タイミングのズレにより、プロセスＰ２のＡｃｔｉｖｅの状態を検出できなかったためと考えられる。
【００８０】
よって、反例解析支援装置１、より詳しくは問題候補箇所探索部４はこの箇所（プロセスＰ１の「他のプロセスの状態がＳｔａｎｄｂｙ」という検出イベント、あるいはプロセスＰ２の状態「Ａｃｔｉｖｅ」、又はこれらの双方）を問題候補箇所として記憶し、反例検証終了後、出力部５にその旨を出力させる。
【００８１】
このように、反例解析支援装置１は、反例１０５に含まれる問題候補箇所を探索して該当仮称を出力することにより、モデル検証者の反例解析を支援することができる。
【００８２】
［４．利点］
本発明の利点を以下に列挙する。
（１）本発明によれば、実行タイミングの微妙なズレなどによって生じるものなど人が発見しにくい部分であっても、反例に含まれる問題の候補箇所の提示が可能となる。
（２）本発明によれば、反例解析の知識や経験がなくても反例出力の要因となり得る箇所を機械的に提示することで不具合の特定がしやすくなる。
（３）本発明によれば、反例が出力された原因の候補箇所を機械的に提示することで、反例解析の検討箇所を絞り込むことができる。これにより反例解析にかかっていたコストを削減することができる。
【図面の簡単な説明】
【００８３】
【図１】一般的なモデル検査の流れを示す図
【図２】モデル検査器が出力する反例の出力例を示す図
【図３】並行動作する複数のプロセスのプログラム例を示す図
【図４】２つのプロセスを並行動作させた場合、それぞれのプロセスの状態の遷移を示したテーブルを示す図
【図５】反例解析支援装置の構成例を示す機能ブロック図
【図６】状態遷移モデルに基づいて作成される状態遷移表の一例を示す図
【図７】図６に示した状態遷移表から作成される関連項目リストの例を示す図
【図８】反例解析支援装置の動作例に相当する反例解析処理の一例のフローチャート
【図９】反例解析処理のより具体的な処理内容を示すフローチャート
【図１０】ある状態遷移モデルについてモデル検査器が出力した反例の内容を図解したシーケンス図
【図１１】図６の反例に対応する状態遷移モデルから作成された関連項目リストの例を示す図
【符号の説明】
【００８４】
１    …  反例解析支援装置
２    …  反例記憶部
３    …  関連項目リスト記憶部
４    …  問題候補箇所探索部
５    …  出力部
【図１】
0004477054.tif 000002
【図２】
0004477054.tif 000003
【図３】
0004477054.tif 000004
【図４】
0004477054.tif 000005
【図５】
0004477054.tif 000006
【図６】
0004477054.tif 000007
【図７】
0004477054.tif 000008
【図８】
0004477054.tif 000009
【図９】
0004477054.tif 000010
【図１０】
0004477054.tif 000011
【図１１】
0004477054.tif 000012