(57)【要約】【課題】モデル検査における反例の分析を効率化する。【解決手段】反例処理装置２００は、反例記憶部２１０、及び、簡約部２２０を含む。反例記憶部２１０は、システムに係る複数の要素の状態の集合であるシステム状態の、検証性質５２０の違反が検出されるまでの遷移系列を示す反例５４０を記憶する。簡約部２２０は、反例５４０から、検証性質５２０の違反が検出された要素と、当該要素の検証性質５２０に違反した状態に影響した可能性がある要素とを、解析対象の要素として抽出し、当該抽出された解析対象の要素の状態の遷移系列を関連付けて出力する。【選択図】図１
2016014959.tif 000002
【特許請求の範囲】
【請求項１】
システムに係る複数の要素の状態の集合であるシステム状態の、所定の検証性質の違反が検出されるまでの遷移系列を示す反例を記憶する反例記憶手段と、
前記反例から、前記検証性質の違反が検出された要素と、当該要素の当該検証性質に違反した状態に影響した可能性がある要素とを、解析対象の要素として抽出し、当該抽出された解析対象の要素の状態の遷移系列を関連付けて出力する簡約手段と、
を備えた情報処理装置。
【請求項２】
前記システム状態の遷移は、前記システムに係る複数の要素の内の、一の要素から他の要素に通知されたイベントにより、当該他の要素の状態が変化することにより発生し、
前記反例は、前記システム状態の遷移系列と当該遷移系列の各遷移に係るイベントを表し、
前記簡約手段は、さらに、前記反例から、前記検証性質の違反が検出された要素の当該検証性質に違反した状態に影響した可能性があるイベントを、解析対象のイベントとして抽出し、前記解析対象の要素の状態の遷移系列と関連付けて出力する、
請求項１に記載の情報処理装置。
【請求項３】
前記反例は、前記システム状態の遷移系列の各遷移に係るイベントの通知元、及び、通知先を含み、
前記簡約手段は、前記検証性質の違反が検出された要素を前記解析対象の要素に設定し、前記反例における前記システム状態の遷移系列上で、前記検証性質の違反が検出されたシステム状態から、当該システム状態より前の方向に、前記解析対象の要素の状態を変化させたイベントの検出、当該検出されたイベントの通知元である要素の前記解析対象の要素への追加、及び、当該検出されたイベントの前記解析対象のイベントへの追加を繰り返すことにより、前記解析対象の要素、及び、前記解析対象のイベントを抽出する、
請求項２に記載の情報処理装置。
【請求項４】
システムに係る複数の要素の状態の集合であるシステム状態の、所定の検証性質の違反が検出されるまでの遷移系列を示す反例を記憶し、
前記反例から、前記検証性質の違反が検出された要素と、当該要素の当該検証性質に違反した状態に影響した可能性がある要素とを、解析対象の要素として抽出し、当該抽出された解析対象の要素の状態の遷移系列を関連付けて出力する、
反例処理方法。
【請求項５】
前記システム状態の遷移は、前記システムに係る複数の要素の内の、一の要素から他の要素に通知されたイベントにより、当該他の要素の状態が変化することにより発生し、
前記反例は、前記システム状態の遷移系列と当該遷移系列の各遷移に係るイベントを表し、
さらに、前記反例から、前記検証性質の違反が検出された要素の当該検証性質に違反した状態に影響した可能性があるイベントを、解析対象のイベントとして抽出し、前記解析対象の要素の状態の遷移系列と関連付けて出力する、
請求項４に記載の反例処理方法。
【請求項６】
前記反例は、前記システム状態の遷移系列の各遷移に係るイベントの通知元、及び、通知先を含み、
前記検証性質の違反が検出された要素を前記解析対象の要素に設定し、
前記反例における前記システム状態の遷移系列上で、前記検証性質の違反が検出されたシステム状態から、当該システム状態より前の方向に、前記解析対象の要素の状態を変化させたイベントの検出、当該検出されたイベントの通知元である要素の前記解析対象の要素への追加、及び、当該検出されたイベントの前記解析対象のイベントへの追加を繰り返すことにより、前記解析対象の要素、及び、前記解析対象のイベントを抽出する、
請求項５に記載の反例処理方法。
【請求項７】
コンピュータに、
システムに係る複数の要素の状態の集合であるシステム状態の、所定の検証性質の違反が検出されるまでの遷移系列を示す反例を記憶し、
前記反例から、前記検証性質の違反が検出された要素と、当該要素の当該検証性質に違反した状態に影響した可能性がある要素とを、解析対象の要素として抽出し、当該抽出された解析対象の要素の状態の遷移系列を関連付けて出力する、
処理を実行させるプログラム。
【請求項８】
前記システム状態の遷移は、前記システムに係る複数の要素の内の、一の要素から他の要素に通知されたイベントにより、当該他の要素の状態が変化することにより発生し、
前記反例は、前記システム状態の遷移系列と当該遷移系列の各遷移に係るイベントを表し、
さらに、前記反例から、前記検証性質の違反が検出された要素の当該検証性質に違反した状態に影響した可能性があるイベントを、解析対象のイベントとして抽出し、前記解析対象の要素の状態の遷移系列と関連付けて出力する、
処理を実行させる請求項７に記載のプログラム。
【請求項９】
前記反例は、前記システム状態の遷移系列の各遷移に係るイベントの通知元、及び、通知先を含み、
前記検証性質の違反が検出された要素を前記解析対象の要素に設定し、
前記反例における前記システム状態の遷移系列上で、前記検証性質の違反が検出されたシステム状態から、当該システム状態より前の方向に、前記解析対象の要素の状態を変化させたイベントの検出、当該検出されたイベントの通知元である要素の前記解析対象の要素への追加、及び、当該検出されたイベントの前記解析対象のイベントへの追加を繰り返すことにより、前記解析対象の要素、及び、前記解析対象のイベントを抽出する、
処理を実行させる請求項８に記載のプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、情報処理装置、反例表示方法、及び、プログラムに関し、特に、モデル検査により得られた反例を出力する、情報処理装置、反例表示方法、及び、プログラムに関する。
【背景技術】
【０００２】
システムやコンピュータプログラムが正しく動作するかどうかを仕様に照らして自動的に判定する仕組みとして、モデル検査法が知られている。モデル検査法では、検証対象となるシステムやコンピュータプログラムの動作仕様を状態遷移系で表現したモデルと、このモデルが満たすべき性質である検証性質と、を用いて、モデルの取りうる状態遷移を網羅的、器械的に検証する。モデル検査法による典型的な検証対象として、複数の動作主体が同時並行的に動作する、並列システムが挙げられる。例えば、ＳＰＩＮ（Simple Promela Interpreter）モデル検査器は、通信機器や並列プロセス、並列スレッドといった、並行動作する検査対象の動作を、ＰＲＯＭＥＬＡ（Process Meta Language）と呼ばれる専用のモデル記述言語で記述、モデル化する。そして、ＳＰＩＮモデル検査器は、モデル中の動作主体の通信のパタンを網羅的に検査することで、システムが、例えば「デッドロックを起こすことはない」といった検証性質を満たすかどうかを検証する。
【０００３】
モデル検査法の特徴の一つに、モデルの状態遷移が検証性質に違反した場合に、初期状態から違反が検出された状態へ至る状態遷移列を反例として得ることができる、という点が挙げられる。反例により、初期状態から違反が検出された状態に至る、モデル上、起こりうる状態遷移の経路が具体的に提示される。したがって、検証対象のシステムが適切にモデル化されていれば、反例により提示される状態遷移の経路は、実際のシステムでも起こりうる、不正な状態に至る状態遷移の経路を具体的に示している。そのため、システムやコンピュータプログラムの動作のモデル検査を用いた検証において、生成された反例を分析することで、設計上のミスや、コーディング上のバグ等を特定することができる。
【０００４】
しかしながら、一般に、モデル検査法により得られる反例は、モデルが複雑な場合、すなわち、検証対象のシステムを構成する各要素が複雑な状態遷移をする、あるいは、検証対象のシステムが多くの並行動作する要素を含む場合、膨大となる。このような膨大な反例は、設計上のミス等を分析する上で、実用上大きな問題となる。また、反例はあくまで検証性質を満たさない状態と、その状態への状態遷移の経路を示すものであり、不具合そのものではない。仮に不具合が一つであっても、検証性質を満たさない状態は、複数存在する可能性がある。また、ある検証性質を満たさない状態に至る状態遷移の経路も、複数存在する可能性がある。検証性質を満たさない状態に至る状態遷移における、設計上あるいはコーディング上の不具合の特定は、通常、人手で行われるが、膨大な反例の人手による解析は大変な労力を伴う。
【０００５】
このような反例の解析を効率化する技術の一例が、例えば、特許文献１に開示されている。特許文献１に記載の反例解析支援装置では、他プロセスの状態、自プロセスの検出イベント、及び、自プロセスの状態が関連づけられた、関連項目リストが、利用者により設定される。反例解析支援装置は、関連項目リストをもとに、検出イベントの発生有無を判定し、反例の状態遷移列における問題候補箇所を特定する。
【０００６】
なお、関連技術として、特許文献２には、反例から、モジュールに挿入された検証コードのステップを削除するモデル検査装置が記載されている。また、特許文献３、特許文献４には、システムの変数群の状態遷移として、木構造で表された状態遷移を用いるモデル検査装置が記載されている。
【先行技術文献】
【特許文献】
【０００７】
【特許文献１】特許第４４７７０５４号公報
【特許文献２】特開２０１３−２０６３１０号公報
【特許文献３】特開２０１３−２００７８７号公報
【特許文献４】特開２０１２−１５５５１７号公報
【発明の概要】
【発明が解決しようとする課題】
【０００８】
しかしながら、特許文献１に記載の技術では、利用者が、システムの状態遷移モデルから関連項目リストを生成し、設定する必要があった。また、検出イベントのタイミング等に係る不具合の特定は効率化されるが、他の要因に係る不具合の特定は効率化されない可能性があった。
【０００９】
本発明の目的は、上述した課題を解決し、モデル検査における反例の分析を効率化する、情報処理装置、反例表示方法、及び、プログラムを提供することにある。
【課題を解決するための手段】
【００１０】
本発明の情報処理装置は、システムに係る複数の要素の状態の集合であるシステム状態の、所定の検証性質の違反が検出されるまでの遷移系列を示す反例を記憶する反例記憶手段と、前記反例から、前記検証性質の違反が検出された要素と、当該要素の当該検証性質に違反した状態に影響した可能性がある要素とを、解析対象の要素として抽出し、当該抽出された解析対象の要素の状態の遷移系列を関連付けて出力する簡約手段と、を備える。
【００１１】
本発明の反例処理方法は、システムに係る複数の要素の状態の集合であるシステム状態の、所定の検証性質の違反が検出されるまでの遷移系列を示す反例を記憶し、前記反例から、前記検証性質の違反が検出された要素と、当該要素の当該検証性質に違反した状態に影響した可能性がある要素とを、解析対象の要素として抽出し、当該抽出された解析対象の要素の状態の遷移系列を関連付けて出力する。
【００１２】
本発明のプログラムは、コンピュータに、システムに係る複数の要素の状態の集合であるシステム状態の、所定の検証性質の違反が検出されるまでの遷移系列を示す反例を記憶し、前記反例から、前記検証性質の違反が検出された要素と、当該要素の当該検証性質に違反した状態に影響した可能性がある要素とを、解析対象の要素として抽出し、当該抽出された解析対象の要素の状態の遷移系列を関連付けて出力する、処理を実行させる。
【発明の効果】
【００１３】
本発明の効果は、モデル検査における反例の分析を効率化できることにある。
【図面の簡単な説明】
【００１４】
【図１】本発明の実施の形態の特徴的な構成を示すブロック図である。
【図２】本発明の実施の形態における、モデル検査システムの構成を示すブロック図である。
【図３】本発明の実施の形態における、コンピュータにより実現された反例処理装置２００の構成を示すブロック図である。
【図４】本発明の実施の形態における、反例処理装置２００の動作を示すフローチャートである。
【図５】本発明の実施の形態における、反例５４０の例を示す図である。
【図６】本発明の実施の形態における、反例トレース５５０の例を示す図である。
【図７】本発明の実施の形態における、簡約化された反例トレース５６０の例を示す図である。
【発明を実施するための形態】
【００１５】
本発明の実施の形態について説明する。
【００１６】
はじめに、本発明の実施の形態における、モデル検査について説明する。
【００１７】
本発明の実施の形態のモデル検査においては、検査対象のシステム（以下、対象システムとも記述する）の仕様が、状態遷移系として表現される。また、検証性質が時相論理式で表現される。
【００１８】
モデル検査のアルゴリズムでは、対象システムの状態（以下、システム状態とも記述する）の状態遷移が有限であれば、時相論理で表現された論理式が成り立つかどうかを判定できる。つまり、システム状態が検証性質を満たすかどうか、もし満たなさない場合にはどのような状態遷移を経て違反したシステム状態に至るかが、具体的に示される。
【００１９】
実際には、システム状態の状態遷移は無限であることも多いため、状態遷移が有限であることを仮定したモデル検査を直接適用できない場合も多い。また、状態遷移が有限であっても、状態遷移の規模が大きいために、現実的な時間内で検証ができない場合も多い。そのような場合には、状態遷移系を必要に応じて拡張しながら、状態探索を一定の範囲まで行う有界モデル検査（Bounded Model Checking）が用いられてもよい。有界モデル検査では、状態遷移の探索空間において遷移が無限になる場合には、その探索を有限の範囲で打ち切る。そのため、実際には、検証性質を満たさない状態が存在しても、その状態を見つけられない可能性がある。しかしながら、有限の探索の範囲で検証性質を満たさないシステム状態が見つかる場合は、通常のモデル検査法と同様に反例を出力できる。
【００２０】
本発明の実施の形態は、有限の状態遷移を仮定した通常のモデル検査、及び、状態探索を有限で打ち切ることで無限の状態遷移も許容する有界モデル検査の内のどちらが用いられてもよい。以降、これらを区別せず、単にモデル検査と記載する。
【００２１】
次に、本発明の実施の形態の構成について説明する。
【００２２】
図２は、本発明の実施の形態における、モデル検査システムの構成を示すブロック図である。
【００２３】
図２を参照すると、本発明のモデル検査システムは、モデル検査装置１００、及び、反例処理装置２００を含む。
【００２４】
モデル検査装置１００は、モデル検査により、検証性質５２０に違反するシステム状態が検出された場合に、反例５４０を生成する。
【００２５】
モデル検査装置１００は、モデル生成部１１０、及び、モデル検査部１２０を含む。
【００２６】
モデル検査装置１００には、利用者により、対象システムのモデル記述５１０、及び、検証性質５２０が入力される。
【００２７】
モデル生成部１１０は、モデル記述５１０を用いて、システム状態の状態遷移に基づくモデルを作成する。
【００２８】
モデル検査部１２０は、システム状態の状態遷移を網羅的に探索し、検証性質５２０に違反するシステム状態を検出する。モデル検査部１２０は、検証性質５２０に違反するシステム状態が無い場合、その旨を示す検査結果５３０を利用者に出力する。また、モデル検査部１２０は、検証性質５２０に違反するシステム状態が存在する場合、反例５４０を含む検査結果５３０を、反例処理装置２００へ出力する。反例５４０は、検証性質５２０に違反するシステム状態に至る状態遷移の遷移系列を示す。
【００２９】
モデル記述５１０は、モデル検査装置１００を実現するためのプログラム（または、ツール）ごとにさまざまであるが、典型的には、簡単なプログラミング言語風の記述により与えられる。また、検証性質５２０も、モデル検査装置１００を実現するためのプログラムごとにさまざまであるが、典型的には、時相論理で表現された条件により与えられる。例えば、検証性質５２０は、「一旦、性質Ｘが満たされれば、以降の状態遷移の各状態において、性質Ｙが成り立つことはない」のような、時間的性質で記述される。
【００３０】
また、反例５４０は、典型的には、モデル検査の結果得られた、検証性質５２０を満たさないシステム状態と、そこに至る状態遷移の系列と、を含むログとして出力される。
【００３１】
図５は、本発明の実施の形態における、反例５４０の例を示す図である。
【００３２】
ここでは、対象システムの構成要素（または、単に、要素）であるノードとして、Ｈｏｓｔ１、Ｃｏｎｔｒｏｌｌｅｒ、Ｓｗｉｔｃｈ１、Ｓｗｉｔｃｈ２、Ｓｗｔｃｈ３、Ｓｗｔｉｃｈ４、及び、Ｈｏｓｔ２が並列に動作していると仮定する。以下、Ｈｏｓｔ１、Ｃｏｎｔｒｏｌｌｅｒ、Ｓｗｉｔｃｈ１、Ｓｗｉｔｃｈ２、Ｓｗｔｃｈ３、Ｓｗｔｉｃｈ４、及び、Ｈｏｓｔ２を、それぞれ、Ｈ１、ＣＮＴ、ＳＷ１、ＳＷ２、ＳＷ３、ＳＷ４、及び、Ｈ２とも記載する。
【００３３】
また、システム状態は、ノードの状態の集合で表され、システム状態間の状態遷移は、二つのノード間で通知されるイベントにより、少なくとも通知先のノードの状態が変化することにより発生すると仮定する。
【００３４】
図５の例では、各システム状態とシステム状態間の状態遷移を発生させるイベントとを示す行が、交互に配置されている。
【００３５】
また、システム状態を示す行において、各列は、対応するノードの状態を示す。ここで、ノードＨ１、ＣＮＴの状態は、「メッセージのキュー」で表されている。また、ノードＳＷ１〜４の状態は、「メッセージのキュー」と「メッセージの配送ルールの集合」との組として表されている。例えば、システム状態Ｓ４におけるノードＳＷ１の状態「｛ｐ１｝，｛Ｈ２→ＳＷ２｝」は、メッセージのキューにメッセージｐ１が存在し、メッセージの配送ルールが「Ｈ２宛てのメッセージは、一旦、ＳＷ２に送る」であることを示す。
【００３６】
また、イベントを示す行において、矢印の元がイベントの通知元のノード、矢印の先がイベントの通知先のノードを示す。例えば、イベントｐ１は、ノードＨ１からＳＷ１へのイベントを示す。
【００３７】
また、検証性質５２０は、「ノードＳＷ１〜４の各々において、同一のメッセージが同じノードを通過する（同じメッセージが同じノードに再度転送され、無限にループする）ことはない」であると仮定する。
【００３８】
図５の例では、システム状態が、Ｓ１からＳ５まで遷移した後に、Ｓ１１で、ノードＳＷ２に配送ルール｛Ｈ２→ＳＷ１｝が追加されている。さらに、システム状態が、Ｓ２１からＳ２３まで遷移した後に、Ｓ２４で、ノードＳＷ１にシステム状態Ｓ２２で通過したメッセージと同じメッセージｐ２が存在している。すなわち、システム状態Ｓ２４において、ノードＳＷ１の状態が、検証性質５２０に違反している。
【００３９】
なお、モデル検査部１２０は、反例５４０をもとに、反例トレース５５０を生成し、利用者へ出力（表示）してもよい。
【００４０】
図６は、本発明の実施の形態における、反例トレース５５０の例を示す図である。
【００４１】
反例トレース５５０は、反例５４０により示されるシステム状態の遷移系列における各ノードの状態の遷移系列を、イベントと関連付けて、シーケンス図で表現したものである。図６の反例トレース５５０は、図５の反例５４０に対応する。
【００４２】
図６の例では、矩形内が各ノードの状態を示す。また、矢印がノード間のイベントを示し、矢印の元がイベントの通知元のノード、矢印の先がイベントの通知先のノードを示す。各ノードの状態は、イベントにより状態が変化したタイミングで示されている。
【００４３】
反例処理装置２００は、反例５４０をもとに、簡約化された反例トレース５６０を生成する。
【００４４】
反例処理装置２００は、反例記憶部２１０、及び、簡約部２２０を含む。
【００４５】
反例記憶部２１０は、モデル検査装置１００から出力された検査結果５３０に含まれる反例５４０を記憶する。
【００４６】
簡約部２２０は、反例５４０をもとに、簡約化された反例トレース５６０を生成する。
【００４７】
ここで、簡約部２２０は、反例５４０の中で、検証性質５２０に違反するシステム状態を特定する。簡約部２２０は、特定されたシステム状態において検証性質５２０の違反が検出されたノード、及び、当該ノードの検証性質５２０に違反した状態に影響した可能性があるノードを、解析対象のノードとして抽出する。そして、簡約部２２０は、解析対象のノードの状態の遷移系列を示す、簡約化された反例トレース５６０を生成し、利用者へ出力（表示）する。
【００４８】
なお、反例処理装置２００は、ＣＰＵ（Central Processing Unit）とプログラムを記憶した記憶媒体を含み、プログラムに基づく制御によって動作するコンピュータであってもよい。
【００４９】
図３は、本発明の実施の形態における、コンピュータにより実現された反例処理装置２００の構成を示すブロック図である。反例処理装置２００は、ＣＰＵ２０１、ハードディスクやメモリ等の記憶手段（記憶媒体）２０２、他の装置等とデータ通信を行う通信手段２０３、キーボード等の入力手段２０４、及び、ディスプレイ等の出力手段２０５を含む。
【００５０】
ＣＰＵ２０１は、簡約部２２０の機能を実現するためのコンピュータプログラムを実行する。記憶手段２０２は、反例記憶部２１０のデータ（反例５４０）を記憶する。通信手段２０３は、モデル検査装置１００から、検査結果５３０を受信する。また、入力手段２０４が、利用者から、モデル検査装置１００により出力された検査結果５３０の入力を受け付けてもよい。出力手段２０５は、簡約化された反例トレース５６０を利用者へ出力（表示）する。また、通信手段２０３が、簡約化された反例トレース５６０を、他の装置へ送信してもよい。
【００５１】
なお、本発明の実施の形態では、モデル検査装置１００と反例処理装置２００とを別の装置としたが、例えば、反例処理装置２００がモデル検査装置１００に含まれる等、モデル検査装置１００と反例処理装置２００とが、一つの装置を構成していてもよい。
【００５２】
次に、本発明の実施の形態の動作を説明する。
【００５３】
図４は、本発明の実施の形態における、反例処理装置２００の動作を示すフローチャートである。
【００５４】
ここでは、反例記憶部２１０が、対象システムの反例５４０として、モデル検査装置１００から出力された、図５のような反例５４０を記憶していると仮定する。
【００５５】
はじめに、簡約部２２０は、解析対象のノードの集合Ｎを空集合で初期化する。また、簡約部２２０は、解析対象のイベントの集合Ｅを空集合で初期化する（ステップＳ１０１）。
【００５６】
簡約部２２０は、反例５４０において、検証性質５２０に違反しているシステム状態を特定する（ステップＳ１０２）。ここで、簡約部２２０は、反例５４０の状態遷移における最後のシステム状態を、検証性質５２０に違反しているシステム状態として特定する。
【００５７】
例えば、簡約部２２０は、図５の反例５４０において、システム状態Ｓ２４を、検証性質５２０に違反しているシステム状態と特定する。
【００５８】
簡約部２２０は、ステップＳ１０２で特定されたシステム状態において検証性質５２０に違反しているノードを抽出し、ノード集合Ｎに追加する（ステップＳ１０３）。ここで、検証性質５２０に違反しているノードは、反例５４０とともに入力されてもよい。また、簡約部２２０が、利用者等から入力された検証性質５２０をもとに、検証性質５２０に違反しているノードを特定してもよい。
【００５９】
例えば、簡約部２２０は、システム状態Ｓ２４において検証性質５２０を満たしていないノードＳＷ１をノード集合Ｎに、Ｎ＝｛ＳＷ１｝のように追加する。
【００６０】
簡約部２２０は、ステップＳ１０２で特定されたシステム状態を対象状態Ｓに設定する（ステップＳ１０４）。
【００６１】
例えば、簡約部２２０は、システム状態Ｓ２４を対象状態Ｓに設定する。
【００６２】
簡約部２２０は、対象状態Ｓに先立つイベントが、ノード集合Ｎに含まれるノードの状態を変更するかどうかを判定する（ステップＳ１０５）。
【００６３】
ステップＳ１０５で変更する場合（ステップＳ１０５／Ｙ）、簡約部２２０は、イベント集合Ｅに、対象状態Ｓに先立つイベントとその通知先ノードの組を追加する（ステップＳ１０６）。そして、簡約部２２０は、ノード集合Ｎに、対象状態Ｓに先立つイベントの通知元ノードと通知先ノードとを追加する（ステップＳ１０７）。
【００６４】
例えば、システム状態Ｓ２４に先立つイベントｐ２’’は、ノード集合Ｎに含まれるノードＳＷ１の状態を変更する。したがって、簡約部２２０は、イベントｐ２’’と通知先ノードＳＷ１との組をイベント集合Ｅに、Ｅ＝｛（ｐ２’’，ＳＷ１）｝のように追加する。そして、簡約部２２０は、イベントｐ２’’の通知先ノードＳＷ１と通知元ノードＳＷ２とを、ノード集合Ｎに、Ｎ＝｛ＳＷ１、ＳＷ２｝のように追加する。
【００６５】
簡約部２２０は、対象状態Ｓが反例５４０中の最初のシステム状態かどうかを判定する（ステップＳ１０８）。
【００６６】
ステップＳ１０８で、最初のシステム状態でない場合（ステップＳ１０８／Ｎ）、簡約部２２０は、対象状態Ｓに、当該対象状態Ｓの一つ前のシステム状態を設定し（ステップＳ１０９）、ステップＳ１０５からの処理を繰り返す。
【００６７】
例えば、対象状態Ｓがシステム状態Ｓ２３の場合、システム状態Ｓ２３に先立つイベントｐ２’は、ノード集合Ｎに含まれるノードＳＷ２の状態を変更する。したがって、簡約部２２０は、イベントｐ２’と通知先ノードＳＷ２との組をイベント集合Ｅに追加する。
【００６８】
同様に、簡約部２２０は、対象状態Ｓがシステム状態Ｓ１になるまで、イベントがノード集合Ｎに含まれるノードの状態を変更するかどうかの判定と、変更する場合のイベント集合Ｅ、ノード集合Ｎへのイベント、ノードの追加を繰り返す。
【００６９】
この結果、ノード集合Ｎとして、Ｎ＝｛ＳＷ１，ＳＷ２，ＣＮＴ，Ｈ１｝が得られる。また、イベント集合Ｅとして、Ｅ＝｛（ｐ１，ＳＷ１），（ｐｉ１，ＣＮＴ），（ｆｍ１，ＳＷ１），（ｐ１’，ＳＷ２），（ｐ２，ＳＷ１），（ｐ２’，ＳＷ２），（ｐ２’’，ＳＷ１）｝が得られる。
【００７０】
このようにして得られたノード集合Ｎには、解析対象のノードとして、検証性質５２０の違反が検出されたノードと、当該ノードの検証性質５２０に違反した状態に影響した可能性があるノードが設定されている。また、イベント集合Ｅには、解析対象のイベントとして、当該ノードの検証性質５２０に違反した状態に影響した可能性があるイベントが設定されている。
【００７１】
ステップＳ１０８で、対象状態Ｓが反例５４０中の最初のシステム状態であれば（ステップＳ１０８／Ｙ）、簡約部２２０は、ノード集合Ｎとイベント集合Ｅとをもとに、簡約化された反例トレース５６０を生成する（ステップＳ１１０）。ここで、簡約部２２０は、反例５４０により示されるシステム状態の遷移系列から、ノード集合Ｎに含まれるノードの状態の遷移系列を抽出し、イベント集合Ｅに含まれるイベントと関連付けることにより、簡約化された反例トレース５６０を生成する。
【００７２】
図７は、本発明の実施の形態における、簡約化された反例トレース５６０の例を示す図である。
【００７３】
例えば、簡約部２２０は、図７のように、簡約化された反例トレース５６０を生成する。
【００７４】
図７の反例トレース５６０では、図６の反例トレース５５０に比べて、解析対象のノード以外のノードＳＷ３、ＳＷ４、Ｈ２の状態の遷移系列や、解析対象のイベント以外のイベントが省略され、簡約化されている。
【００７５】
簡約部２２０は、簡約化された反例トレース５６０を出力する（ステップＳ１１１）。
【００７６】
例えば、簡約部２２０は、図７の反例トレース５６０を利用者へ出力（表示）する。
【００７７】
利用者は、解析対象のノードの状態の遷移系列と、解析対象のイベントのみに簡約化された反例トレース５６０を解析することにより、検証性質５２０の違反を引き起こす不具合の原因を、容易に推定できる。
【００７８】
以上により、本発明の実施の形態の動作が完了する。
【００７９】
次に、本発明の実施の形態の特徴的な構成を説明する。図１は、本発明の実施の形態の特徴的な構成を示すブロック図である。
【００８０】
図１を参照すると、本発明の実施の形態の反例処理装置２００（情報処理装置）は、反例記憶部２１０、及び、簡約部２２０を含む。反例記憶部２１０は、システムに係る複数の要素の状態の集合であるシステム状態の、検証性質５２０の違反が検出されるまでの遷移系列を示す反例５４０を記憶する。簡約部２２０は、反例５４０から、検証性質５２０の違反が検出された要素と、当該要素の検証性質５２０に違反した状態に影響した可能性がある要素とを、解析対象の要素として抽出し、当該抽出された解析対象の要素の状態の遷移系列を関連付けて出力する。
【００８１】
本発明の実施の形態によれば、モデル検査における反例の分析を効率化できる。その理由は、簡約部２２０が、反例５４０から、検証性質５２０の違反が検出された要素と、当該要素の検証性質５２０に違反した状態に影響した可能性がある要素とを、解析対象の要素として抽出し、簡約化された反例トレース５６０として出力するためである。これにより、モデル検査における、不具合の特定を効率化できる。
【００８２】
以上、実施形態を参照して本願発明を説明したが、本願発明は上記実施形態に限定されるものではない。本願発明の構成や詳細には、本願発明のスコープ内で当業者が理解し得る様々な変更をすることができる。
【産業上の利用可能性】
【００８３】
本発明は、モデル検査において反例の解析により不具合の特定を支援するツールに適用できる。また、本発明は、モデル検査以外に、実行トレースを表示するツールにも適用できる。
【符号の説明】
【００８４】
１００    モデル検査装置
１１０    モデル生成部
１２０    モデル検査部
２００    反例処理装置
２０１    ＣＰＵ
２０２    記憶手段
２０３    通信手段
２０４    入力手段
２０５    出力手段
２１０    反例記憶部
２２０    簡約部
５１０    モデル記述
５２０    検証性質
５３０    検査結果
５４０    反例
５５０    反例トレース
５６０    反例トレース
【図１】
2016014959.tif 000003
【図２】
2016014959.tif 000004
【図３】
2016014959.tif 000005
【図４】
2016014959.tif 000006
【図５】
2016014959.tif 000007
【図６】
2016014959.tif 000008
【図７】
2016014959.tif 000009