"第1の装置から第2の装置への通信中に指定順序とは異なる順序でパケットが送信されたことが検出された場合に、前記第1の装置内のレジスタ群の状態を示すスナップショットを取得し、取得された前記スナップショットに含まれているレジスタ群の各々のレジスタに関する識別情報と値との組み合わせを抽出し、抽出された各組み合わせの抽出回数に基づいて前記各組み合わせの出現頻度を算出し、前記各組み合わせについて、前記組み合わせと当該組み合わせに対応する出現頻度とを出力する、処理をコンピュータに実行させることを特徴とする検証支援プログラム。前記出力する処理は、前記各組み合わせについて、前記組み合わせと当該組み合わせに対応する出現頻度と前記組み合わせの選択入力を受け付けるインターフェース情報とを有する選択画面を表示することを特徴とする請求項1に記載の検証支援プログラム。前記インターフェース情報から少なくともいずれか1つの組み合わせについての選択入力を受け付け、前記選択入力が受け付けられた前記少なくともいずれか1つの組み合わせについては、前記指定順序とは異なる順序でのパケットの送信とみなさない旨を示す制約条件を有する論理関数を生成する、処理を前記コンピュータに実行させ、前記出力する処理は、生成された前記論理関数を出力することを特徴とする請求項2に記載の検証支援プログラム。前記出力する処理は、前記論理関数を、前記第1の装置から前記第2の装置へのデータ通信中に前記指定順序とは異なる順序でデータ通信されたことを検出する監視装置に送信することを特徴とする請求項3に記載の検証支援プログラム。第1の装置から第2の装置への通信中に指定順序とは異なる順序でパケットが送信されたことが検出された場合に、前記第1の装置内のレジスタ群の状態を示すスナップショットを取得する取得部と、前記取得部によって取得された前記スナップショットに含まれているレジスタ群の各々のレジスタに関する識別情報と値との組み合わせを抽出する抽出部と、前記抽出部によって抽出された各組み合わせの抽出回数に基づいて前記各組み合わせの出現頻度を算出する算出部と、前記各組み合わせについて、前記組み合わせと当該組み合わせに対応する出現頻度とを出力する出力部と、を有することを特徴とする検証支援装置。コンピュータが、第1の装置から第2の装置への通信中に指定順序とは異なる順序でパケットが送信されたことが検出された場合に、前記第1の装置内のレジスタ群の状態を示すスナップショットを取得し、取得された前記スナップショットに含まれているレジスタ群の各々のレジスタに関する識別情報と値との組み合わせを抽出し、抽出された各組み合わせの抽出回数に基づいて前記各組み合わせの出現頻度を算出し、前記各組み合わせについて、前記組み合わせと当該組み合わせに対応する出現頻度とを出力する、ことを特徴とする検証支援方法。しかしながら、パケットがスキップされる論理的なルールやアサーションを検証者が仕様書に記載すると、記載ミスが発生しがちである。そのような仕様書を読んだ者は、パケットがスキップされる論理的なルールやアサーションについて誤った解釈をしてしまうことになる。このような解釈は擬似エラーの原因となり、重要なプロパティが監視から外れてしまうことになる。本発明は、パケットがスキップされる論理的なルールの探索の容易化を図ることを目的とする。本発明の一側面によれば、第1の装置から第2の装置への通信中に指定順序とは異なる順序でパケットが送信されたことが検出された場合に、前記第1の装置内のレジスタ群の状態を示すスナップショットを取得し、取得されたスナップショットに含まれているレジスタ群の各々のレジスタに関する識別情報と値との組み合わせを抽出し、抽出された各組み合わせの抽出回数に基づいて前記各組み合わせの出現頻度を算出し、前記各組み合わせについて、前記組み合わせと当該組み合わせに対応する出現頻度とを出力する検証支援プログラム、検証支援装置、および検証支援方法が提案される。本発明の一側面によれば、パケットがスキップされる論理的なルールの探索の容易化を図ることができるという効果を奏する。以下に添付図面を参照して、この発明にかかる検証支援プログラム、検証支援装置、および検証支援方法の実施の形態を詳細に説明する。<検証支援例>図1は、本実施の形態にかかる検証支援例を示す説明図である。送信元装置101は、送信先装置102に対し、パケットを送信する送信元装置101である。送信元装置101が検証対象となる。送信元装置101は、たとえば、USBUniversalSerialBusホストコントローラを有する通信装置である。また、送信元装置101は、トランザクションごとの一連のパケットPをフレーム単位で送信する。送信先装置102は、送信元装置101から送信されてくるパケットを受信する通信装置である。送信先装置102は、たとえば、USBデバイスである。監視装置103は、送信元装置101と送信先装置102とのデータ通信を監視する装置である。具体的には、たとえば、監視装置103は、送信元装置101から送信されるフレームにおいてパケットがスキップされたことを検出する。各パケットには、どのトランザクションに所属しているかを識別可能なトランザクションIDidentificationが付与されている。トランザクションIDは、たとえば、連続番号とする。この場合、監視装置103は、スキップ前後のパケットのトランザクションIDを参照することで、どのトランザクションのパケットがスキップされたかを特定することができる。ここで、パケットがスキップされる原因には、たとえば、送信元装置101の動作が不正確でありエラーが発生する不当な場合と、通信プロトコルや送信元装置101に関する設計仕様で決められて発生する正当な場合と、がある。検証支援装置104は、監視装置103がパケットのスキップを検出したときの送信元装置101内のレジスタ群の状態を示すスナップショット群から、パケットがスキップされる論理的なルールを探索する。具体的には、たとえば、検証支援装置104は、スナップショット群から、レジスタとその値の組み合わせごとの出現頻度を算出する。出現頻度としては、たとえば、出現確率や出現回数が採用される。以下、検証支援の動作手順について説明する。1まず、送信元装置101は、監視装置103からの指示により、送信先装置102へのデータ通信に関するシミュレーションを実行する。そして、監視装置103は、データ通信を監視し、シミュレーション中に発生するパケットのスキップを検出する。監視装置103でパケットのスキップが検出される都度、スキップ発生時のレジスタ群の各レジスタの値を示すスナップショットが送信元装置101から得られる。21のシミュレーションが終了すると、検証支援装置104は、蓄積されたスナップショット群106を取得する。検証支援装置104は、スナップショット群106から、スキップ発生時でのレジスタとその値の組み合わせの出現回数を集計する。集計内容については、図3で後述する。検証支援装置104は、組み合わせごとに出現確率を算出する。そして、検証支援装置104は、スキップ時のレジスタの状態とスキップ時の出現確率とチェックボックスを含む選択画面105を表示する。これにより、ユーザは、スキップ発生時にどの組み合わせの状態がどのくらいの頻度で発生しているかを把握することができる。また、チェックボックスは、ユーザ操作によりレジスタの状態を選択させるためのインターフェース情報である。3検証支援装置104は、ユーザ操作によりレジスタの状態の選択を受け付ける。選択されたチェックボックスにはチェックマークとなるレ点が入力されている。図1では、ActiveBit=0、ErrorCounter=0にレ点が入力されている。すなわち、ユーザは、エラー原因には成りえないレジスタの状態に対しレ点を入力することで、後述の論理関数によりエラーの対象外とすることができる。4検証支援装置104は、論理関数107を生成する。論理関数107とは、制約条件を満たした場合は真であり、満たさなかった場合は偽とするアサーションである。検証支援装置104は、ユーザがチェックボックスで選択したレジスタとその値の組み合わせを制約条件とした論理関数107を生成する。たとえば、図1では、ActiveBit=0、ErrorCounter=0にレ点が入力されているため、ActiveBit=0、ErrorCounter=0を真とし、それ以外を偽とする論理関数107が生成される。5生成された論理関数107は、監視装置103に付与される。監視装置103は、付与された論理関数107をスキップ発生時の制約条件として、再度1のシミュレーションを実行する。監視装置103は、制約条件を満たしている場合は、当該スキップは、通信プロトコルや送信元装置101に関する設計仕様で決められて発生する正当な処理であるとして、検出対象外とする。一方、制約条件を満たしていない場合は、1で説明したように、監視装置103は、スキップを検出する。これにより、当該スキップ検出時のスナップショットが取得されることになる。図2は、再度1のシミュレーションを実行したことにより得られるスキップ時のレジスタの状態とスキップ時の出現確率とチェックボックスの選択画面105の表示例である。図1では、論理関数107によりActiveBit=0およびErrorCounter=0のときのスキップはスキップとして検出されない。このため、Aのように、レジスタの状態は、ErrorCounter=15、ActiveBit=1、受信完了フラグ=1となる。ユーザは、この表示結果を見て、エラーカウンタの値が0でないときにスキップの出現確率が他のレジスタの状態に比べて高いことがわかる。このため、ユーザは、エラーカウンタを計数させる処理がスキップの原因であると推測することができる。また、Bのように、再度シミュレーションをしたときのレジスタの状態がエラーカウンタ≠0で、出現確率の総和が100になったとする。このような場合、エラーカウンタ≠0のときにのみスキップが発生したことを意味するため、ユーザは、エラーカウンタを計数させる処理がスキップの原因であると突き止めることができる。また、Cのように、再度シミュレーションをしたときのレジスタの状態がActiveBit=1のみで、出現確率が100になったとする。このような場合、ActiveBit=1のときにのみスキップが発生したことを意味するため、ユーザは、アクティブビットの値を1にする処理がスキップの原因であると突き止めることができる。このように、1~5を繰り返すことにより、レジスタの状態は、ユーザにとって必要なものに絞り込まれる。たとえば、図1では、3において、ActiveBit=0、ErrorCounter=0にレ点が入力されている。したがって、次回のシミュレーションで、スキップ発生時にActiveBit=0またはErrorCounter=0である場合には、スキップ検出対象外となる。そのため、スキップ検出されたレジスタの状態について出現回数の計数や出現確率の算出が実行される。これにより、ユーザは、スキップが発生する場合のルール、換言すれば、レジスタがどのような状態のときにスキップが発生するかを突き止めることができる。<レジスタの状態の集計例>図3は、レジスタの状態の集計例を示す説明図である。レジスタの状態の集計は、図1では、2で実行される。A上述したように、送信元装置101は、トランザクションごとの一連のパケットをフレーム単位で送信する。ここで、1フレームのデータ構造について説明する。フレームの先頭はSOFStartOfFrameである。SOFは、フレームの先頭を示すパケットである。P1~Pnは、トランザクション1~nに対応するパケットである。パケットP1~Pnは、1フレーム中に1または複数回送信される。トランザクションごとのパケットPiは同一データでもよく異なるデータでもよい。図2では、先頭のフレームの2順目のパケットP1~Pnにおいて、パケットPiが何らかの原因でスキップされたことを示している。BパケットPiのスキップが検出されると、スキップ検出時のレジスタの状態がスナップショットSiとして取得される。ここでは、送信元装置101のレジスタR1~R3の状態として、レジスタR1の値0、レジスタR2の値4、レジスタR3の値1が取得されている。Cこのあと、検証支援装置104は、レジスタ状態テーブル300を用いて、レジスタごとに、レジスタの値の出現回数を計数する。ここでは、例として、レジスタR1を上述したActiveBit、レジスタR2を上述したErrorCounter、レジスタR3を受信完了フラグとする。レジスタR1の値は0であるため、検証支援装置104は、レジスタR1の値0の出現回数を5から6にカウントアップする。また、レジスタR2の値は4であるため、検証支援装置104は、レジスタR2の値4の出現回数を6から7にカウントアップする。また、レジスタR3の値は1であるため、検証支援装置104は、レジスタR3の値1の出現回数を4から5にカウントアップする。これにより、スナップショットが得られる都度計数が実行されることになる。<システム構成例>図4は、本実施の形態にかかる検証支援システムのシステム構成例を示す説明図である。検証支援システムは、送信元装置101と、送信先装置102と、監視装置103と、トランザクタ400と、検証支援装置104と、を有する。トランザクタ400は、送信元装置101のレジスタ群の状態を示すスナップショットを取得する。具体的には、たとえば、トランザクタ400は、監視装置103からのパケットのスキップ検出信号を受信したタイミングで、送信元装置101の各レジスタの値をスナップショットとして取得する。トランザクタ400は、スキップ検出信号を受信する都度、スナップショットが得られ、スナップショット群106となる。なお、図3では、トランザクタ400は、独立した装置として規定したが、監視装置103または検証支援装置104に組み込まれていてもよい。<送信元装置101のハードウェア構成例>図5は、送信元装置101のハードウェア構成例を示すブロック図である。送信元装置101は、CPUCentralProcessingUnit501と、メモリ502と、USBホストコントローラ503と、これらを接続するバス504と、を有する。CPU501は、送信元装置101の全体の制御を司る。メモリ502は、CPU501のワークエリアとして使用される。また、メモリ502は、各種データを記憶する。USBホストコントローラ503は、フレーム単位で時間を管理し、パケットの送信を制御する。また、USBホストコントローラ503は、送信元装置101の状態を示すレジスタ群を有し、状態に応じた値を設定する。具体的には、たとえば、USBホストコントローラ503は、上述したアクティブビットとして規定されたレジスタR1や、エラーカウンタとして規定されたレジスタR2や、受信完了フラグとして規定されたレジスタR3を有する。そして、USBホストコントローラ503は、送信先装置102とのデータ通信中に、レジスタR1~R3の値を書き換える。たとえば、USBホストコントローラ503は、エラーが発生したら、レジスタR2の値を1に書き換え、エラーが発生しなくなったら再度、レジスタR2の値を0に書き換える。<検証支援装置104のハードウェア構成例>図6は、実施の形態にかかる検証支援装置104のハードウェア構成例を示すブロック図である。図6において、検証支援装置104は、CPU601と、ROMReadOnlyMemory602と、RAMRandomAccessMemory603と、磁気ディスクドライブHardDiskDrive604と、磁気ディスク605と、光ディスクドライブ606と、光ディスク607と、ディスプレイ608と、I/FInterface609と、キーボード610と、マウス611と、スキャナ612と、プリンタ613と、を備えている。また、各構成部はバス600によってそれぞれ接続されている。ここで、CPU601は、検証支援装置104の全体の制御を司る。ROM602は、ブートプログラムなどのプログラムを記憶している。RAM603は、CPU601のワークエリアとして使用される。磁気ディスクドライブ604は、CPU601の制御にしたがって磁気ディスク605に対するデータのリード/ライトを制御する。磁気ディスク605は、磁気ディスクドライブ604の制御で書き込まれたデータを記憶する。光ディスクドライブ606は、CPU601の制御にしたがって光ディスク607に対するデータのリード/ライトを制御する。光ディスク607は、光ディスクドライブ606の制御で書き込まれたデータを記憶したり、光ディスク607に記憶されたデータをコンピュータに読み取らせたりする。ディスプレイ608は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ608は、たとえば、液晶ディスプレイ、プラズマディスプレイなどを採用することができる。インターフェース以下、I/Fと略する。609は、通信回線を通じてLANLocalAreaNetwork、WANWideAreaNetwork、インターネットなどのネットワーク614に接続され、このネットワーク614を介して他の装置に接続される。そして、I/F609は、ネットワーク614と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。I/F609には、たとえばモデムやLANアダプタなどを採用することができる。キーボード610は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス611は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。スキャナ612は、画像を光学的に読み取り、検証支援装置104内に画像データを取り込む。なお、スキャナ612は、OCROpticalCharacterReader機能を持たせてもよい。また、プリンタ613は、画像データや文書データを印刷する。プリンタ613には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。なお、光ディスクドライブ606、光ディスク607、ディスプレイ608、キーボード610、マウス611、スキャナ612、およびプリンタ613の少なくともいずれか1つは、なくてもよい。<検証支援装置104の機能的構成例>図7は、検証支援装置104の機能的構成例を示すブロック図である。検証支援装置104は、取得部701と、抽出部702と、算出部703と、出力部704と、受付部705と、生成部706と、を有する。取得部701~生成部706は、具体的には、たとえば、図6に示したROM602、RAM603、磁気ディスク605、光ディスク607などの記憶装置に記憶されたプログラムをCPU601に実行させることにより、または、I/F609により、その機能を実現する。取得部701は、第1の装置から第2の装置へのデータ通信中に指定順序とは異なる順序でパケットが送信されたことが検出された場合に、第1の装置内のレジスタ群の状態を示すスナップショットを取得する。具体的には、たとえば、取得部701は、送信元装置101から送信先装置102へのデータ通信中に監視装置103においてパケットのスキップが検出された場合に、送信元装置101内のレジスタ群の状態を示すスナップショットを取得する。図1~図4に示した例の場合、監視装置103がパケットのスキップを検出すると、監視装置103はトランザクタ400に対しスキップ検出信号を送信する。トランザクタ400は、監視装置103からのスキップ検出信号を受信すると、送信元装置101内のUSBコントローラにアクセスして送信元装置101内のレジスタ群からレジスタごとにレジスタに関する識別情報と値との組み合わせを抽出する。レジスタごとのレジスタに関する識別情報と値との組み合わせが1回のスキップでのスナップショットとなる。そして、取得部701は、シミュレーション中にトランザクタ400から出力されたスナップショット群106を取得することになる。抽出部702は、取得部701によって取得されたスナップショットに含まれているレジスタ群の各々のレジスタに関する識別情報と値との組み合わせを抽出する。具体的には、たとえば、抽出部702は、スナップショット群106の各スナップショットから、レジスタに関する識別情報と値との組み合わせを抽出する。たとえば、図3に示したように、抽出部702は、スナップショットSiからレジスタR1のレジスタ名R1と値0の組み合わせ、レジスタR2のレジスタ名R2と値4の組み合わせ、レジスタR3のレジスタ名R3と値1の組み合わせを抽出する。算出部703は、抽出部702によって抽出された各組み合わせの抽出回数に基づいて各組み合わせの出現頻度を算出する。具体的には、算出部703は、組み合わせごとに出現回数を計数し、出現頻度を算出する。ここで、出現頻度とは、単に出現回数でもよく、出現確率でもよい。出現確率の場合、算出部703は、全組み合わせの総出現回数を分母とし、各組み合わせの出現回数を分子とすることにより、出現確率を算出する。たとえば、図3のCが最終的な計数結果になった場合、分母になる総出現回数は、24回=632715である。分子はそれぞれ、レジスタR1の値0の6回、レジスタR1の値1の3回、レジスタR2の値0の2回、レジスタR2の値4の7回、レジスタR2の値2の1回、レジスタR3の値1の5回となる。これにより、レジスタの値ごとに、出現確率が算出される。算出部703は、シミュレーションの終了後に算出処理を実行するが、シミュレーション中に算出処理を実行してもよい。出力部704は、各組み合わせについて、組み合わせと当該組み合わせに対応する出現頻度とを出力する。具体的には、たとえば、出力部704は、組み合わせと当該組み合わせに対応する出現頻度とを、ディスプレイ608に表示出力したり、プリンタ613に印刷出力したり、他の装置、たとえば、監視装置103に送信したりする。ディスプレイ608に表示出力する場合、出力部704は、図1の2に示したような選択画面105を表示する。図1の2の場合、さらに、組み合わせの選択入力を受け付けるインターフェース情報の一例としてチェックボックスが表示されている。インターフェース情報は、チェックボックスに限らずラジオボタンなど入力装置からの操作入力で選択できるインターフェース情報であればよい。受付部705は、インターフェース情報から少なくともいずれか1つの組み合わせについての選択入力を受け付ける。具体的には、たとえば、図1の3に示したように、受付部705は、入力装置からの操作入力により、チェックボックスにレ点の入力を受け付ける。生成部706は、受付部705によって選択入力が受け付けられた少なくともいずれか1つの組み合わせについては、指定順序とは異なる順序でのパケットの送信とみなさない旨を示す制約条件を有する論理関数を生成する。具体的には、たとえば、生成部706は、図1の4に示した論理関数107を生成する。論理関数107は、図1の3で選択入力された組み合わせについて、スキップが発生した場合であってもスキップの検出対象外とする制約条件を規定する。生成部706によって制約条件が生成された場合、出力部704は、生成された制約条件を監視装置103に送信する。監視装置103は、生成部706から送信されてきた制約条件を次回以降のシミュレーションに適用する。たとえば、図1の4の論理関数107の例では、ActiveBit=0またはErrorCounter=0の場合がスキップの検出対象外となる。したがって、次回以降のシミュレーションで、スキップ発生時のレジスタR1、R2の状態がActiveBit=0またはErrorCounter=0である場合には、監視装置103は、スキップ検出対象外となり、このときのスキップについては、監視装置103からスキップ検出信号が発行されず、スナップショットが得られないことになる。このように、監視装置103は、ユーザによって選択されたレジスタの状態を次回以降のシミュレーションから除外することができる。<監視装置103の監視処理手順>図8は、監視装置103のシミュレーション中における監視処理手順例を示すフローチャートである。まず、監視装置103は、送信元装置101から送信先装置102へのデータ通信のシミュレーションが終了しているか否かを判断するステップS801。終了していない場合ステップS801:No、監視装置103は、図3のAに示したように、パケットのスキップが発生したか否かを判断するステップS802。スキップが発生していない場合ステップS802:No、ステップS801に戻る。スキップが発生した場合ステップS802:Yes、監視装置103は、検証支援装置104からの制約条件があるか否かを判断するステップS803。制約条件がない場合ステップS803:No、ステップS808に移行する。一方、制約条件がある場合ステップS803:Yes、監視装置103は、レジスタの状態の取得要求をトランザクタ400に送信するステップS804。監視装置103は、トランザクタ400からレジスタ群の状態が受信できなかった場合ステップS805:No、ステップS801に戻る。一方、受信できた場合ステップS805:Yes、監視装置103は、受信したレジスタ群の状態を参照して、制約条件を満たしているか否かを判断するステップS806。満たしている場合ステップS806:Yes、発生したスキップは検出対象外となるため、監視装置103は、トランザクタ400に検出対象外信号を送信してステップS807、ステップS801に戻る。一方、制約条件を満たさない場合ステップS806:No、ステップS808に移行する。ステップS808では、監視装置103は、スキップを検出したことを示すスキップ検出信号をトランザクタ400に送信してステップS808、ステップS801に戻る。そして、ステップS801において、シミュレーションが終了した場合ステップS801:Yes、監視装置103は一連の処理を終了する。このように、監視装置103は、制約条件の有無や制約条件の遵守または違反に応じて、トランザクタ400によるスナップショットの取得を制御することができる。<トランザクタ400のスナップショット取得処理手順>図9は、トランザクタ400によるスナップショット取得処理手順例を示すフローチャートである。まず、トランザクタ400は、監視装置103からステップS804での取得要求を受信したか否かを判断するステップS901。受信していない場合ステップS901:No、ステップS901に戻る。一方、受信した場合ステップS901:Yes、トランザクタ400は、送信元装置101のUSBホストコントローラ503にアクセスしてレジスタ群の状態を取得するステップS902。そして、トランザクタ400は、取得要求のレスポンスとして、取得したレジスタ群の状態を監視装置103に送信するステップS903。このあと、トランザクタ400は、監視装置103からの信号の受信を待ち受けるステップS904。受信した信号がスキップ検出信号である場合ステップS904:スキップ検出、トランザクタ400は、ステップS902で取得したレジスタ群の状態をスナップショットとして、検証支援装置104がアクセス可能な記憶装置に保存するステップS905。そして、ステップS901に戻る。また、受信した信号が検出対象外信号である場合ステップS904:対象外、トランザクタ400は、ステップS902で取得したレジスタ群の状態を消去してステップS906、ステップS901に戻る。このように、トランザクタ400は、検出すべきスキップが発生したときの送信元装置101のレジスタ群の状態をスナップショットとして取得することができる。<検証支援処理手順>図10は、検証支援装置104による検証支援処理手順を示すフローチャートである。検証支援装置104は、まず、図3のB,Cに示したような集計処理を実行するステップS1001。集計処理ステップS1001の詳細な処理手順については図11で説明する。集計処理ステップS1001により、検証支援装置104は、図1の2に示したようなレジスタの状態ごとの出現頻度を得ることができる。検証支援装置104は、集計処理ステップS1101のあと、図1の2に示したように、レジスタの状態ごとに出現頻度を算出しステップS1002、表示出力するステップS1003。このあと、検証支援装置104は、ユーザによる入力装置からの操作により、レジスタの状態の選択入力を受け付けて、確定入力を待ち受けるステップS1004:No。確定入力があった場合ステップS1004:Yes、検証支援装置104は、選択項目であるレジスタの状態を特定してステップS1005、論理関数107を生成するステップS1006。そして、検証支援装置104は、生成した論理関数107を出力するステップS1007。これにより、検証支援装置104は、一連の処理を終了する。このように、検証支援装置104は、シミュレーションが終了する都度、論理関数107を生成して監視装置103に提供することができる。したがって、ユーザは、スキップが発生する場合のルール、換言すれば、レジスタがどのような状態のときにスキップが発生するかを絞り込むことができる。図11は、図10に示した集計処理ステップS1001の詳細な処理手順例を示すフローチャートである。まず、検証支援装置104は、スナップショット群106の中から未選択のスナップショットがあるか否かを判断するステップS1101。未選択のスナップショットがある場合ステップS1101:Yes、検証支援装置104は、未選択のスナップショットを1つ選択するステップS1102。そして、検証支援装置104は、選択したスナップショットの中から未選択のレジスタがあるか否かを判断するステップS1103。未選択のレジスタがない場合ステップS1103:No、ステップS1101に戻る。未選択のレジスタがある場合ステップS1103:Yes、検証支援装置104は、未選択のレジスタを1つ選択しステップS1104、レジスタ状態テーブル300に登録済みか否かを判断するステップS1105。登録済みである場合ステップS1105:Yes、ステップS1107に移行する。一方、登録済みでない場合ステップS1105:No、検証支援装置104は、選択レジスタの項目をレジスタ状態テーブル300に登録してステップS1106、ステップS1107に移行する。ステップS1107では、検証支援装置104は、選択レジスタの値をスナップショットから抽出しステップS1107、登録済みか否かを判断するステップS1108。登録済みである場合ステップS1108:Yes、ステップS1110に移行する。一方、登録済みでない場合ステップS1108:No、検証支援装置104は、選択レジスタの値とその出現回数Nの初期値N=0を登録してステップS1109、ステップS1110に移行して一連の処理を終了する。ステップS1110では、検証支援装置104は、選択レジスタについて抽出した値の出現回数NをインクリメントしステップS1110、ステップS1101に戻る。また、ステップS1101において、未選択のスナップショットがない場合ステップS1101:No、ステップS1002に移行する。このように、集計処理ステップS1001では、検証支援装置104は、シミュレーション中に取得されたスナップショット群106から、レジスタの値の出現回数をレジスタの値ごとに集計することができる。したがって、検証支援装置104は、どのレジスタがどのような値のときにスキップが何回発生したかを計数することができる。このように、本実施の形態によれば、検証支援装置104は、スキップ発生時のレジスタの値とその出現回数から、レジスタの値ごとに、出現頻度を算出して、出力する。したがって、シミュレーション中にスキップが発生したときに送信元装置101がどのような状態であったかを把握することができる。また、このような状態が、レジスタの値ごとに出現頻度として得られる。ここで、あるレジスタのある値がスキップの正当な処理であることをユーザが理解している場合には、ユーザはそのレジスタの値と出現頻度について選択入力することで、検証支援装置104は論理関数107を生成する。これにより、次回以降のシミュレーションにおいて選択入力されたレジスタの値については出現回数が計数されない。したがって、監視装置103によるシミュレーションと、生成された論理関数107の監視装置103への付与と、が繰り返されることにより、検証支援装置104は、エラーの発生原因となるスキップに絞り込んで、エラー発生原因となるパケットがスキップされる論理的なルールを突き止めることができる。また、上述した実施の形態では、送信先装置102を1台の装置を例に挙げて説明したが、送信先装置102は複数台でもよい。この場合、送信元装置101のUSBホストコントローラ503は、送信先装置102のアドレスも専用のレジスタで逐次管理することになる。この場合、スキップが発生すると、送信先装置102のアドレスもレジスタの値として読み出され、レジスタ状態テーブル300に登録されることになる。したがって、検証支援装置104は、送信先装置102ごとにエラー原因となる処理を突き止めることができる。以上説明したように、検証支援プログラム、検証支援装置、および検証支援方法によれば、パケットがスキップされる論理的なルールの探索の容易化を図ることができるという効果を奏する。"