"第1のクロック信号で動作する第1の回路部と、第2のクロック信号で動作する第2の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第1の回路部と前記第2の回路部間でのデータの送受信を行うハンドシェイク部を抽出する抽出部と、抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第1の回路部と前記第2の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する検証部と、を有することを特徴とする検証装置。前記信号が、前記データの送受信時に満たすべき条件を記述した第1の検証用情報を生成する検証用情報生成部を有し、前記検証部は、生成された前記第1の検証用情報を用いて、前記信号が前記手順を満たすか否か検証することを特徴とする請求項1に記載の検証装置。前記検証用情報生成部は、前記手順を満たさない前記信号があるとき、前記第1の回路部と前記第2の回路部のうち当該信号を出力する側で、当該信号が前記データの送受信時に前記手順を満たす場合の条件を記述した第2の検証用情報を生成し、前記検証部は、生成された前記第2の検証用情報を用いて、前記信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証することを特徴とする請求項2に記載の検証装置。コンピュータによって実行される検証方法であって、第1のクロック信号で動作する第1の回路部と、第2のクロック信号で動作する第2の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第1の回路部と前記第2の回路部間でのデータの送受信を行うハンドシェイク部を抽出し、抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第1の回路部と前記第2の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する、ことを特徴とする検証方法。第1のクロック信号で動作する第1の回路部と、第2のクロック信号で動作する第2の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第1の回路部と前記第2の回路部間でのデータの送受信を行うハンドシェイク部を抽出し、抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第1の回路部と前記第2の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する、処理をコンピュータに実行させるプログラム。しかしながら、従来の手法では、回路全体に対して検証を行うことになるため、ハンドシェイクを行う部分以外の機能検証も同時に行うことになる。そのため、検証を実施する条件の組み合わせが膨大なものになり、検証コストや、検証時間が増加する問題があった。発明の一観点によれば、以下に示すような検証装置が提供される。この検証装置は、第1のクロック信号で動作する第1の回路部と、第2のクロック信号で動作する第2の回路部とを含む検証対象回路から、ハンドシェイクの手順に従って前記第1の回路部と前記第2の回路部間でのデータの送受信を行うハンドシェイク部を抽出する抽出部と、抽出された前記ハンドシェイク部の信号が、前記手順を満たすかを検証し、前記手順を満たさない前記信号があるとき、前記第1の回路部と前記第2の回路部のうち当該信号を出力する側で、当該信号が前記手順を満たさなくなる条件が回路動作時に起こり得るか検証する検証部と、を備える。開示の検証装置、検証方法及びプログラムによれば、検証する範囲を少なくでき、検証コストや検証時間の増大を抑制することができる。以下、本発明の実施の形態を、図面を参照しつつ説明する。第1の実施の形態図1は、第1の実施の形態の検証装置の一例を示す図である。検証装置10は、記憶部11、抽出部12、検証部13を有している。記憶部11は、検証対象データD1を記憶している。検証対象データD1は、検証対象回路図1の例では論理回路20を、たとえば、Verilogや、VHDLVeryhighspeedintegratedcircuitHardwareDescriptionLanguageなどのハードウェア記述言語などで記述したデータである。論理回路20は、互いに異なるクロックで動作する回路部21,22を有するものである。すなわち、回路部21,22は、異なるクロックで動作するクロックドメインとなる。回路部21,22間でハンドシェイクの手順に従ってデータの送受信を行う部分が、ハンドシェイク部23である。ハンドシェイク部23には、複数のFFが含まれる。抽出部12は、論理回路20から、ハンドシェイク部23を抽出する。たとえば、抽出部12は、検証対象データD1に含まれる論理回路20の回路記述から、ハンドシェイク部23の回路記述を抽出する。検証部13は、抽出されたハンドシェイク部23に対して、シミュレーションを行い、ハンドシェイク部23の信号が、ハンドシェイクの手順を満たすか検証する。ハンドシェイクの手順を満たさない信号があるとき、検証部13は、回路部21,22のうち、その信号を出力する側で、その信号がハンドシェイクの手順を満たさなくなる条件が、回路動作時に起こり得るか検証する。図2は、ハンドシェイクの手順の一例を示す図である。図2では、回路部21がA_DATA[:0]というデータを回路部22に送信するときのハンドシェイクの手順の一例が示されている。FF30,31は、ハンドシェイク部23の回路部22側に含まれるFFであり、回路部22で用いられるクロック信号がクロック端子に入力される。FF32,33は、ハンドシェイク部23の回路部21側に含まれるFFであり、回路部21で用いられるクロック信号がクロック端子に入力される。回路部21がA_DATA[:0]というデータを回路部22に送信するとき、回路部22は、リクエスト信号A_REQをアサートする図2の例では1とすることを示す。A_REQは、回路部22のFF30に入力される。回路部22で用いられるクロック信号に同期して、A_REQはFF30からFF31に伝達され、FF31の出力信号であるA_REQ_q2がアサートされる。A_REQ_q2がアサートされると、回路部22側で、A_DATAがB_DATAとして受信される。その後、回路部22側で、受信が行われたことを示す信号B_ACKがアサートされる。B_ACKは、回路部21のFF32に入力される。回路部21で用いられるクロック信号に同期して、B_ACKはFF32からFF33に伝達され、FF33の出力信号であるB_ACK_q2がアサートされる。B_ACK_q2がアサートされると、回路部21は、A_REQをデアサートする図2の例では0とすることを示す。A_REQの変化は、回路部22のFF30,31を介して伝わり、A_REQ_q2がデアサートされる。A_REQ_q2がデアサートされると、回路部22は、B_ACKをデアサートする。B_ACKの変化は、回路部21のFF32,33を介して伝わり、B_ACK_q2がデアサートされる。図3は、ハンドシェイク部のRTLRegisterTransferLevelの回路記述の一つ目の例である。回路記述は、Verilogで記述されており、前述したハンドシェイク部23の回路部22側で出力される信号であるB_ACKが変化する条件が示されている。図3の1行目では、回路部22のクロック信号BCLKの立ち上がりエッジ、または、論理回路20のリセット信号RSTの立ち下がりエッジに同期して、以下の行の処理を行うことが示されている。2,3行目では、RSTが0のとき、B_ACKが0B_ACK<=1’b0となることが示されている。なお、1’は1ビットを示し、bは2進数であることを示している。4,5行目では、RSTが0でないとき、回路部22のみのリセット信号B_RSTが0、回路部22内のカウンタ値B_CNTが15のとき、もしくはA_REQ_q2が0で、かつB_CNTが0のとき、B_ACKが0となることが示されている。なお、4’は4ビット、hは16進数であることを示している。6,7行目では、A_REQ_q2が1のときに、B_ACKが1となることが示されている。図4は、ハンドシェイク部のRTLの回路記述の二つ目の例である。回路記述は、Verilogで記述されており、前述したハンドシェイク部23の回路部21側で出力される信号であるA_REQが変化する条件が示されている。図4の1行目では、回路部21のクロック信号ACLKの立ち上がりエッジ、または、論理回路20のリセット信号RSTの立ち下がりエッジに同期して、以下の行の処理を行うことが示されている。2,3行目では、RSTが0のとき、A_REQが0となることが示されている。4,5行目では、RSTが0でないとき、回路部21内のカウンタ値A_CNTが2、かつB_ACK_q2が1のとき、A_REQが0となることが示されている。6,7行目では、A_CNTが0のときに、A_REQが1となることが示されている。検証部13は、抽出された、図3、図4のようなハンドシェイク部23の回路記述において、A_REQやB_ACKなどの信号が、図2に示したようなハンドシェイクの手順を満たすか検証する。たとえば、検証部13は、A_REQ_q2がアサートされたにもかかわらず、回路部22だけのリセットや、ある条件などによりB_ACKがアサートされなくなった場合、B_ACKがハンドシェイクの手順を満たさないと判定する。このとき、検証部13は、B_ACKを出力する側の回路部22で、B_ACKがアサートされない条件が、回路動作時に起こり得るか検証する。このように、本実施の形態の検証装置10によれば、ハンドシェイク部23の検証を行い、ハンドシェイクの手順を満たさない信号があるときには、その信号を出力する側の回路部で検証を行うので、検証する範囲を少なくできる。これにより、検証コストや検証時間の増大を抑制することができる。第2の実施の形態図5は、第2の実施の形態の検証装置の一例を示す図である。第1の実施の形態の検証装置10と同様の要素については同一符号を付し、説明を省略する。第2の実施の形態の検証装置10aは、検証用情報生成部14を有している。検証用情報生成部14は、抽出部12で抽出されたハンドシェイク部23の信号をもとに、検証部13で検証を行うための検証用情報以下検証プロパティと呼ぶを生成する。検証用情報生成部14は、検証部13が行う2段階の検証、すなわち、前述したハンドシェイク部23の検証と、ハンドシェイクの手順を満たさないと判定された信号を出力する側の回路部の検証の、それぞれの検証用の検証プロパティを生成する。検証プロパティは、たとえば、SystemVerilog、e言語、PSLPropertySpecificationLanguageなどの検証記述言語で記述される。ハンドシェイク部23の検証用に生成される検証プロパティには、データ送受信時に、ハンドシェイク部23の信号が満たすべき条件つまりハンドシェイクの手順を満たすような条件が記述される。ハンドシェイクの手順を満たさないと判定された信号を出力する側の回路部の検証時に生成される検証プロパティには、手順を満たさないと判定された信号が、その回路部において、データ送受信時に手順を満たす場合の条件が記述される。そして、検証部13は、この2種類の検証プロパティを用いて検証を行う。2番目の検証では、検証部13は、検証プロパティBに記述された条件が偽になる場合が、回路動作時において存在するか否かによって、回路部21,22間のデータ送受信時にデッドロックが発生するか否か検証する。図6は、第2の実施の形態の検証装置による検証方法の一例の流れを説明するフローチャートである。なお、以下では、図1に示したような論理回路20に対して検証を行う場合を例にして説明する。まず、抽出部12は、論理回路20から、ハンドシェイク部23を抽出するステップS10。たとえば、抽出部12は、論理回路20の回路記述から、図3や図4に示したようなハンドシェイク部23の回路記述を抽出する。さらに、抽出部12は、ハンドシェイク部23の信号A_REQ,A_REQ_q2,B_ACK,BACK_q2を抽出するステップS11。ステップS10,S11の処理において、抽出部12は、0-InCDCClockDomainCrossingなどの検証ツールを適用してもよい。その後、検証用情報生成部14は、抽出されたハンドシェイク部23とその信号をもとに、ハンドシェイク部23の検証を行うための検証プロパティ以下検証プロパティAと呼ぶを生成するステップS12。図7は、検証プロパティAの例を示す図である。図7では、検証プロパティAとして、アサーション設計対象の論理回路で期待されている動作などを記述した文をSystemVerilogで記述した、3つの検証プロパティの例が示されている。各検証プロパティの1行目の1_b_ack_ast、2_a_req_dast、3_b_ack_dastが、それぞれの検証プロパティ名である。検証プロパティ名が1_b_ack_astの検証プロパティは、前述したハンドシェイクの手順のように、A_REQ_q2がアサートされるとB_ACKがアサートされるかどうかを検証するためのものである。2行目には、この検証プロパティの内容が記述されている。回路部22のクロック信号BCLKの立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、RSTが0のとき、この検証プロパティを無効にすること、A_REQ_q2が1アサートの状態が1サイクル以上連続して成り立つ場合、次のサイクルでB_ACKが1アサートになることが示されている。3行目では、検証プロパティの終わりが示されており、4行目では、1_b_ack_astの検証プロパティが偽と判断された場合、エラーとすることが示されている。検証プロパティ名が2_a_req_dastの検証プロパティは、前述したハンドシェイクの手順のように、B_ACK_q2がアサートされるとA_REQがデアサートされるかどうかを検証するためのものである。2行目には、この検証プロパティの内容として、回路部21のクロック信号ACLKの立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、RSTが0のとき、この検証プロパティを無効にすること、B_ACK_q2が1アサートの状態が1サイクル以上連続して成り立つ場合、次のサイクルでA_REQが0デアサートになることが示されている。3行目では、検証プロパティの終わりが示されており、4行目では、2_a_req_dastの検証プロパティが偽と判断された場合、エラーとすることが示されている。検証プロパティ名が3_b_ack_dastの検証プロパティは、前述したハンドシェイクの手順のように、A_REQ_q2がデアサートされるとB_ACKがデアサートされるかどうかを検証するためのものである。2行目には、この検証プロパティの内容として、回路部22のクロック信号BCLKの立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、RSTが0のとき、この検証プロパティを無効にすること、A_REQ_q2が1アサートの状態が1サイクル以上連続して成り立つ場合、次のサイクルでB_ACKが0デアサートになることが示されている。3行目では、検証プロパティの終わりが示されており、4行目では、3_b_ack_dastの検証プロパティが偽と判断された場合、エラーとすることが示されている。検証部13は、上記のような検証プロパティAを用いてハンドシェイク部23の形式的検証を行いステップS13、エラーが発生するか否かを判定するステップS14。図7に示した、検証プロパティ名が1_b_ack_astの検証プロパティAを適用した形式検証では、A_REQ_q2がアサートされるとB_ACKがアサートされるかどうかが検証される。たとえば、図3に示したように記述されているハンドシェイク部23の場合、回路部22のリセット信号B_RSTが0になっていたりすると、A_REQ_q2がアサートの状態にもかかわらず、B_ACKは0となり、アサートされない。このような場合、検証部13はエラーが発生したと判定する。検証部13は、同様に、検証プロパティ名が2_a_req_dast,3_b_ack_dastの検証プロパティAについても検証を行い、エラーが発生するか否かを判定する。検証の結果、エラーが生じたと判定された場合、検証用情報生成部14は、ハンドシェイクの手順を満たさない信号を出力する側の回路部を検証するための検証プロパティ以下検証プロパティBと呼ぶを生成するステップS15。検証用情報生成部14は、たとえば、検証プロパティ名が1_b_ack_astの検証プロパティAを用いた検証でエラーが発生したときには、ハンドシェイク部23からB_ACK部分の論理をトレースし、B_ACKが1にならない条件を抽出する。そして、検証用情報生成部14は、抽出した条件が、回路部22の動作レベルで発生するかどうかを確認する検証プロパティBを生成する。図8は、検証プロパティ名が1_b_ack_astの検証プロパティAを用いた検証でエラーが発生したときに生成される検証プロパティBの例である。図8では、検証プロパティBとして、アサーションをSystemVerilogで記述した、2つの検証プロパティの例が示されている。各検証プロパティの1行目の4_b_ack_ast_practice,5_b_ack_ast_practice2が、それぞれの検証プロパティ名である。検証プロパティ名が4_b_ack_ast_practiceの検証プロパティBでは、回路部22のクロック信号BCLKの立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、RSTが0のとき、この検証プロパティBを無効にすること、A_REQ_q2が1アサートの状態が1サイクル以上連続したとき、B_RSTが1になっていることが示されている。検証プロパティ名が5_b_ack_ast_practice2の検証プロパティBでも、回路部22のクロック信号BCLKの立ち上がりエッジに同期してこの検証プロパティが動作することが示されている。さらに、RSTが0のとき、この検証プロパティBを無効にすること、A_REQ_q2が1アサートの状態が1サイクル以上連続したときには、回路部22のカウンタ値B_CNTは15ではないことが示されている。3行目では、検証プロパティBの終わりが示されており、4行目では、上記の検証プロパティBの内容が偽と判断された場合、エラーとすることが示されている。検証用情報生成部14は、たとえば、検証プロパティ名が2_a_req_dastの検証プロパティAを用いた検証でエラーが発生したときには、ハンドシェイク部23からA_REQ部分の論理をトレースし、A_REQが0にならない条件を抽出する。そして、検証用情報生成部14は、抽出した条件が、回路の動作レベルで発生するかどうかを確認する検証プロパティBを生成する。図9は、検証プロパティ名が2_a_req_dastの検証プロパティAを用いた検証でエラーが発生したときに生成される検証プロパティBの例である。1行目の6_a_req_ast_practiceが、検証プロパティ名である。2行目には、この検証プロパティBの内容が記述されており、回路部21のクロック信号ACLKの立ち上がりエッジに同期してこの検証プロパティBが動作することが示されている。さらに、RSTが0のとき、この検証プロパティBを無効にすること、B_ACK_q2が1アサートの状態が1サイクル以上連続するとき、次のサイクルでA_CNTが2になることが示されている。3行目では、検証プロパティBの終わりが示されており、4行目では、上記の検証プロパティBの内容が偽と判断された場合、エラーとすることが示されている。検証用情報生成部14は、たとえば、検証プロパティ名が3_b_ack_dastの検証プロパティAを用いた検証でエラーが発生したときには、ハンドシェイク部23からB_ACK部分の論理をトレースし、B_ACKが1にならない条件を抽出する。そして、検証用情報生成部14は、抽出した条件が、回路の動作レベルで発生するかどうかを確認する検証プロパティBを生成する。図10は、検証プロパティ名が3_b_ack_dastの検証プロパティAを用いた検証でエラーが発生したときに生成される検証プロパティBの例である。1行目の7_b_ack_ast_practiceが、検証プロパティ名である。2行目には、この検証プロパティBの内容が記述されており、回路部22のクロック信号BCLKの立ち上がりエッジに同期してこの検証プロパティBが動作することが示されている。さらに、RSTが0のとき、この検証プロパティBを無効にすること、A_REQ_q2が1アサートの状態が1サイクル以上連続するとき、次のサイクルでB_CNTが0になることが示されている。3行目では、検証プロパティBの終わりが示されており、4行目では、上記の検証プロパティBの内容が偽と判断された場合、エラーとすることが示されている。検証部13は、上記のような検証プロパティBを用いて、ハンドシェイクの手順を満たさない信号を出力する側の回路部の動作レベル実使用レベルの検証形式検証または動的検証を行いステップ16、その結果を出力するステップS17。なお、ステップS14の処理で、エラーが発生しないと判定された場合には、ハンドシェイク部23でデッドロックは発生しない旨の検証結果が出力される。ステップS16では、たとえば、以下のような検証が行われる。たとえば、図8に示した検証プロパティBが生成された場合、A_REQ_q2がアサートされたにもかかわらずB_ACKがアサートされない条件があるということを示している。このとき検証部13は、B_ACKを出力する回路部22において、検証プロパティBを用いて、A_REQ_q2がアサートされたにもかかわらずB_ACKがアサートされない条件が回路動作時に起こり得るか検証する。検証部13は、A_REQ_q2が1の状態が1サイクル以上連続したとき、B_RSTが1でなく、回路部22がリセット状態のままである場合が回路部22の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部13は、ハンドシェイク部23でデッドロックが発生する可能性があることを検証結果として出力する。また、検証部13は、A_REQ_q2が1の状態が1サイクル以上連続したとき、回路部22のカウンタ値B_CNTが15のままである場合が回路部22の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部13は、ハンドシェイク部23でデッドロックが発生する可能性があることを検証結果として出力する。一方、図9に示した検証プロパティBが生成された場合、B_ACK_q2がアサートされたにもかかわらずA_REQがデアサートされない条件があるということを示している。このとき検証部13は、A_REQに変化を与える側の回路部21において、検証プロパティBを用いて、B_ACK_q2がアサートされたにもかかわらずA_REQがデアサートされない条件が回路動作時に起こり得るか検証する。検証部13は、B_ACK_q2が1の状態が1サイクル以上連続しても、A_CNTが2にならない場合が、回路部22の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部13は、ハンドシェイク部23でデッドロックが発生する可能性があることを検証結果として出力する。また、図10に示した検証プロパティBが生成された場合、A_REQ_q2がデアサートされたにもかかわらずB_ACKがデアサートされない条件があるということを示している。このとき検証部13は、B_ACKを出力する側の回路部22において、検証プロパティBを用いて、A_REQ_q2がデアサートされたにもかかわらずB_ACKがデアサートされない条件が回路動作時に起こり得るか検証する。検証部13は、A_REQ_q2が1の状態が1サイクル以上連続しても、B_CNTが0にならない場合が、回路部22の動作レベルで存在するとき、上記の条件が起こり得ると判定する。そのため、検証部13は、ハンドシェイク部23でデッドロックが発生する可能性があることを検証結果として出力する。以上のように第2の実施の形態の検証装置10a及び検証方法によれば、検証プロパティAを生成して、検証することで、論理回路の非同期部分であるハンドシェイク部23の検証漏れを抑制できる。また、検証プロパティAを用いてハンドシェイク部23の検証を行い、ハンドシェイクの手順を満たさない信号があるときには、その信号を出力する側の回路部で検証プロパティBを用いて検証を行うので、検証する範囲を少なくできる。これにより、検証コストや検証時間の増大を抑制できる。また、ハンドシェイク部23のデッドロックを見逃さなくなるので、各クロックドメイン別に検証を進めることも可能となる。なお、上記のような第1及び第2の実施の形態の検証装置10,10aは、以下のようなコンピュータにより実現可能である。図11は、本実施の形態に用いるコンピュータのハードウェアの一構成例を示す図である。コンピュータ100は、CPUCentralProcessingUnit101によって装置全体が制御されている。CPU101には、バス108を介してRAMRandomAccessMemory102と複数の周辺機器が接続されており、検証装置10,10aの各部の機能を実現する。RAM102は、コンピュータ100の主記憶装置として使用される。RAM102には、CPU101に実行させるOSOperatingSystemのプログラムやアプリケーションプログラムの少なくとも一部が一時的に格納される。また、RAM102には、CPU101による処理に用いる各種データが格納される。バス108に接続されている周辺機器としては、ハードディスクドライブHDDHardDiskDrive103、グラフィック処理装置104、入力インタフェース105、光学ドライブ装置106、及び通信インタフェース107がある。HDD103は、内蔵したディスクに対して、磁気的にデータの書き込み及び読み出しを行う。HDD103は、コンピュータ100の二次記憶装置として使用される。HDD103には、OSのプログラム、各種検証ツールなどのアプリケーションプログラム、及び図1に示した検証対象データD1などの各種データが格納される。なお、二次記憶装置としては、フラッシュメモリなどの半導体記憶装置を使用することもできる。グラフィック処理装置104には、モニタ104aが接続されている。グラフィック処理装置104は、CPU101からの命令に従って、検証結果などの画像をモニタ104aの画面に表示させる。モニタ104aとしては、CRTCathodeRayTubeを用いた表示装置や液晶表示装置などがある。入力インタフェース105には、キーボード105aとマウス105bとが接続されている。入力インタフェース105は、キーボード105aやマウス105bから送られてくる信号をCPU101に送信する。なお、マウス105bは、ポインティングデバイスの一例であり、他のポインティングデバイスを使用することもできる。他のポインティングデバイスとしては、タッチパネル、タブレット、タッチパッド、トラックボールなどがある。光学ドライブ装置106は、レーザ光などを利用して、光ディスク106aに記録されたデータの読み取りを行う。光ディスク106aは、光の反射によって読み取り可能なようにデータが記録された可搬型の記録媒体である。光ディスク106aには、DVDDigitalVersatileDisc、DVD-RAM、CD-ROMCompactDiscReadOnlyMemory、CD-RRecordable/RWReWritableなどがある。通信インタフェース107は、ネットワーク107aに接続されている。通信インタフェース107は、ネットワーク107aを介して、他のコンピュータまたは通信機器との間でデータの送受信を行う。以上のようなハードウェア構成によって、本実施の形態の処理機能を実現することができる。また、検証装置10,10aが有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータたとえば、図11のようなコンピュータ100で実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、磁気記憶装置、光ディスク、光磁気記録媒体、半導体メモリなどがある。磁気記憶装置には、HDD、フレキシブルディスクFD、磁気テープなどがある。光ディスクには、DVD、DVD-RAM、CD-ROM/RWなどがある。光磁気記録媒体には、MOMagnetoOpticaldiskなどがある。プログラムを流通させる場合には、たとえば、そのプログラムが記録されたDVD、CD-ROMなどの可搬型記録媒体が販売される。また、プログラムをサーバコンピュータの記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。プログラムを実行するコンピュータは、たとえば、可搬型記録媒体に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶装置に格納する。そして、コンピュータは、自己の記憶装置からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、可搬型記録媒体から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、ネットワークを介して接続されたサーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムにしたがった処理を実行することもできる。また、上記の処理機能の少なくとも一部を、DSPDigitalSignalProcessor、ASICApplicationSpecificIntegratedCircuit、PLDProgrammableLogicDeviceなどの電子回路で実現することもできる。以上、実施の形態に基づき、本発明の検証装置、検証方法及びプログラムの一観点について説明してきたが、これらは一例にすぎず、上記の記載に限定されるものではない。"