(57)【要約】【課題】モデル検査を用いたシステムの検証において、ひとつの反例から不具合の原因を特定するのが困難である。【解決手段】生成される複数の反例を集積し、集積された複数の反例を解析して、最も多くの反例に現れるプロセスと最も多くの反例に現れる処理を出力する。(これらの最も多くの反例に現れるプロセス・処理は不具合の原因である可能性が高い。)【選択図】図１
2010205066.tif 000002
【特許請求の範囲】
【請求項１】
入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルと、モデルが満たすべき性質を示す検証項目と、を参照して、前記モデルが前記検証項目を満たすか否かを検査して、前記モデルが前記検証項目を満たしていないと１つ以上の反例を生成するモデル検査手段と、
一つのモデルと一つの検証項目に対して前記モデル検査手段が生成した複数の反例を集積し、保存する反例集積手段と、
集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析手段と、
前記反例解析手段で求められた処理を特定する情報を出力する出力手段と、を備えることを特徴とする反例解析支援装置。
【請求項２】
前記システムは、複数の並行に動作するプロセスから構成され、
前記プロセスは複数の処理を実行する並行システムである時に、前記反例解析手段が、さらに最も多くの反例に現れるプロセスを求め、
前記出力手段は、プロセスを特定する情報を出力することを特徴とする請求項１記載の反例解析支援装置。
【請求項３】
前記反例解析手段は、さらに各プロセスが出現する反例の数と各処理が出現する反例の数を求め、
前記出力手段は、前記反例解析手段により求められた数を出力することを特徴とする請求項１又は２記載の反例解析支援装置。
【請求項４】
前記反例集積手段に保存された反例から、入力された条件に合致する反例を検索する反例検索手段を備え、
前記出力手段は、前記反例検索手段にて検索された情報を出力することを特徴とする請求項１から３のいずれか１項に記載の反例解析支援装置。
【請求項５】
入力された複数のモデルを格納するモデル群格納手段を備え、
前記モデル検査手段は、前記複数のモデルを一つずつ順に同じ検証項目を満たすか否かを検査することを特徴とする請求項１から４のいずれか１項に記載の反例解析支援装置。
【請求項６】
前記反例集積手段に保存された反例から、入力された条件に合致する反例を検索する反例検索手段と、
前記反例検索手段にて検索された反例に対応するモデルを前記モデル群格納手段より検索するモデル検索手段、を備え、
前記出力手段は、前記反例検索手段と前記モデル検索手段により、検索された反例とモデルを特定する情報を出力することを特徴とする請求項５記載の反例解析支援装置。
【請求項７】
入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルが、満たすべき性質を示す検証項目を満たしているか否かを検査して、反例を生成するモデル検査装置と、前記反例を解析して出力する反例解析支援装置と、を備える反例解析支援システムであって、
前記モデル検査装置は、
前記モデルと、前記検証項目と、を参照して、前記モデルが前記検証項目を満たすか否かを検査して、前記モデルが前記検証項目を満たしていないと１つ以上の反例を生成するモデル検査手段を有し、
前記反例解析支援装置は、
一つのモデルと一つの検証項目に対して前記モデル検査手段にて生成された複数の反例を集積し、保存する反例集積手段と、
集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析手段と、
前記反例解析手段で求められた処理を特定する情報を出力する出力手段と、を備えることを特徴とする反例解析支援システム。
【請求項８】
前記システムは、複数の並行に動作するプロセスから構成され、
前記プロセスは複数の処理を実行する並行システムである時に、前記反例解析手段が、さらに最も多くの反例に現れるプロセスを求め、
前記出力手段は、プロセスを特定する情報を出力することを特徴とする請求項７記載の反例解析支援システム。
【請求項９】
前記反例解析手段は、さらに各プロセスが出現する反例の数と各処理が出現する反例の数を求め、
前記出力手段は、前記反例解析手段により求められた数を出力することを特徴とする請求項７又は８記載の反例解析支援システム。
【請求項１０】
前記反例集積手段に保存された反例から、入力された条件に合致する反例を検索する反例検索手段をさらに備え、
前記出力手段は、前記反例検索手段にて検索された情報を出力することを特徴とする請求項７から９のいずれか１項に記載の反例解析支援システム。
【請求項１１】
入力された複数のモデルを格納するモデル群格納手段を備え、
前記モデル検査手段は、前記複数のモデルを一つずつ順に同じ検証項目を満たすか否かを検査することを特徴とする請求項７から１０のいずれか１項に記載の反例解析支援システム。
【請求項１２】
前記反例集積手段に保存された反例から、入力された条件に合致する反例を検索する反例検索手段と、
前記反例検索手段にて検索された反例に対応するモデルを前記モデル群格納手段より検索するモデル検索手段、を備え、
前記出力手段は、前記反例検索手段と前記モデル検索手段により、検索された反例とモデルを特定する情報を出力することを特徴とする請求項１１記載の反例解析支援システム。
【請求項１３】
入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルと、モデルが満たすべき性質を示す検証項目と、を参照して、前記モデルが前記検証項目を満たすか否かを検査して、前記モデルが前記検証項目を満たしていないと１つ以上の反例を生成するモデル検査ステップと、
一つのモデルと一つの検証項目に対して前記モデル検査ステップにて生成した複数の反例を集積し、保存する反例集積ステップと、
集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析ステップと、
前記反例解析ステップで求められた処理を特定する情報を出力する出力ステップと、を備えることを特徴とする反例解析支援装置の反例解析支援方法。
【請求項１４】
前記システムは、複数の並行に動作するプロセスから構成され、
前記プロセスは複数の処理を実行する並行システムである時に、前記反例解析ステップにて、さらに最も多くの反例に現れるプロセスを求め、
前記出力ステップは、プロセスを特定する情報を出力することを特徴とする請求項１３記載の反例解析支援装置の反例解析支援方法。
【請求項１５】
前記反例解析ステップは、さらに各プロセスが出現する反例の数と各処理が出現する反例の数を求め、
前記出力ステップは、前記反例解析ステップにより求められた数を出力することを特徴とする請求項１３又は１４記載の反例解析支援装置の反例解析支援方法。
【請求項１６】
前記反例集積ステップに保存された反例から、入力された条件に合致する反例を検索する反例検索ステップを備え、
前記出力ステップは、前記反例検索ステップにて検索された情報を出力することを特徴とする請求項１３から１５のいずれか１項に記載の反例解析支援装置の反例解析支援方法。
【請求項１７】
入力された複数のモデルを格納するモデル群格納ステップを備え、
前記モデル検査ステップは、前記複数のモデルを一つずつ順に同じ検証項目を満たすか否かを検査することを特徴とする請求項１３から１６のいずれか１項に記載の反例解析支援装置の反例解析支援方法。
【請求項１８】
前記反例集積ステップに保存された反例から、入力された条件に合致する反例を検索する反例検索ステップと、
前記反例検索ステップにて検索された反例に対応するモデルを格納した複数のモデルより検索するモデル検索ステップ、を備え、
前記出力ステップは、前記反例検索ステップと前記モデル検索ステップにより、検索された反例とモデルを特定する情報を出力することを特徴とする請求項１７記載の反例解析支援装置の反例解析支援方法。
【請求項１９】
モデル検査装置による、入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルと、モデルの満たすべき性質を示す検証項目と、を参照して、前記モデルが前記検証項目を満たすか否かを検査して、前記モデルが前記検証項目を満たしていないと１つ以上の反例を生成するモデル検査ステップと、
反例解析支援装置による、一つのモデルと一つの検証項目に対して前記モデル検査ステップにて生成された複数の反例を集積し、保存する反例集積ステップと、
集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析ステップと、
前記反例解析ステップで求められた処理を特定する情報を出力する出力ステップと、を備えることを特徴とする反例解析支援システムの反例解析支援方法。
【請求項２０】
入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルと、モデルが満たすべき性質を示す検証項目と、を参照して、前記モデルが前記検証項目を満たすか否かを検査して、前記モデルが前記検証項目を満たしていないと１つ以上の反例を生成するモデル検査処理と、
一つのモデルと一つの検証項目に対して前記モデル検査処理にて生成した複数の反例を集積し、保存する反例集積処理と、
集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析処理と、
前記反例解析処理で求められた処理を特定する情報を出力する出力処理と、をコンピュータに実行させるプログラム。
【請求項２１】
モデル検査装置による、入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルと、モデルの満たすべき性質を示す検証項目と、を参照して、前記モデルが前記検証項目を満たすか否かを検査して、前記モデルが前記検証項目を満たしていないと１つ以上の反例を生成するモデル検査処理と、
反例解析支援装置による、一つのモデルと一つの検証項目に対して前記モデル検査処理にて生成された複数の反例を集積し、保存する反例集積処理と、
集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析処理と、
前記反例解析処理で求められた処理を特定する情報を出力する出力処理と、をコンピュータに実行させるプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検査技術を用いた並行システムまたは並行システムのソフトウェアの検証における反例解析支援装置、反例解析支援システム、それらの反例解析支援方法及びプログラムに関し、特に複数の反例を集積し、集積した複数の反例におけるプロセスや処理の出現頻度を解析することにより、不具合原因の候補群を提示できる反例解析支援装置、反例解析支援システム、それらの反例解析支援方法及びプログラムに関する。
【背景技術】
【０００２】
システムやソフトウェアの動作仕様を検証する方法として、モデル検査法が知られている。モデル検査法とは、検証対象のシステムやソフトウェアの動作仕様を示す状態遷移系のモデルと、動作仕様が満たすべき性質（検証性質）を示す検証項目を入力し、モデルが検証項目に違反しないか否かにより、検証対象の動作仕様を検証する方法である。
【０００３】
従って、モデル検査を行うエンジンであるモデル検査器への入力は、モデルと検証項目となるが、このモデルが検証対象システム・ソフトウェアの動作仕様に加えて、検証対象システム・ソフトウェアが動作する外界の環境の振舞いを含む場合もある。
【０００４】
モデル検査法を用いて、複数のプロセスが並行して同時に実行される並行システム(やそのソフトウェア)の検証をすることができる。並行システムのモデル検査を行うことができるツール(モデル検査器)として、ＳＰＩＮ等が知られている。
【０００５】
モデル検査法では、モデルが検証項目に違反する（検証性質を満たしていない）場合、性質を満たさなくなっている場合の実行例（実行ログ）である反例を出力する。一般には性質を満たさなくなるような実行例は複数あり、その複数の中のひとつの例についてひとつの反例が対応する。ひとつの反例が膨大な量となることもある。特に、並行システムをモデル検査で検証した場合の反例には、複数のプロセスにおける処理が含まれ得る。
【０００６】
反例は、検証性質を満たさないようなひとつの実行例を示すものであり、検証性質が満たされない原因、つまり不具合の原因を示すものではない。したがって、モデル検査法により動作仕様を検査する場合、反例が出力されると、システム(ソフトウェア)開発者がその反例を解析し、システム(ソフトウェア)の不具合を発見しなければならない。
【０００７】
そのため、第１の問題点として、システムのモデル検査を用いた検証において、反例から不具合の原因を突き止めるのが難しいという問題がある。その理由は、反例はその量が膨大であることがあり、人間が人手だけで解析するのは困難だからである。
【０００８】
また、第２の問題点は、並行システムの検証において反例から不具合の原因を突き止めるのが難しいということである。その理由は、第1の問題点の理由に加えて、並行システムの検証の場合には反例には複数のプロセスにおける処理が含まれ得るので、そのうちのどのプロセス・どの処理が不具合に関連にしているのか、反例だけではわからないからである。
【０００９】
そこで、第１の問題点に対して、この反例解析を典型的な不具合を抽出してパターン化したものを利用して支援する方法が、非特許文献１に記載されている。
【先行技術文献】
【非特許文献】
【００１０】
【非特許文献１】高田沙都子、外３名、「産業用コントローラに対するモデル検査適用事例」、ソフトウェア品質シンポジウム２００８
【発明の概要】
【発明が解決しようとする課題】
【００１１】
しかしながら、非特許文献１における問題点は、反例から不具合の原因を突き止めるための典型的な不具合のパターンの入手は一般には困難であるということである。その理由は、検証対象となるシステムについて類似システムがない、あるいは少ない場合には、起こりうる不具合についてパターンとして抽出するに足る十分な情報を持ち得ないからである。
【００１２】
そこで本発明は、上記問題点に鑑みてなされたもので、システムの不具合の原因の特定を支援できる反例解析支援装置を提供することを目的とする。
【課題を解決するための手段】
【００１３】
上記課題を解決するため、本発明における反例解析支援装置は、入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルと、モデルが満たすべき性質を示す検証項目と、を参照して、モデルが前記検証項目を満たすか否かを検査して、モデルが前記検証項目を満たしていないと１つ以上の反例を生成するモデル検査手段と、一つのモデルと一つの検証項目に対してモデル検査手段が生成した複数の反例を集積し、保存する反例集積手段と、集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析手段と、反例解析手段で求められた処理を特定する情報を出力する出力手段と、を備えることを特徴とする。
【００１４】
また、本発明における反例解析支援システムは、入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルが、満たすべき性質を示す検証項目を満たしているか否かを検査して、反例を生成するモデル検査装置と、反例を解析して出力する反例解析支援装置と、を備える反例解析支援システムであって、モデル検査装置は、モデルと、検証項目と、を参照して、モデルが検証項目を満たすか否かを検査して、モデルが検証項目を満たしていないと１つ以上の反例を生成するモデル検査手段を有し、反例解析支援装置は、一つのモデルと一つの検証項目に対してモデル検査手段にて生成された複数の反例を集積し、保存する反例集積手段と、集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析手段と、反例解析手段で求められた処理を特定する情報を出力する出力手段と、を備えることを特徴とする。
【００１５】
また、本発明における反例解析支援装置の反例解析支援方法は、入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルと、モデルが満たすべき性質を示す検証項目と、を参照して、モデルが検証項目を満たすか否かを検査して、モデルが検証項目を満たしていないと１つ以上の反例を生成するモデル検査ステップと、一つのモデルと一つの検証項目に対してモデル検査ステップにて生成した複数の反例を集積し、保存する反例集積ステップと、集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析ステップと、反例解析ステップで求められた処理を特定する情報を出力する出力ステップと、を備えることを特徴とする。
【００１６】
また、本発明における反例解析支援システムの反例解析支援方法は、モデル検査装置による、入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルと、モデルの満たすべき性質を示す検証項目と、を参照して、モデルが検証項目を満たすか否かを検査して、モデルが検証項目を満たしていないと１つ以上の反例を生成するモデル検査ステップと、反例解析支援装置による、一つのモデルと一つの検証項目に対してモデル検査ステップにて生成された複数の反例を集積し、保存する反例集積ステップと、集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析ステップと、反例解析ステップで求められた処理を特定する情報を出力する出力ステップと、を備えることを特徴とする。
【００１７】
また、本発明におけるプログラムは、入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルと、モデルが満たすべき性質を示す検証項目と、を参照して、モデルが検証項目を満たすか否かを検査して、モデルが検証項目を満たしていないと１つ以上の反例を生成するモデル検査処理と、一つのモデルと一つの検証項目に対してモデル検査処理にて生成した複数の反例を集積し、保存する反例集積処理と、集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析処理と、反例解析処理で求められた処理を特定する情報を出力する出力処理と、をコンピュータに実行させることを特徴とする。
【００１８】
また、本発明におけるプログラムは、モデル検査装置による、入力された複数の処理を有するシステムの動作仕様もしくはシステムの動作仕様と外部環境を示すモデルと、モデルの満たすべき性質を示す検証項目と、を参照して、モデルが検証項目を満たすか否かを検査して、モデルが検証項目を満たしていないと１つ以上の反例を生成するモデル検査処理と、反例解析支援装置による、一つのモデルと一つの検証項目に対してモデル検査処理にて生成された複数の反例を集積し、保存する反例集積処理と、集積された複数の反例を解析し、最も多くの反例に現れる処理を求める反例解析処理と、反例解析処理で求められた処理を特定する情報を出力する出力処理と、をコンピュータに実行させることを特徴とする。
【発明の効果】
【００１９】
本発明により、複数の反例を解析して反例の多数に現れるプロセスや処理を求めることによって、不具合の原因になっている可能性が高いプロセスや処理を出力するため、システムの検証において開発者が反例から不具合の原因を突き止めることを効果的に支援できる。
【図面の簡単な説明】
【００２０】
【図１】本発明の第１及び第２の実施形態に係る本発明の反例解析支援装置の構成を示すブロック図である。
【図２】本発明の第３の実施形態に係る本発明の反例解析支援装置の構成を示すブロック図である。
【図３】本発明の第４の実施形態に係る本発明の反例解析支援装置の構成を示すブロック図である。
【図４】本発明の第５の実施形態に係る本発明の反例解析支援装置の構成を示すブロック図である。
【図５】本発明の実施形態に係る本発明の反例解析支援システムの構成図である。
【図６】反例の一例を示す図である。
【図７】統計情報の一例を示す図である。
【図８】最多出現情報の一例を示す図である。
【発明を実施するための形態】
【００２１】
次に、発明を実施するための最良の形態について図面を参照して詳細に説明する。
【００２２】
（第１の実施形態）
図１は、本発明の第１の実施の形態における反例解析支援装置の構成図である。本反例解析支援装置は、入力手段１と、モデル検査手段２と、反例集積手段３と、反例解析手段４と、出力手段５と、を有して構成される。これらの手段はそれぞれ概略つぎのように動作する。
【００２３】
入力手段１は、モデル検査手段への入力であり、モデルと検証項目を入力するためのものである。モデルは、検証対象のシステムやソフトウェアの動作仕様を示すものであり、さらに検証対象システム・ソフトウェアが動作する外界の環境の振舞いを含んでも良い。検証項目は、検証すべき性質を表すものである。
【００２４】
モデル検査手段２は、モデル検査を行うエンジンであり、具体例としてはＳＰＩＮ等のモデル検査器などと同様の機能を有する機能部である。
【００２５】
反例集積手段３は、モデル検査手段２が生成する複数の反例を集積する。
【００２６】
反例解析手段４は、反例集積手段３により集積された複数の反例を解析し、複数の反例中の処理の出現回数の統計情報を生成する。また、最も出現回数の多い処理を示す最多出現情報を生成する。
【００２７】
出力手段５は、反例解析手段４が生成した統計情報や、最多出現情報を出力するためのものである。
【００２８】
次に、図１を参照して本実施の形態の全体の動作について詳細に説明する。
【００２９】
入力手段１により、モデル検査手段２への入力を行う。モデル検査手段２が、例えばＳＰＩＮであった場合、Ｐｒｏｍｅｌａで記述したモデルと、線形時相論理式(ＬＴＬ)で記述した検証項目を入力する。
【００３０】
モデル検査手段２は、入力手段１より入力されたモデルが検証項目を満たすかどうかを検査し、その結果を出力する。検証項目を満たしていれば反例は出力されず、その解析を行う必要はないので、ここで動作は終了する。
【００３１】
検証項目を満たしていない場合、モデル検査手段は反例を複数生成することができる。ここでモデル検査手段は、すべての反例を生成し、保存するように起動される。例えば、モデル検査手段がＳＰＩＮであった場合、モデル検査手段に与えるオプションによってすべての反例を識別可能なように連続する番号をつけて保存するか、反例がひとつしか保存されないように動作を抑制するかを切り替えることができるが、全てを保存するオプションを与えて起動される。
【００３２】
反例集積手段３は、モデル検査手段２の出力を受け取り、モデル検査手段２が生成した複数の反例を集積し、保存する。
【００３３】
反例解析手段４は、反例集積手段３が集積した複数の反例について、反例に含まれる処理に関する統計情報を生成する。反例には、どの処理が実行されたかが順に記載されている。反例解析手段４は、処理が何個の反例に出現しているか出現回数を数え、処理の出現回数の統計情報を生成する。このような統計情報は、本装置のユーザが不具合の解析を行う際に補助的な情報として利用することができる。
【００３４】
さらに、反例解析手段４は、この統計情報から、最も出現回数の多い処理を求め、最多出現情報を生成する。この最多出現処理は、不具合の原因であることが多い。
【００３５】
出力手段５は、反例解析手段４から、統計情報と最多出現情報を受け取り、出力する。
【００３６】
本実施の形態では、反例集積手段３が複数の反例を集積し、反例解析手段４が複数の反例を解析することにより多くの反例に現れる処理を求め、出力手段５に出力するというように構成されているため、ひとつの反例を人手で解析することなく、不具合の原因になっている可能性が高い処理を特定することが可能である。
【００３７】
（第２の実施形態）
本発明の第２の実施の形態における反例解析支援装置は、第1の実施の形態と同様の形態を取り、図１に示すように、入力手段１と、モデル検査手段２と、反例集積手段３と、反例解析手段４と、出力手段５と、を有して構成される。本実施形態では、検証対象システムが並行システム、すなわち複数のプロセスが並行に動くシステムである場合を対象とする。
【００３８】
入力手段１、モデル検査手段２、反例集積手段３は、第1の発明と同様に動作する。
【００３９】
反例解析手段４は、反例集積手段３が集積した複数の反例について、反例に含まれる処理に関する統計情報を生成する。反例には、どのプロセスがどういう処理をしたかが順に記載されている。反例解析手段４は、各プロセスが何個の反例に出現しているか出現回数を数える。また、反例解析手段４は、各プロセスが行った処理が何個の反例に出現しているか出現回数を数える。このような解析を行い、複数の反例中のプロセスの出現回数、処理の出現回数の統計情報を生成する。
【００４０】
このような統計情報は、本装置のユーザが不具合の解析を行う際に補助的な情報として利用することができる。さらに、反例解析手段４は、この統計情報から、最も出現回数の多いプロセス、最も出現回数の多い処理を求め、最多出現情報を生成する。この最多出現プロセス、最多出現処理は、不具合の原因であることが多い。
【００４１】
出力手段５は、反例解析手段４から、統計情報と最多出現情報を受け取り、出力する。
【００４２】
本実施の形態では、反例集積手段３が複数の反例を集積し、反例解析手段４が複数の反例を解析することにより反例に多く現れるプロセスや処理を求め、出力手段５に出力するというように構成されているため、ひとつの反例を人手で解析することなく、並行システムの不具合の原因になっている可能性が高いプロセスや処理を特定することができる。
【００４３】
（第３の実施形態）
図２は、本発明の第３の実施の形態における反例解析支援装置の構成図である。本反例解析支援装置は、入力手段１と、モデル検査手段２と、反例集積手段３と、反例解析手段４と、出力手段５と、反例検索手段６と、を有して構成される。
【００４４】
入力手段１は、まず、第１及び第２の実施形態と同様にモデル検査手段２への入力を行い、モデル検査手段２と、反例集積手段３は、第１及び第２の実施形態と同様に動作する。
【００４５】
反例解析手段４は、第１又は第２の実施形態と同様の動作に加えて、（検証対象システムが並行システムであれば）各反例毎の出現プロセスの一覧と、各反例毎の出現処理の一覧を生成する。
【００４６】
反例検索手段６は、反例集積手段３に集積された反例からユーザが指定した検索条件に合致する反例を検索する。
【００４７】
ユーザは、(反例集積手段３に集積されている)複数の反例から特定の反例のみを見るために、反例の検索条件を入力手段１を使って入力する。検索条件とは、（検証対象システムが並行システムであれば）出現するプロセス（「プロセスＡが出現しているか」）、出現する処理（「処理aが出現しているか」）、反例の長さなどであり、さらにそれらの和や積や否定でも良い。
【００４８】
出力手段５は、反例解析手段４から受け取った統計情報と最多出現情報及び／又は反例検索手段６が検索した反例を出力する。
【００４９】
本実施の形態では、第１及び第２の発明の構成に加えて、反例検索手段を持つように構成されているため、ユーザが不具合を特定する際に参考になると考えられる反例（最多出現プロセスと最多出現処理が現れていてかつ一番短い等）を検索して出力することができ、ユーザによる不具合の特定をより正確にすることを支援する。
【００５０】
（第４の実施形態）
図３は、本発明の第４の実施の形態における反例解析支援装置の構成図である。本反例解析支援装置は、入力手段１と、モデル群格納手段１１と、全体制御手段２１と、モデル検査手段２と、反例集積手段３と、反例解析手段４と、反例検索手段６と、出力手段５と、を有して構成される。
【００５１】
入力手段１は、モデルと検証項目を入力するために使用される。モデルは、複数のモデルであっても良い。典型的には、検証対象システムを示す部分は全く同じであるが、環境を示す部分がそれぞれ異なる複数のモデルである。検証項目は、これら複数のモデルに共通して検証されるひとつの検証項目である。
【００５２】
入力手段１により入力された複数のモデルは、モデル群格納手段１１に格納される。
【００５３】
全体制御手段２１は、モデル群格納手段１１に格納されたモデルがひとつずつ順に検証され、ひとつのモデルに対する検証が終了する毎に反例が反例集積手段３に集積され、全てのモデルが検証され反例が集積された後に反例解析手段４による解析が行われるように全体を制御する。
【００５４】
全体制御手段２１は、モデル格納手段１１からモデルを順にひとつ取り出し、モデル検査手段２に入力する。また、入力手段１により入力された検証項目は、モデル検査手段２に入力される。
【００５５】
モデル検査手段２は、与えられたモデルと検証項目に対して検証を行い、（モデルが検証項目を満たしていない場合）複数の反例を生成する。
【００５６】
反例集積手段３は、モデル検査手段２の出力を受け取り、モデル検査手段２が生成した複数の反例を集積し保存する。モデル検査手段２による検証は、全体制御手段２１によりモデルの数だけ複数回行われるので、各検証毎にモデル検査手段２の出力を受け取り、反例を集積する。
【００５７】
全体制御手段２１は、全てのモデルの検証が終了すると、反例解析手段４を起動させる。反例解析手段４は、第１及び第２の実施形態と同様に動作し、統計情報と最多出現情報を生成する。
【００５８】
出力手段５は、第１及び第２の実施形態と同様に動作し、反例解析手段４から、統計情報と最多出現情報を受け取り、出力する。
【００５９】
本実施の形態では、第１及び第２の発明の構成に加えて、全体制御手段とモデル群格納手段を持つように構成されているため、検証対象システムが同一であって環境だけが異なる複数のモデルの検証を行った際の複数の反例全体を解析して、検証対象システムの不具合の原因になっている可能性が高いプロセスや処理を特定することができる。
【００６０】
（第５の実施形態）
図４は、本発明の第５の実施の形態における反例解析支援装置の構成図である。本反例解析支援装置は、入力手段１と、モデル群格納手段１１と、全体制御手段２１と、モデル検査手段２と、反例集積手段３と、反例解析手段４と、反例検索手段６と、モデル検索手段７と、出力手段５と、を有して構成される。
【００６１】
入力手段１は、まず第４の実施形態と同様に、モデルと検証項目を入力するために使用される。
【００６２】
全体制御手段２１、モデル検査手段２は、第４の実施形態と同様に動作する。
【００６３】
反例集積手段３は、第４の実施形態と同様の動作に加え、モデルと反例の対応（反例がどのモデルに対して生成された反例であるか）を記録する。
【００６４】
反例解析手段４は、第３の実施形態と同様に動作し、統計情報、最多出現情報、各反例毎の出現プロセスの一覧、各反例毎の出現処理の一覧を生成する。
【００６５】
出力手段５は、反例解析手段４から、統計情報と最多出現情報を受け取り、出力する。
【００６６】
ユーザは、(反例集積手段３に集積されている)複数の反例から特定の反例のみを見るために、反例の検索条件を入力手段1を使って入力する。検索条件とは、（検証対象システムが並行システムであれば）出現するプロセス（「プロセスＡが出現しているか」）、出現する処理（「処理aが出現しているか」）、反例の長さであり、さらにそれらの和や積や否定でも良い。
【００６７】
反例検索手段６は、反例集積手段３に集積された反例からユーザが指定した検索条件に合致する反例を検索する。
【００６８】
モデル検索手段７は、反例検索手段６が検索した反例を受け取り、反例集積手段３に記録されたモデルと反例の対応を参照し、モデル群格納手段１１から反例に対応するモデルを検索する。
【００６９】
出力手段５は、反例検索手段６が検索した反例と、モデル検索手段７が検索したモデルを出力する。
【００７０】
本実施の形態では、第４の実施形態の構成に加えて、反例検索手段、モデル検索手段を持つように構成されているため、ユーザが不具合を特定する際に参考になると考えられる反例（最多出現プロセスと最多出現処理が現れていてかつ一番短い等）とその反例に対応するモデルを検索して出力することができ、ユーザによる不具合の特定をより正確にすることを支援する。
【００７１】
（第６の実施形態）
図５は、本発明の実施形態における反例解析支援システム１００の構成図である。本反例解析支援システムは、反例解析支援装置１１０と、モデル検査装置１２０と、を有して構成される。
【００７２】
モデル検査装置１２０は、上記の各実施形態におけるモデル検査手段２と同様の機能を有し、例えば、具体例としてはＳＰＩＮ等のモデル検査器である。
【００７３】
反例解析支援装置１１０は、各実施形態におけるモデル検査手段以外の機能を有して各実施形態において説明した反例解析支援装置と同様の処理を行う。
【実施例】
【００７４】
次に、具体的な実施例を用いて本発明を実施するための最良の形態の動作を説明する。
【００７５】
入力手段１により動作仕様と検査項目を入力し、モデル検査手段２が検証を行い、反例を生成する。生成された反例が例えば図６に示す３個であったとする。
【００７６】
ここで反例の各行は、プロセス名.処理名のように記述されているとする。この３個の反例が、反例集積手段３に保存される。反例解析手段４は、保存された３個の反例について、プロセスの出現回数と処理の出現回数を解析する。
【００７７】
ここでは、プロセスprocAの出現回数は３、プロセスprocBの出現回数は２、プロセスprocCの出現回数は１、プロセスprocDの出現回数は１である。同様に、処理の出現回数も求められる。このようにして、反例解析手段４は、プロセスの出現回数と処理の出現回数を含む統計情報を生成する。この場合の統計情報を図７に示す。さらに、反例解析手段４は、この統計情報から最も出現回数の多いプロセス、最も出現回数の多い処理を示す最多出現情報を生成する。この場合の最多出現情報を図８に示す。
【００７８】
本発明の実施形態における反例解析支援装置の各構成要素は、任意のコンピュータのＣＰＵ、メモリ、メモリにロードされた構成要素を実現するプログラム、そのプログラムを格納するハードディスクなどの記憶ユニット、ネットワーク接続用インタフェースを中心にハードウエアとソフトウエアの任意の組合せによって実現される。そして、その実現方法、装置にはいろいろな変形例があることは、当業者には理解されるところである。
【００７９】
本発明の実施形態における反例解析支援装置は、反例集積手段(図1の３)と、反例解析手段(図1の４)とを備え、検証対象システム（及びその環境）を示すひとつのモデルと、ひとつの検証項目に対し、モデル検査器が生成する反例を全て集積し、集積された反例の多数に現れるプロセスや検証対象システムが行う処理が何かを調べてその結果を出力するように動作する。反例の多数に現れるプロセスや処理は不具合の原因であることが多いので、反例集積手段と反例解析手段を備える構成を採用して反例の多数に現れる処理の情報を出力することにより、本発明の目的を達成することができる。
【００８０】
本実施形態における第１の効果は、システムの検証において開発者が反例から不具合の原因を突き止めることを本装置が効果的に支援できることにある。その理由は、複数の反例を解析して反例の多数に現れるプロセスや処理を求めることによって、不具合の原因になっている可能性が高いプロセスや処理を出力するためである。
【００８１】
第２の効果は、開発者が不具合の典型的なパターンに関する情報が入手できない場合にも、それに代わって反例解析に有効であると考えられる情報を本システムが提供できることにある。その理由は、不具合の典型的なパターンの情報を用いることなく、モデル検査器が生成する複数の反例を解析し、反例の多数に現れるプロセスや処理を求めることによって、不具合の原因になっている可能性が高いプロセスや処理を出力するためである。
【００８２】
以上、実施の形態を説明したが、特許請求の範囲に定義された本発明の広範囲な趣旨および範囲から逸脱することなく、これら実施の形態や具体例に様々な修正および変更が可能である。
【産業上の利用可能性】
【００８３】
本発明によれば、ソフトウェア開発における設計の妥当性を検証するツールにおける不具合の解析支援ツールといった用途に適用できる。また、ハードウエア開発における設計の妥当性を検証するツールにおける不具合の解析支援ツールといった用途に適用できる。
【符号の説明】
【００８４】
１    入力手段
２    モデル検査手段
３    反例集積手段
４    反例解析手段
５    出力手段
６    反例検索手段
７    モデル検索手段
１１    モデル群格納手段
２１    全体制御手段
【図１】
2010205066.tif 000003
【図２】
2010205066.tif 000004
【図３】
2010205066.tif 000005
【図４】
2010205066.tif 000006
【図５】
2010205066.tif 000007
【図６】
2010205066.tif 000008
【図７】
2010205066.tif 000009
【図８】
2010205066.tif 000010