状態探索装置、及び状態カバー率推定方法
【課題】有限状態の状態遷移グラフにおける探索すべき状態空間のうち、探索し得た空間のカバー率を推定すること。
【解決手段】既訪状態を管理するブルームフィルタ１１２と、サイズの異なるブルームフィルタ１１２を利用して複数回のモデル検査を実施するモデル検査部１１０と、複数回のモデル検査におけるブルームフィルタ１１２のサイズと到達状態数との関係を近似する成長曲線を推定することにより状態カバー率を推定する状態カバー率推定部１２０とを備える。
【解決手段】既訪状態を管理するブルームフィルタ１１２と、サイズの異なるブルームフィルタ１１２を利用して複数回のモデル検査を実施するモデル検査部１１０と、複数回のモデル検査におけるブルームフィルタ１１２のサイズと到達状態数との関係を近似する成長曲線を推定することにより状態カバー率を推定する状態カバー率推定部１２０とを備える。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、状態探索装置、及び状態カバー率推定方法に関する。特に本発明は、ブルームフィルタを用いて取り得る各状態を訪問して処理を行う状態探索装置、並びに有限状態の状態遷移グラフにおける探索すべき状態空間のうち、探索し得た空間のカバー率を推定する状態カバー率推定方法に関する。
【背景技術】
【０００２】
モデル検査とは、システムの設計書や仕様書からモデルを作成し、モデルが検査項目を満たすかどうかを全数探索することによって不具合を発見する技術である。具体的には、モデル検査では、システムを有限状態の状態遷移グラフとしてモデルを記述する。そして、モデル検査では、その状態遷移グラフにおいて、不変条件や時相論理式によって記述された形式仕様が満たされるかどうかを検査する。
【０００３】
しかしながら、モデル検査には、状態爆発問題と呼ばれる課題もある。具体的には、モデル検査において探索すべき状態数は、検査するシステムが複雑になると指数的に増加する。モデル検査では、状態数の増加に伴い、検査に必要なメモリ量も増加する。そのため、モデル検査では、検査するシステムの規模が大きくなると、検査の途中でメモリ不足となり探索が打ち切られてしまい、ごく一部の探索空間しかカバーできなくなってしまうことがある。
【０００４】
このような問題への対処方法としては、様々な手法が採られている。例えば、ＳＰＩＮ（Ｓｉｍｐｌｅ Ｐｒｏｍｅｌａ Ｉｎｔｅｒｐｒｅｔｅｒ）と呼ばれるモデル検査器では、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇと呼ばれる手法によって、メモリ量が十分に確保できない状態での状態空間のカバー率向上を実現している。
【０００５】
また、モデル検査では、状態空間の網羅的探索を行う場合、遷移先の状態に既に訪問したかどうかを確認するために、既訪状態を保存する必要がある。データ操作の効率を考えると状態を保存するためにはハッシュテーブルを用いるのが一般的であるが、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇではブルームフィルタを用いて既訪状態を管理する。ブルームフィルタは、ある要素が集合のメンバーであるかを判定するために用いることができるデータ構造である。ただし、ブルームフィルタは確率的データ構造であり、擬陽性の可能性がある。つまり、既訪状態であることを判定するためにブルームフィルタを利用する場合、未だ訪問していないにも関わらず、既訪と判断される可能性がある。しかしながら、１状態を保持するために必要なデータ量はハッシュテーブルを用いる場合に比べ少なくてすむため、結果としてメモリが十分確保できない場合では状態空間のカバー率が向上する。
【０００６】
Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇは、メモリが少ない計算機環境においても効率的な検査を可能にする。しかしながら、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇは近似的手法であり、検査により必ずしも全ての状態の探索を行えるわけではない。したがって、検査の精度という観点から考えれば、全状態に対してどれだけのカバー率が達成できたかを利用者に対して提示できることが望ましい。
【０００７】
ところで、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇを用いたモデル検査器における状態カバー率の推定方法が知られている（例えば、非特許文献１参照。）。図７は、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇを用いたモデル検査器９００の構成を示す。モデル検査器９００は、モデル検査部９１０、及び状態カバー率推定部９２０を備える。モデル検査部９１０は、初期状態と状態遷移規則から定義される有限の状態遷移グラフを、深さ優先探索などの探索アルゴリズムにより探索し、与えられた形式仕様に違反する状態又は実行系列を探索する。モデル検査部９１０は、ブルームフィルタ９１２を用いて訪問済み状態を記憶し、到達状態計数部９１１により探索により到達した状態数を計数する。到達状態計数部９１１は、ブルームフィルタ９１２に状態が追加されるときに到達状態数をインクリメントすることで到達状態数を計数する。モデル検査部９１０による探索が完了すると、状態カバー率推定部９２０は、モデル検査部９１０から到達状態数Ｎとブルームフィルタ９１２のサイズｍ（ビット）を受け取り状態カバー率の推定値を計算する。非特許文献１に記載の状態カバー率推定値の計算式は、次のとおりである。
【０００８】
【数１】
【０００９】
この計算式は、モデル検査器ＳＰＩＮでは以前用いられていたが、精度はあまり高くない。そのため、ＳＰＩＮ ｖｅｒｓｉｏｎ ５ではこの計算式による推定値の表示を行うオプションは廃止されている。
【００１０】
モデル検査器ＳＰＩＮでは、この他に、状態カバー率の指標としてｍ／Ｎで定義されるｈａｓｈ ｆａｃｔｏｒを検査終了時に提示する。ｈａｓｈ ｆａｃｔｏｒは、１状態当たりの探索に利用できたメモリ量（ビット数）を表しており、この値が大きいほどハッシュ値の衝突が少ない。そのため、良好な状態カバー率を達成できたと判断できる。しかし、この値は十分な状態カバー率が達成できているかどうかの判定には適しているが、状態カバー率を直感的に表すものではなく、利用者が得られる情報は限定的である。モデル検査を複数回又は並列に実行することで総合的な状態カバー率を向上させる手法では、１回の検査の状態カバー率によって、十分な状態カバー率を実現するのに必要な検査の回数や並列度が異なるため、ｈａｓｈ ｆａｃｔｏｒはそのような用途におけるカバー率指標としては不十分である。
【先行技術文献】
【非特許文献】
【００１１】
【非特許文献１】ジェラルド ジェイ・ホルツマン（Ｇｅｒａｒｄ Ｊ． Ｈｏｌｚｍａｎｎ）著、「ザ スピン モデル チェッカー」、（米国）、アジソン ウェスレイ プロフェッショナル（Ａｄｄｉｓｏｎ−Ｗｅｓｌｅｙ Ｐｒｏｆｅｓｓｉｏｎａｌ）、２００３年
【発明の概要】
【発明が解決しようとする課題】
【００１２】
上述のとおり、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇを用いたモデル検査は、利用者に提示する状態カバー率の推定値は信頼度の低いものであった。
【課題を解決するための手段】
【００１３】
上記課題を解決するために、本発明の第１の形態によると、ブルームフィルタを用いて取り得る各状態を訪問して処理を行う状態探索装置であって、既訪状態を管理するブルームフィルタと、サイズの異なるブルームフィルタを利用して複数回の探索を実施する探索部と、複数回の探索におけるブルームフィルタのサイズと到達状態数との関係を近似する成長曲線を推定することにより状態カバー率を推定する状態カバー率推定部とを備える。
【００１４】
本発明の第２の形態によると、有限状態の状態遷移グラフにおける探索すべき状態空間のうち、探索し得た空間のカバー率を推定する状態カバー率推定方法であって、ブルームフィルタにより既訪状態を管理する段階と、サイズの異なるブルームフィルタを利用して複数回の探索を実施する段階と、複数回の探索におけるブルームフィルタのサイズと到達状態数との関係を近似する成長曲線を推定することにより状態カバー率を推定する段階とを備える。
【００１５】
なお、上記の発明の概要は、本発明の必要な特徴の全てを列挙したものではなく、これらの特徴群のサブコンビネーションもまた、発明となり得る。
【発明の効果】
【００１６】
以上の説明から明らかなように、この発明によれば、ブルームフィルタのサイズに応じた到達状態数の変化に伴う推定値を得ることができるため、一回の検査結果のみを用いる推定方法に比べ、精度の高い状態カバー率の推定値を求めることができる。
【図面の簡単な説明】
【００１７】
【図１】第１の実施形態に係るモデル検査器１００のブロック構成の一例を示す図である。
【図２】本発明の第１の実施形態のモデル検査器１００の動作を示すフローチャートである。
【図３】本発明の第１の実施形態の状態カバー率推定方法による推定結果の一例である。
【図４】第２の実施形態に係るモデル検査器２００のブロック構成の一例を示す図である。
【図５】本発明の第２の実施形態のモデル検査器２００の動作を示すフローチャートである。
【図６】本発明の第２の実施形態の状態カバー率推定方法による推定結果の一例である。
【図７】Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇを用いたモデル検査器９００の構成を示す図である。
【発明を実施するための形態】
【００１８】
以下、発明の実施の形態を通じて本発明を説明するが、以下の実施形態は特許請求の範囲にかかる発明を限定するものではなく、また実施形態の中で説明されている特徴の組み合わせの全てが発明の解決手段に必須であるとは限らない。
【００１９】
図１は、第１の実施形態に係るモデル検査器１００のブロック構成の一例を示す。モデル検査器１００は、モデル検査部１１０、状態カバー率推定部１２０、及び検査履歴記憶部１３０を備える。なお、モデル検査器１００は、この発明における「状態探索装置」の一例であってよい。また、モデル検査部１１０は、この発明における「探索部」の一例であってよい。
【００２０】
モデル検査部１１０は、到達状態計数部１１１とブルームフィルタ１１２を有する。モデル検査部１１０は、初期状態と状態遷移規則及び形式仕様の入力を受け付けると、初期状態と状態遷移規則によって定義される有限の状態遷移グラフを探索し、与えられた形式仕様に違反する状態を探索する。具体的には、モデル検査部１１０は、深さ優先探索などの探索アルゴリズムを使って状態グラフの探索を行う。また、モデル検査部１１０は、状態グラフの探索において、訪問済みの状態の管理にブルームフィルタ１１２を用いる。なお、「訪問」とは、状態グラフの探索において、ある状態に到達することを指す。
【００２１】
到達状態計数部１１１は、探索により到達した状態数を計数する。具体的には、状態の計数は、モデル検査部１１０がブルームフィルタ１１２に未訪問の状態を訪問済みとして追加する際に、それまでの計数値に１加算することにより行う。
【００２２】
ブルームフィルタ１１２は、モデル検査部１１０の状態グラフの探索における既訪状態を管理する。ブルームフィルタ１１２は、長さｍビットのビット列から構成され、初期状態では全てのビットがオフになっている。ブルームフィルタ１１２に対する操作は、状態の登録（追加）と登録済みかのチェック（既訪チェック）が定義される。これらの操作には、状態を入力として、０からｍ−１のハッシュ値を出力する、ｋ個のハッシュ関数を用いる。状態を追加する場合、これらのハッシュ関数を用いてｋ個のハッシュ値を求め、それらハッシュ値をインデックスとする全てのビットをオンにする。状態の既訪チェックをする場合、ｋ個のハッシュ値をインデックスとする全てのビットがオンであるとき既訪であると判断し、そうでなければ、未訪問と判断する。ブルームフィルタ１１２には、未訪問の状態を既訪と判断する偽陽性による誤判定の可能性がある。ブルームフィルタ１１２のサイズｍは、モデル検査の実行時にオプションとして指定できる。
【００２３】
検査履歴記憶部１３０は、モデル検査部１１０による複数回の検査結果を保持する。具体的には、検査時のブルームフィルタ１１２のサイズｍ（ビット数）と検査終了時の到達状態計数部１１１の計数した到達状態数Ｎが記憶される。
【００２４】
状態カバー率推定部１２０は、検査履歴記憶部１３０の保持する検査結果から状態カバー率を推定する。状態カバー率の推定は、検査結果を近似する成長曲線を推定することにより行う。ここで、成長曲線とは最初は緩やかに増加し、徐々に増加速度が速くなるが、十分大きくなると増加速度が減少し、ある値に漸近するようなＳ字型の曲線である。成長曲線は、生物の個体数やソフトウェアの累積バグ数などのモデルとして利用され、ロジスティック曲線やゴンペルツ曲線が広く知られる。
【００２５】
Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇを用いたモデル検査では、ｔは底を２とするブルームフィルタ１１２のサイズの対数、Ｍは全状態数、Ｎは到達状態数とするとき、ブルームフィルタ１１２を用いたモデル検査におけるｔとＮの関係は次の性質が言える。
【００２６】
ｔの増加によりブルームフィルタ１１２が大きくなると、擬陽性により訪問済みと判断されていた状態が未訪問と判断されることにより、到達状態数が増加する。状態カバー率が１に近づくと、ブルームフィルタ１１２により擬陽性と判断される確率は低下するため、ｔの増加による到達状態数の増加は緩やかになり、ｄＮ／ｄｔは０に近づく。
【００２７】
特に、ｔが十分小さい領域では、検査の終了時にはブルームフィルタのほぼ全てがオンビットとなる。このような条件で、ｔを１だけ減少させる場合、つまりブルームフィルタ１１２のサイズを半減させる場合、同様にブルームフィルタ１１２のほぼ全てがオンビットとなる。ｋ＝１の場合を考えると、ブルームフィルタ１１２のオンビット数は到達状態数と等しいため、ｔが１減少することによりＮは半減することが分かる。ｋが２以上の場合は、オンビット数と到達状態数は等しくはないが、ｋ＝１の場合と同様、ｔが十分小さい領域ではＮは指数的に増加する。
【００２８】
次に、ハッシュ関数の数と状態カバー率の変化の関係性について述べる。ブルームフィルタ１１２に用いるハッシュ関数の数が２の場合、ｔの増加に伴い、擬陽性と判断された状態は２つのハッシュ値のうちいずれかの衝突を避けることができれば、擬陽性と判断されなくなり到達状態数が増加する。同じ状態カバー率を達成している状態であればｔの増加量が同じであっても、ハッシュ関数の数が１の場合に比べて、２つのハッシュ値のうちどちらか一方が衝突を回避できればよいため、その確率は高くなる。同様の議論はｋを増加させた場合にも成り立つ。したがって、同じ状態カバー率を達成している状況では、ハッシュ関数の数ｋが多い方が、ｔの増加によるＮの増分は多くなる。
【００２９】
本実施形態における状態カバー率の推定には、以上の性質を満たす成長曲線を用いる。例えば、式（１）に示す微分方程式で定義される曲線を用いることができる。
【００３０】
【数２】
【００３１】
ここで、ｔは底を２とするブルームフィルタ１１２のサイズの対数、Ｎは到達状態数、Ｍは状態グラフの全状態数、ｒは増加率、ｐは状態カバー率、ｋはブルームフィルタ１１２が用いるハッシュ関数の数を表す。式（１）を解くと、次の式（２）が得られる。（Ｃは積分定数。）特に、ｋ＝１のとき式（２）はロジスティック曲線を表す。
【００３２】
【数３】
【００３３】
検査終了時に、未知な値はＭ、Ｃ、ｒである。このうちＭを推定できれば状態カバー率（Ｎ／Ｍ）の推定値を求めることができる。特にｒについては、ｔが十分小さい領域では、ｔが１増加するとＮが２倍になるという前述の議論から、ｒをｌｎ（２）としてもよい。ここで、ｌｎ（ｘ）は底をｅとするｘの対数を表す。
【００３４】
次に図２を参照して本実施形態の動作について説明する。図２は、本実施形態における状態カバー率推定の手順のフローチャートである。
【００３５】
状態カバー率を推定するために、モデル検査部１１０は複数回のモデル検査を実施する（Ｓ１〜Ｓ４）。検査の回数には、任意の値を用いてよい。ただし、少なくとも、式２における未知数の数以上は、ブルームフィルタ１１２のサイズが互いに異なる検査を行う必要がある。複数回行われる検査において、それぞれの検査ではブルームフィルタ１１２のサイズを変更して検査を実施する（Ｓ１）。ブルームフィルタ１１２のサイズの設定の具体例としては、検査毎にブルームフィルタ１１２のサイズを１／２にする方法を用いることができる。Ｓ２で実施されたモデル検査の結果は、検査履歴記憶部１３０に保持される（Ｓ３）。ここで、保持される情報は、ブルームフィルタ１１２のサイズと到達状態計数部１１１の保持する到達状態数の組である。このようにして、蓄積された検査履歴をもとに、状態カバー率推定部１２０は状態カバー率の推定値を求める（Ｓ４）。カバー率の推定には、まず、検査履歴記憶部１３０の保持するデータを近似する成長曲線を求め、全状態数Ｍを推定する（Ｓ５）。近似曲線を求めるには、例えば非線形最小二乗法を用いることができる。式２を成長曲線として用いる場合、非線形二乗法により全状態数Ｍの推定値を求めることができ、検査履歴記憶部１３０の保持する到達状態数の最大値がＮｍａｘのとき、状態カバー率はＮｍａｘ／Ｍと推定できる。
【００３６】
図３は約４０万状態の状態グラフに対して、ブルームフィルタ１１２を利用した深さ優先探索を実施した場合のブルームフィルタ１１２のサイズと実際の状態カバー率（＋）と本実施形態の手法を用いた推定値（□）、非特許文献１の計算式による推定値（△）を表している。本実施形態の手法は、非特許文献１の手法より精度の高い推定値が得られていることが分かる。
【００３７】
ＳＰＩＮのように、明示的な探索を行うモデル検査では、ある状態ｓの遷移先状態の列ｎｅｘｔ（ｓ）の順序をランダムにすることで、複数回実行時の総合的なカバー率を向上させることができる。しかし、本実施形態においてそのようなランダム性を導入した場合、各々の検査によって探索される部分グラフが大きく変わってしまい、結果として到達状態数が検査度に大きくぶれ、近似曲線の推定が上手くできない状況が生じる可能性がある。そのため、状態ｓの遷移先状態の生成順序は同一とすることが望ましい。ランダム性を導入する場合は、ブルームフィルタ１１２のサイズが同一の検査を複数回実施し、その最大値（最小値）のみを用いて状態カバー率を推定することで結果を安定させることができる。
【００３８】
本実施形態では、サイズの異なるブルームフィルタ１１２を利用した複数回のモデル検査を実施し、その結果を近似する成長曲線を推定することで状態カバー率を推定する。ブルームフィルタ１１２のサイズに応じた到達状態数の変化に応じた推定値を得ることができるため、一回の検査結果のみを用いる推定方法に比べ、精度の高い状態カバー率の推定値を求めることができる。
【００３９】
図４は、第２の実施形態に係るモデル検査器２００のブロック構成の一例を示す。モデル検査器２００は、モデル検査部２１０、状態カバー率推定部２２０、及び検査履歴記憶部２３０を備える。モデル検査器２００と、第１の実施形態に係るモデル検査器１００との相違点は、状態カバー率推定部２２０の処理が異なる点にある。その他の構成要素の機能及び動作は、第１の実施形態に係るモデル検査器１００の構成要素と同様の機能及び動作であるため、その詳細な説明を省略する。
【００４０】
具体的には、本実施形態では、第１の実施形態と比べ、２回のモデル検査で状態カバー率を推定できるという点が異なる。ブルームフィルタ２１２のサイズが２のｔ乗ビットと２の（ｔ−ｎ）乗ビットにおける到達状態数の比Ｒを、次のとおりとする。
【００４１】
【数４】
【００４２】
これを用いると、式２から状態カバー率の推定値は次式で表せる。ここで、第１の実施形態での議論からｒ＝ｌｎ（２）とする。本実施形態では、式（３）を状態カバー率の推定値として用いる。
【００４３】
【数５】
【００４４】
式（３）を用いることで、ブルームフィルタ２１２のサイズが、２のｔ乗ビットの場合と２の（ｔ−ｎ）乗ビットの場合の到達状態数が分かれば、状態カバー率を推定できることが分かる。
【００４５】
本実施形態における動作のフローチャートを図５に示す。本実施形態における状態カバー率推定部１２０は、式（３）を用いて状態カバー率の推定を行う。また、本実施形態の動作は図５に示すように、Ｓ４ｂとＳ５ｂが第１の実施形態と異なる。本実施形態では、Ｓ４ｂにおける指定回数は２回であり、Ｓ５ｂでの状態カバー率の推定は式３で行う。本実施形態におけるその他の構成、動作については、第１の実施形態と同様であり、同一の符号を付し詳細な説明を省略する。
【００４６】
図６は図３と同じ状態グラフに対して、ブルームフィルタ２１２を利用した深さ優先探索を実施した場合のブルームフィルタ２１２のサイズと実際の状態カバー率（＋）と本実施形態の手法を用いた推定値（□）、非特許文献１の計算式による推定値（△）を表している。本実施形態においても、非特許文献１の手法より精度の高い推定値が得られていることが分かる。
【００４７】
本実施形態においても、第１の実施形態同様、遷移先状態の生成順序は同一とすることが望ましく、生成順序にランダム性を導入する場合は、ブルームフィルタ２１２のサイズが同一の検査を複数回実施し、その最大値（最小値）のみを用いて状態カバー率を推定することで結果を安定させることができる。
【００４８】
本実施形態は、２回のモデル検査で精度の高い状態カバー率を推定でき、単純な式により状態カバー率を推定できるため、第１の実施形態に比べて状態カバー率の推定にかかる計算時間が短いという利点がある。
【００４９】
以上、本発明を実施の形態を用いて説明したが、本発明の技術的範囲は上記実施の形態に記載の範囲には限定されない。上記実施の形態に、多様な変更又は改良を加えることが可能であることが当業者に明らかである。その様な変更又は改良を加えた形態も本発明の技術的範囲に含まれ得ることが、特許請求の範囲の記載から明らかである。
【符号の説明】
【００５０】
１００ モデル検査器
１１０ モデル検査部
１１１ 到達状態計数部
１１２ ブルームフィルタ
１２０ 状態カバー率推定部
１３０ 検査履歴記憶部
１００ モデル検査器
２１０ モデル検査部
２１１ 到達状態計数部
２１２ ブルームフィルタ
２２０ 状態カバー率推定部
２３０ 検査履歴記憶部
【技術分野】
【０００１】
本発明は、状態探索装置、及び状態カバー率推定方法に関する。特に本発明は、ブルームフィルタを用いて取り得る各状態を訪問して処理を行う状態探索装置、並びに有限状態の状態遷移グラフにおける探索すべき状態空間のうち、探索し得た空間のカバー率を推定する状態カバー率推定方法に関する。
【背景技術】
【０００２】
モデル検査とは、システムの設計書や仕様書からモデルを作成し、モデルが検査項目を満たすかどうかを全数探索することによって不具合を発見する技術である。具体的には、モデル検査では、システムを有限状態の状態遷移グラフとしてモデルを記述する。そして、モデル検査では、その状態遷移グラフにおいて、不変条件や時相論理式によって記述された形式仕様が満たされるかどうかを検査する。
【０００３】
しかしながら、モデル検査には、状態爆発問題と呼ばれる課題もある。具体的には、モデル検査において探索すべき状態数は、検査するシステムが複雑になると指数的に増加する。モデル検査では、状態数の増加に伴い、検査に必要なメモリ量も増加する。そのため、モデル検査では、検査するシステムの規模が大きくなると、検査の途中でメモリ不足となり探索が打ち切られてしまい、ごく一部の探索空間しかカバーできなくなってしまうことがある。
【０００４】
このような問題への対処方法としては、様々な手法が採られている。例えば、ＳＰＩＮ（Ｓｉｍｐｌｅ Ｐｒｏｍｅｌａ Ｉｎｔｅｒｐｒｅｔｅｒ）と呼ばれるモデル検査器では、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇと呼ばれる手法によって、メモリ量が十分に確保できない状態での状態空間のカバー率向上を実現している。
【０００５】
また、モデル検査では、状態空間の網羅的探索を行う場合、遷移先の状態に既に訪問したかどうかを確認するために、既訪状態を保存する必要がある。データ操作の効率を考えると状態を保存するためにはハッシュテーブルを用いるのが一般的であるが、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇではブルームフィルタを用いて既訪状態を管理する。ブルームフィルタは、ある要素が集合のメンバーであるかを判定するために用いることができるデータ構造である。ただし、ブルームフィルタは確率的データ構造であり、擬陽性の可能性がある。つまり、既訪状態であることを判定するためにブルームフィルタを利用する場合、未だ訪問していないにも関わらず、既訪と判断される可能性がある。しかしながら、１状態を保持するために必要なデータ量はハッシュテーブルを用いる場合に比べ少なくてすむため、結果としてメモリが十分確保できない場合では状態空間のカバー率が向上する。
【０００６】
Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇは、メモリが少ない計算機環境においても効率的な検査を可能にする。しかしながら、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇは近似的手法であり、検査により必ずしも全ての状態の探索を行えるわけではない。したがって、検査の精度という観点から考えれば、全状態に対してどれだけのカバー率が達成できたかを利用者に対して提示できることが望ましい。
【０００７】
ところで、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇを用いたモデル検査器における状態カバー率の推定方法が知られている（例えば、非特許文献１参照。）。図７は、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇを用いたモデル検査器９００の構成を示す。モデル検査器９００は、モデル検査部９１０、及び状態カバー率推定部９２０を備える。モデル検査部９１０は、初期状態と状態遷移規則から定義される有限の状態遷移グラフを、深さ優先探索などの探索アルゴリズムにより探索し、与えられた形式仕様に違反する状態又は実行系列を探索する。モデル検査部９１０は、ブルームフィルタ９１２を用いて訪問済み状態を記憶し、到達状態計数部９１１により探索により到達した状態数を計数する。到達状態計数部９１１は、ブルームフィルタ９１２に状態が追加されるときに到達状態数をインクリメントすることで到達状態数を計数する。モデル検査部９１０による探索が完了すると、状態カバー率推定部９２０は、モデル検査部９１０から到達状態数Ｎとブルームフィルタ９１２のサイズｍ（ビット）を受け取り状態カバー率の推定値を計算する。非特許文献１に記載の状態カバー率推定値の計算式は、次のとおりである。
【０００８】
【数１】
【０００９】
この計算式は、モデル検査器ＳＰＩＮでは以前用いられていたが、精度はあまり高くない。そのため、ＳＰＩＮ ｖｅｒｓｉｏｎ ５ではこの計算式による推定値の表示を行うオプションは廃止されている。
【００１０】
モデル検査器ＳＰＩＮでは、この他に、状態カバー率の指標としてｍ／Ｎで定義されるｈａｓｈ ｆａｃｔｏｒを検査終了時に提示する。ｈａｓｈ ｆａｃｔｏｒは、１状態当たりの探索に利用できたメモリ量（ビット数）を表しており、この値が大きいほどハッシュ値の衝突が少ない。そのため、良好な状態カバー率を達成できたと判断できる。しかし、この値は十分な状態カバー率が達成できているかどうかの判定には適しているが、状態カバー率を直感的に表すものではなく、利用者が得られる情報は限定的である。モデル検査を複数回又は並列に実行することで総合的な状態カバー率を向上させる手法では、１回の検査の状態カバー率によって、十分な状態カバー率を実現するのに必要な検査の回数や並列度が異なるため、ｈａｓｈ ｆａｃｔｏｒはそのような用途におけるカバー率指標としては不十分である。
【先行技術文献】
【非特許文献】
【００１１】
【非特許文献１】ジェラルド ジェイ・ホルツマン（Ｇｅｒａｒｄ Ｊ． Ｈｏｌｚｍａｎｎ）著、「ザ スピン モデル チェッカー」、（米国）、アジソン ウェスレイ プロフェッショナル（Ａｄｄｉｓｏｎ−Ｗｅｓｌｅｙ Ｐｒｏｆｅｓｓｉｏｎａｌ）、２００３年
【発明の概要】
【発明が解決しようとする課題】
【００１２】
上述のとおり、Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇを用いたモデル検査は、利用者に提示する状態カバー率の推定値は信頼度の低いものであった。
【課題を解決するための手段】
【００１３】
上記課題を解決するために、本発明の第１の形態によると、ブルームフィルタを用いて取り得る各状態を訪問して処理を行う状態探索装置であって、既訪状態を管理するブルームフィルタと、サイズの異なるブルームフィルタを利用して複数回の探索を実施する探索部と、複数回の探索におけるブルームフィルタのサイズと到達状態数との関係を近似する成長曲線を推定することにより状態カバー率を推定する状態カバー率推定部とを備える。
【００１４】
本発明の第２の形態によると、有限状態の状態遷移グラフにおける探索すべき状態空間のうち、探索し得た空間のカバー率を推定する状態カバー率推定方法であって、ブルームフィルタにより既訪状態を管理する段階と、サイズの異なるブルームフィルタを利用して複数回の探索を実施する段階と、複数回の探索におけるブルームフィルタのサイズと到達状態数との関係を近似する成長曲線を推定することにより状態カバー率を推定する段階とを備える。
【００１５】
なお、上記の発明の概要は、本発明の必要な特徴の全てを列挙したものではなく、これらの特徴群のサブコンビネーションもまた、発明となり得る。
【発明の効果】
【００１６】
以上の説明から明らかなように、この発明によれば、ブルームフィルタのサイズに応じた到達状態数の変化に伴う推定値を得ることができるため、一回の検査結果のみを用いる推定方法に比べ、精度の高い状態カバー率の推定値を求めることができる。
【図面の簡単な説明】
【００１７】
【図１】第１の実施形態に係るモデル検査器１００のブロック構成の一例を示す図である。
【図２】本発明の第１の実施形態のモデル検査器１００の動作を示すフローチャートである。
【図３】本発明の第１の実施形態の状態カバー率推定方法による推定結果の一例である。
【図４】第２の実施形態に係るモデル検査器２００のブロック構成の一例を示す図である。
【図５】本発明の第２の実施形態のモデル検査器２００の動作を示すフローチャートである。
【図６】本発明の第２の実施形態の状態カバー率推定方法による推定結果の一例である。
【図７】Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇを用いたモデル検査器９００の構成を示す図である。
【発明を実施するための形態】
【００１８】
以下、発明の実施の形態を通じて本発明を説明するが、以下の実施形態は特許請求の範囲にかかる発明を限定するものではなく、また実施形態の中で説明されている特徴の組み合わせの全てが発明の解決手段に必須であるとは限らない。
【００１９】
図１は、第１の実施形態に係るモデル検査器１００のブロック構成の一例を示す。モデル検査器１００は、モデル検査部１１０、状態カバー率推定部１２０、及び検査履歴記憶部１３０を備える。なお、モデル検査器１００は、この発明における「状態探索装置」の一例であってよい。また、モデル検査部１１０は、この発明における「探索部」の一例であってよい。
【００２０】
モデル検査部１１０は、到達状態計数部１１１とブルームフィルタ１１２を有する。モデル検査部１１０は、初期状態と状態遷移規則及び形式仕様の入力を受け付けると、初期状態と状態遷移規則によって定義される有限の状態遷移グラフを探索し、与えられた形式仕様に違反する状態を探索する。具体的には、モデル検査部１１０は、深さ優先探索などの探索アルゴリズムを使って状態グラフの探索を行う。また、モデル検査部１１０は、状態グラフの探索において、訪問済みの状態の管理にブルームフィルタ１１２を用いる。なお、「訪問」とは、状態グラフの探索において、ある状態に到達することを指す。
【００２１】
到達状態計数部１１１は、探索により到達した状態数を計数する。具体的には、状態の計数は、モデル検査部１１０がブルームフィルタ１１２に未訪問の状態を訪問済みとして追加する際に、それまでの計数値に１加算することにより行う。
【００２２】
ブルームフィルタ１１２は、モデル検査部１１０の状態グラフの探索における既訪状態を管理する。ブルームフィルタ１１２は、長さｍビットのビット列から構成され、初期状態では全てのビットがオフになっている。ブルームフィルタ１１２に対する操作は、状態の登録（追加）と登録済みかのチェック（既訪チェック）が定義される。これらの操作には、状態を入力として、０からｍ−１のハッシュ値を出力する、ｋ個のハッシュ関数を用いる。状態を追加する場合、これらのハッシュ関数を用いてｋ個のハッシュ値を求め、それらハッシュ値をインデックスとする全てのビットをオンにする。状態の既訪チェックをする場合、ｋ個のハッシュ値をインデックスとする全てのビットがオンであるとき既訪であると判断し、そうでなければ、未訪問と判断する。ブルームフィルタ１１２には、未訪問の状態を既訪と判断する偽陽性による誤判定の可能性がある。ブルームフィルタ１１２のサイズｍは、モデル検査の実行時にオプションとして指定できる。
【００２３】
検査履歴記憶部１３０は、モデル検査部１１０による複数回の検査結果を保持する。具体的には、検査時のブルームフィルタ１１２のサイズｍ（ビット数）と検査終了時の到達状態計数部１１１の計数した到達状態数Ｎが記憶される。
【００２４】
状態カバー率推定部１２０は、検査履歴記憶部１３０の保持する検査結果から状態カバー率を推定する。状態カバー率の推定は、検査結果を近似する成長曲線を推定することにより行う。ここで、成長曲線とは最初は緩やかに増加し、徐々に増加速度が速くなるが、十分大きくなると増加速度が減少し、ある値に漸近するようなＳ字型の曲線である。成長曲線は、生物の個体数やソフトウェアの累積バグ数などのモデルとして利用され、ロジスティック曲線やゴンペルツ曲線が広く知られる。
【００２５】
Ｂｉｔｓｔａｔｅ Ｈａｓｈｉｎｇを用いたモデル検査では、ｔは底を２とするブルームフィルタ１１２のサイズの対数、Ｍは全状態数、Ｎは到達状態数とするとき、ブルームフィルタ１１２を用いたモデル検査におけるｔとＮの関係は次の性質が言える。
【００２６】
ｔの増加によりブルームフィルタ１１２が大きくなると、擬陽性により訪問済みと判断されていた状態が未訪問と判断されることにより、到達状態数が増加する。状態カバー率が１に近づくと、ブルームフィルタ１１２により擬陽性と判断される確率は低下するため、ｔの増加による到達状態数の増加は緩やかになり、ｄＮ／ｄｔは０に近づく。
【００２７】
特に、ｔが十分小さい領域では、検査の終了時にはブルームフィルタのほぼ全てがオンビットとなる。このような条件で、ｔを１だけ減少させる場合、つまりブルームフィルタ１１２のサイズを半減させる場合、同様にブルームフィルタ１１２のほぼ全てがオンビットとなる。ｋ＝１の場合を考えると、ブルームフィルタ１１２のオンビット数は到達状態数と等しいため、ｔが１減少することによりＮは半減することが分かる。ｋが２以上の場合は、オンビット数と到達状態数は等しくはないが、ｋ＝１の場合と同様、ｔが十分小さい領域ではＮは指数的に増加する。
【００２８】
次に、ハッシュ関数の数と状態カバー率の変化の関係性について述べる。ブルームフィルタ１１２に用いるハッシュ関数の数が２の場合、ｔの増加に伴い、擬陽性と判断された状態は２つのハッシュ値のうちいずれかの衝突を避けることができれば、擬陽性と判断されなくなり到達状態数が増加する。同じ状態カバー率を達成している状態であればｔの増加量が同じであっても、ハッシュ関数の数が１の場合に比べて、２つのハッシュ値のうちどちらか一方が衝突を回避できればよいため、その確率は高くなる。同様の議論はｋを増加させた場合にも成り立つ。したがって、同じ状態カバー率を達成している状況では、ハッシュ関数の数ｋが多い方が、ｔの増加によるＮの増分は多くなる。
【００２９】
本実施形態における状態カバー率の推定には、以上の性質を満たす成長曲線を用いる。例えば、式（１）に示す微分方程式で定義される曲線を用いることができる。
【００３０】
【数２】
【００３１】
ここで、ｔは底を２とするブルームフィルタ１１２のサイズの対数、Ｎは到達状態数、Ｍは状態グラフの全状態数、ｒは増加率、ｐは状態カバー率、ｋはブルームフィルタ１１２が用いるハッシュ関数の数を表す。式（１）を解くと、次の式（２）が得られる。（Ｃは積分定数。）特に、ｋ＝１のとき式（２）はロジスティック曲線を表す。
【００３２】
【数３】
【００３３】
検査終了時に、未知な値はＭ、Ｃ、ｒである。このうちＭを推定できれば状態カバー率（Ｎ／Ｍ）の推定値を求めることができる。特にｒについては、ｔが十分小さい領域では、ｔが１増加するとＮが２倍になるという前述の議論から、ｒをｌｎ（２）としてもよい。ここで、ｌｎ（ｘ）は底をｅとするｘの対数を表す。
【００３４】
次に図２を参照して本実施形態の動作について説明する。図２は、本実施形態における状態カバー率推定の手順のフローチャートである。
【００３５】
状態カバー率を推定するために、モデル検査部１１０は複数回のモデル検査を実施する（Ｓ１〜Ｓ４）。検査の回数には、任意の値を用いてよい。ただし、少なくとも、式２における未知数の数以上は、ブルームフィルタ１１２のサイズが互いに異なる検査を行う必要がある。複数回行われる検査において、それぞれの検査ではブルームフィルタ１１２のサイズを変更して検査を実施する（Ｓ１）。ブルームフィルタ１１２のサイズの設定の具体例としては、検査毎にブルームフィルタ１１２のサイズを１／２にする方法を用いることができる。Ｓ２で実施されたモデル検査の結果は、検査履歴記憶部１３０に保持される（Ｓ３）。ここで、保持される情報は、ブルームフィルタ１１２のサイズと到達状態計数部１１１の保持する到達状態数の組である。このようにして、蓄積された検査履歴をもとに、状態カバー率推定部１２０は状態カバー率の推定値を求める（Ｓ４）。カバー率の推定には、まず、検査履歴記憶部１３０の保持するデータを近似する成長曲線を求め、全状態数Ｍを推定する（Ｓ５）。近似曲線を求めるには、例えば非線形最小二乗法を用いることができる。式２を成長曲線として用いる場合、非線形二乗法により全状態数Ｍの推定値を求めることができ、検査履歴記憶部１３０の保持する到達状態数の最大値がＮｍａｘのとき、状態カバー率はＮｍａｘ／Ｍと推定できる。
【００３６】
図３は約４０万状態の状態グラフに対して、ブルームフィルタ１１２を利用した深さ優先探索を実施した場合のブルームフィルタ１１２のサイズと実際の状態カバー率（＋）と本実施形態の手法を用いた推定値（□）、非特許文献１の計算式による推定値（△）を表している。本実施形態の手法は、非特許文献１の手法より精度の高い推定値が得られていることが分かる。
【００３７】
ＳＰＩＮのように、明示的な探索を行うモデル検査では、ある状態ｓの遷移先状態の列ｎｅｘｔ（ｓ）の順序をランダムにすることで、複数回実行時の総合的なカバー率を向上させることができる。しかし、本実施形態においてそのようなランダム性を導入した場合、各々の検査によって探索される部分グラフが大きく変わってしまい、結果として到達状態数が検査度に大きくぶれ、近似曲線の推定が上手くできない状況が生じる可能性がある。そのため、状態ｓの遷移先状態の生成順序は同一とすることが望ましい。ランダム性を導入する場合は、ブルームフィルタ１１２のサイズが同一の検査を複数回実施し、その最大値（最小値）のみを用いて状態カバー率を推定することで結果を安定させることができる。
【００３８】
本実施形態では、サイズの異なるブルームフィルタ１１２を利用した複数回のモデル検査を実施し、その結果を近似する成長曲線を推定することで状態カバー率を推定する。ブルームフィルタ１１２のサイズに応じた到達状態数の変化に応じた推定値を得ることができるため、一回の検査結果のみを用いる推定方法に比べ、精度の高い状態カバー率の推定値を求めることができる。
【００３９】
図４は、第２の実施形態に係るモデル検査器２００のブロック構成の一例を示す。モデル検査器２００は、モデル検査部２１０、状態カバー率推定部２２０、及び検査履歴記憶部２３０を備える。モデル検査器２００と、第１の実施形態に係るモデル検査器１００との相違点は、状態カバー率推定部２２０の処理が異なる点にある。その他の構成要素の機能及び動作は、第１の実施形態に係るモデル検査器１００の構成要素と同様の機能及び動作であるため、その詳細な説明を省略する。
【００４０】
具体的には、本実施形態では、第１の実施形態と比べ、２回のモデル検査で状態カバー率を推定できるという点が異なる。ブルームフィルタ２１２のサイズが２のｔ乗ビットと２の（ｔ−ｎ）乗ビットにおける到達状態数の比Ｒを、次のとおりとする。
【００４１】
【数４】
【００４２】
これを用いると、式２から状態カバー率の推定値は次式で表せる。ここで、第１の実施形態での議論からｒ＝ｌｎ（２）とする。本実施形態では、式（３）を状態カバー率の推定値として用いる。
【００４３】
【数５】
【００４４】
式（３）を用いることで、ブルームフィルタ２１２のサイズが、２のｔ乗ビットの場合と２の（ｔ−ｎ）乗ビットの場合の到達状態数が分かれば、状態カバー率を推定できることが分かる。
【００４５】
本実施形態における動作のフローチャートを図５に示す。本実施形態における状態カバー率推定部１２０は、式（３）を用いて状態カバー率の推定を行う。また、本実施形態の動作は図５に示すように、Ｓ４ｂとＳ５ｂが第１の実施形態と異なる。本実施形態では、Ｓ４ｂにおける指定回数は２回であり、Ｓ５ｂでの状態カバー率の推定は式３で行う。本実施形態におけるその他の構成、動作については、第１の実施形態と同様であり、同一の符号を付し詳細な説明を省略する。
【００４６】
図６は図３と同じ状態グラフに対して、ブルームフィルタ２１２を利用した深さ優先探索を実施した場合のブルームフィルタ２１２のサイズと実際の状態カバー率（＋）と本実施形態の手法を用いた推定値（□）、非特許文献１の計算式による推定値（△）を表している。本実施形態においても、非特許文献１の手法より精度の高い推定値が得られていることが分かる。
【００４７】
本実施形態においても、第１の実施形態同様、遷移先状態の生成順序は同一とすることが望ましく、生成順序にランダム性を導入する場合は、ブルームフィルタ２１２のサイズが同一の検査を複数回実施し、その最大値（最小値）のみを用いて状態カバー率を推定することで結果を安定させることができる。
【００４８】
本実施形態は、２回のモデル検査で精度の高い状態カバー率を推定でき、単純な式により状態カバー率を推定できるため、第１の実施形態に比べて状態カバー率の推定にかかる計算時間が短いという利点がある。
【００４９】
以上、本発明を実施の形態を用いて説明したが、本発明の技術的範囲は上記実施の形態に記載の範囲には限定されない。上記実施の形態に、多様な変更又は改良を加えることが可能であることが当業者に明らかである。その様な変更又は改良を加えた形態も本発明の技術的範囲に含まれ得ることが、特許請求の範囲の記載から明らかである。
【符号の説明】
【００５０】
１００ モデル検査器
１１０ モデル検査部
１１１ 到達状態計数部
１１２ ブルームフィルタ
１２０ 状態カバー率推定部
１３０ 検査履歴記憶部
１００ モデル検査器
２１０ モデル検査部
２１１ 到達状態計数部
２１２ ブルームフィルタ
２２０ 状態カバー率推定部
２３０ 検査履歴記憶部
【特許請求の範囲】
【請求項１】
ブルームフィルタを用いて取り得る各状態を訪問して処理を行う状態探索装置であって、
既訪状態を管理するブルームフィルタと、
サイズの異なる前記ブルームフィルタを利用して複数回の探索を実施する探索部と、
前記複数回の探索における前記ブルームフィルタのサイズと到達状態数との関係を近似する成長曲線を推定することにより状態カバー率を推定する状態カバー率推定部と
を備える状態探索装置。
【請求項２】
前記成長曲線は、到達状態数、全状態数、前記ブルームフィルタに用いるハッシュ関数の数、及び前記ブルームフィルタのサイズの各値を用いて定義される曲線である
請求項１に記載の状態探索装置。
【請求項３】
前記状態カバー率の推定には、非線形最小二乗法を用いる
請求項１又は２に記載の状態探索装置。
【請求項４】
前記状態カバー率の推定には、前記ブルームフィルタのサイズが異なる２回の探索の検査結果を用い、それらの到達状態数の比を用いる
請求項２に記載の状態探索装置。
【請求項５】
前記状態カバー率の推定には、前記２回の探索に用いた前記ブルームフィルタのサイズの比と前記到達状態数の比の差を用いる
請求項２乃至４のいずれかに記載の状態探索装置。
【請求項６】
前記複数回の探索において遷移先状態の生成順序を同一にする
請求項１乃至５のいずれかに記載の状態探索装置。
【請求項７】
有限状態の状態遷移グラフにおける探索すべき状態空間のうち、探索し得た空間のカバー率を推定する状態カバー率推定方法であって、
ブルームフィルタにより既訪状態を管理する段階と、
サイズの異なる前記ブルームフィルタを利用して複数回の探索を実施する段階と、
前記複数回の探索における前記ブルームフィルタのサイズと到達状態数との関係を近似する成長曲線を推定することにより状態カバー率を推定する段階と
を備える状態カバー率推定方法。
【請求項１】
ブルームフィルタを用いて取り得る各状態を訪問して処理を行う状態探索装置であって、
既訪状態を管理するブルームフィルタと、
サイズの異なる前記ブルームフィルタを利用して複数回の探索を実施する探索部と、
前記複数回の探索における前記ブルームフィルタのサイズと到達状態数との関係を近似する成長曲線を推定することにより状態カバー率を推定する状態カバー率推定部と
を備える状態探索装置。
【請求項２】
前記成長曲線は、到達状態数、全状態数、前記ブルームフィルタに用いるハッシュ関数の数、及び前記ブルームフィルタのサイズの各値を用いて定義される曲線である
請求項１に記載の状態探索装置。
【請求項３】
前記状態カバー率の推定には、非線形最小二乗法を用いる
請求項１又は２に記載の状態探索装置。
【請求項４】
前記状態カバー率の推定には、前記ブルームフィルタのサイズが異なる２回の探索の検査結果を用い、それらの到達状態数の比を用いる
請求項２に記載の状態探索装置。
【請求項５】
前記状態カバー率の推定には、前記２回の探索に用いた前記ブルームフィルタのサイズの比と前記到達状態数の比の差を用いる
請求項２乃至４のいずれかに記載の状態探索装置。
【請求項６】
前記複数回の探索において遷移先状態の生成順序を同一にする
請求項１乃至５のいずれかに記載の状態探索装置。
【請求項７】
有限状態の状態遷移グラフにおける探索すべき状態空間のうち、探索し得た空間のカバー率を推定する状態カバー率推定方法であって、
ブルームフィルタにより既訪状態を管理する段階と、
サイズの異なる前記ブルームフィルタを利用して複数回の探索を実施する段階と、
前記複数回の探索における前記ブルームフィルタのサイズと到達状態数との関係を近似する成長曲線を推定することにより状態カバー率を推定する段階と
を備える状態カバー率推定方法。
【図１】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【図２】
【図３】
【図４】
【図５】
【図６】
【図７】
【公開番号】特開２０１１−１４５９９０（Ｐ２０１１−１４５９９０Ａ）
【公開日】平成２３年７月２８日（２０１１．７．２８）
【国際特許分類】
【出願番号】特願２０１０−８２１５（Ｐ２０１０−８２１５）
【出願日】平成２２年１月１８日（２０１０．１．１８）
【出願人】（０００００４２３７）日本電気株式会社 (19,353)
【Ｆターム（参考）】
【公開日】平成２３年７月２８日（２０１１．７．２８）
【国際特許分類】
【出願日】平成２２年１月１８日（２０１０．１．１８）
【出願人】（０００００４２３７）日本電気株式会社 (19,353)
【Ｆターム（参考）】
[ Back to top ]