(57)【要約】【課題】チェッカの検出精度を高めること。【解決手段】論理回路の正当性を検証する際に用いる、事前条件発生時に事後条件の発生の有無を検査する第１のチェッカ２ａを読み込む読み込み部１ｂと、読み込み部１ｂが読み込んだ第１のチェッカ２ａに基づき、事前条件未発生時には事後条件が発生しないことを検査する第２のチェッカ２ｂを生成する生成部１ｃと、を有する。【選択図】図１
2013200745.tif 000002
【特許請求の範囲】
【請求項１】
論理回路の正当性を検証する際に、事前条件発生時に事後条件の発生の有無を検査する第１のチェッカを読み込む読み込み部と、
前記読み込み部が読み込んだ第１のチェッカに基づき、事前条件未発生時には事後条件が発生しないことを検査する第２のチェッカを生成する生成部と、
を有することを特徴とする情報処理装置。
【請求項２】
前記生成部は、前記第１のチェッカに記載された事前条件と事後条件間の最小許容間隔から最大許容間隔まで事前条件の論理和を追加して前記第２のチェッカを生成することを特徴とする請求項１記載の情報処理装置。
【請求項３】
前記読み込み部が読み込んだ第１のチェッカに同じ事後条件に対して事前条件が複数存在するチェッカが存在する場合、前記生成部は、複数の前記事前条件のうちのいずれか１つが成立した場合に前記論理回路の論理が正当であると判断する情報を前記第２のチェッカに追加することを特徴とする請求項１記載の情報処理装置。
【請求項４】
前記生成部は、前記第１のチェッカに含まれるアサーションのうち、事後条件が同じアサーションが存在するか否かを判断し、判断結果に基づき事後条件が同じアサーション同士を同じグループのアサーションに関連づけることを特徴とする請求項１記載の情報処理装置。
【請求項５】
コンピュータが、
論理回路の正当性を検証する際に、事前条件発生時に事後条件の発生の有無を検査する第１のチェッカを読み込み、
読み込んだ第１のチェッカに基づき、事前条件未発生時には事後条件が発生しないことを検査する第２のチェッカを生成する、
ことを特徴とする情報処理方法。
【請求項６】
コンピュータに、
論理回路の正当性を検証する際に、事前条件発生時に事後条件の発生の有無を検査する第１のチェッカを読み込み、
読み込んだ第１のチェッカに基づき、事前条件未発生時には事後条件が発生しないことを検査する第２のチェッカを生成する、
処理を実行させることを特徴とするプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は情報処理装置、情報処理方法およびプログラムに関する。
【背景技術】
【０００２】
ＬＳＩ（Large Scale Integration）開発では、設計仕様を基にレジスタ・トランスファ・レベル（RTL: Register Transfer Level）と呼ばれる記述方法を用い、論理式を組み合わせて回路の論理を表現する。ＲＴＬで設計された論理回路が仕様どおりの機能・動作を実現できているかどうかを検証するために、計算機を用いて論理シミュレーションを行う。
【０００３】
このとき、仕様違反が起きた場合にそれを自動で検出するための機構として、ＰＳＬ（Property Specification Language）／ＳＶＡ（System Verilog Assertion）といったアサーション言語で記述されるチェッカを開発する。これを論理シミュレーションに適用し、チェッカの検出結果を基に論理回路が仕様に違反していないかどうかを確認する。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開２００８−３１０６６３号公報
【特許文献２】特開２０１０−１１３３９５号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
例えば事前条件が発生した場合に事後条件の発生有無を検査し、事後条件が発生していればチェックをパスし、事後条件が発生していなければエラーを検出するチェッカを考える。
【０００６】
このチェッカは、論理障害の影響等により事前条件が発生していないにもかかわらず、事後条件が発生した場合には、検査を開始する条件が満たされないため事後条件を検出することができない。このように、論理障害による意図しない動作の発生や、仕様書に記載されていない条件における動作の発生が生じた場合、検出漏れが発生するという問題がある。
【０００７】
１つの側面では、本発明は、チェッカの検出精度を高めることを目的とする。
【課題を解決するための手段】
【０００８】
上記目的を達成するために、開示の情報処理装置が提供される。この情報処理装置は、読み込み部と、生成部とを有している。
読み込み部は、論理回路の正当性を検証する際に用いる、事前条件発生時に事後条件の発生の有無を検査する第１のチェッカを読み込む。生成部は、読み込み部が読み込んだ第１のチェッカに基づき、事前条件未発生時には事後条件が発生しないことを検査する第２のチェッカを生成する。
【発明の効果】
【０００９】
１態様では、チェッカの検出精度を高めることができる。
【図面の簡単な説明】
【００１０】
【図１】第１の実施の形態の情報処理装置を示す図である。
【図２】第２の実施の形態の情報処理装置のハードウェア構成を示す図である。
【図３】第２の実施の形態の情報処理装置の機能を示すブロック図である。
【図４】チェッカ読み込み部の処理を説明する図である。
【図５】データベースに格納されている情報を示す図である。
【図６】第２の実施の形態の生成部の処理を示すフローチャートである。
【図７】第２の実施の形態の第２のチェッカではカバーできないチェックパターンを説明する図である。
【図８】第３の実施の形態のチェッカ読み込み部の処理を説明する図である。
【図９】第３の実施の形態のデータベースに格納されている情報を示す図である。
【図１０】グルーピング検出処理を説明するフローチャートである。
【図１１】第３の実施の形態の生成部の処理を説明するフローチャートである。
【図１２】第３の実施の形態の処理結果を説明する図である。
【図１３】第４の実施の形態の第１のチェッカを説明する図である。
【発明を実施するための形態】
【００１１】
以下、実施の形態の情報処理装置を、図面を参照して詳細に説明する。
＜第１の実施の形態＞
図１は、第１の実施の形態の情報処理装置を示す図である。
【００１２】
第１の実施の形態の情報処理装置（コンピュータ）１は、記憶部１ａと、読み込み部１ｂと、生成部１ｃと、記憶部１ｄとを有している。記憶部１ａ、１ｄは、情報処理装置１が有するＲＡＭ（Random Access Memory）やハードディスクドライブ（ＨＤＤ:Hard Disk Drive）等が備えるデータ記憶領域により実現することができる。また、読み込み部１ｂと、生成部１ｃは、情報処理装置１が有するＣＰＵ（Central Processing Unit）が備える機能により実現することができる。
【００１３】
記憶部１ａには、設計対象の論理回路の正当性を検証する際に用いる、事前条件発生時に事後条件の発生の有無を検査する第１のチェッカ２ａが記憶されている。なお、記憶部１ａは、情報処理装置１の外部にあってもよい。第１のチェッカ２ａは、アサーション言語で記述されている。第１のチェッカ２ａには、アサーション名（assertion＿name）、同期条件（event）、アボート条件（abort）、事前条件（precond）、事前条件と事後条件の最小許容間隔（n）、事前条件と事後条件の最大許容間隔（m）、事後条件（postcond）に関する情報が記述されている。具体的には、第１のチェッカ２ａは、アサーション名が「ｃｈｋ＿ｘｘ」、同期条件が「ｐｏｓｅｄｇｅ  ｃｌｏｃｋ」、アボート条件が「Ｃ１＝＝０」、事前条件が「Ａ１＝＝１」、事前条件と事後条件の最小許容間隔が「２」、事前条件と事後条件の最大許容間隔が「４」、事後条件が「Ｂ１＝＝１」である。第１のチェッカ２ａには、「事前条件Ａ１が１になったら２〜４サイクル後に事後条件Ｂ１が１になること」を検査するアサーション名が「ｃｈｋ＿ｘｘ」のアサーション（以下、「アサーション「ｃｈｋ＿ｘｘ」」のように表記する）が記述されている。
【００１４】
読み込み部１ｂは、第１のチェッカ２ａを記憶部１ａから読み込む。
生成部１ｃは、読み込み部１ｂが読み込んだ第１のチェッカ２ａに基づき、事前条件未発生時には事後条件が発生しないことを検査する第２のチェッカ２ｂを生成する。
【００１５】
第２のチェッカ２ｂは、第１のチェッカ２ａに記述されているアサーション「ｃｈｋ＿ｘｘ」に加え、生成部１ｃにより定義されたアサーション「ｃｈｋ＿ｘｘ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」が記述されている。このアサーション「ｃｈｋ＿ｘｘ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」は、事後条件Ｂ１が１になったら２〜４サイクル前に事前条件Ａ１が１になっていたことを検査する事前条件チェッカ２ｂ１として機能する。事前条件チェッカ２ｂ１の４行目の記述については、最小許容間隔ｎの数値を１ずつインクリメントしていき、最大許容間隔ｍに到達するまで「＄ｐａｓｔ（＜ｐｒｅｃｏｎｄ＿ｅｘｐｒ＞，ｄｅｌａｙ）」の記述を論理和（ｏｒ）で繋ぐことで生成する。
【００１６】
また、生成されたアサーション「ｃｈｋ＿ｘｘ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」の１行前には、アサーション「ｃｈｋ＿ｘｘ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」が、アサーション「ｃｈｋ＿ｘｘ」に基づき生成部１ｃが生成したアサーションであることを示すコメント「／／ＣＡＧＳ  Ｉｎｆｏ：Ｇｅｎｅｒａｔｅｄ  ｆｒｏｍ  ｃｈｋ＿ｘｘ」が挿入されている。
【００１７】
生成部１ｃは、生成した第２のチェッカ２ｂを記憶部１ｄに記憶する。なお、記憶部１ｄは、情報処理装置１の外部にあってもよい。
例えば、情報処理装置１は、この第２のチェッカ２ｂを論理シミュレーションに適用し、チェッカの検出結果を基に、論理回路が仕様に違反していないか否かを確認する。第２のチェッカ２ｂを用いることで、第１のチェッカ２ａだけを用いて検査する場合には検出できなかった、事後条件Ｂ１の発生をトリガとし、この事後条件Ｂ１の発生が事前条件Ａ１の発生に起因するものであることを遡って検査することができる。これにより、設計者のミス等により意図せず事後条件Ｂ１が書き換わってしまうように論理回路の機能が実装された場合でも、エラーとして検出することができる。従って、チェッカの検出精度を高めることができる。
【００１８】
以下、第２の実施の形態において、開示の情報処理装置をより具体的に説明する。
＜第２の実施の形態＞
図２は、第２の実施の形態の情報処理装置のハードウェア構成を示す図である。
【００１９】
情報処理装置１０は、ＣＰＵ１０１によって装置全体が制御されている。ＣＰＵ１０１には、バス１０８を介してＲＡＭ１０２と複数の周辺機器が接続されている。
ＲＡＭ１０２は、情報処理装置１０の主記憶装置として使用される。ＲＡＭ１０２には、ＣＰＵ１０１に実行させるＯＳ（Operating System）のプログラムやアプリケーションプログラムの少なくとも一部が一時的に格納される。また、ＲＡＭ１０２には、ＣＰＵ１０１による処理に使用する各種データが格納される。
【００２０】
バス１０８には、ハードディスクドライブ１０３、グラフィック処理装置１０４、入力インタフェース１０５、ドライブ装置１０６、および通信インタフェース１０７が接続されている。
【００２１】
ハードディスクドライブ１０３は、内蔵したディスクに対して、磁気的にデータの書き込みおよび読み出しを行う。ハードディスクドライブ１０３は、情報処理装置１０の二次記憶装置として使用される。ハードディスクドライブ１０３には、ＯＳのプログラム、アプリケーションプログラム、および各種データが格納される。なお、二次記憶装置としては、フラッシュメモリ等の半導体記憶装置を使用することもできる。
【００２２】
グラフィック処理装置１０４には、モニタ１０４ａが接続されている。グラフィック処理装置１０４は、ＣＰＵ１０１からの命令に従って、画像をモニタ１０４ａの画面に表示させる。モニタ１０４ａとしては、ＣＲＴ（Cathode Ray Tube）を用いた表示装置や、液晶表示装置等が挙げられる。
【００２３】
入力インタフェース１０５には、キーボード１０５ａとマウス１０５ｂとが接続されている。入力インタフェース１０５は、キーボード１０５ａやマウス１０５ｂから送られてくる信号をＣＰＵ１０１に送信する。なお、マウス１０５ｂは、ポインティングデバイスの一例であり、他のポインティングデバイスを使用することもできる。他のポインティングデバイスとしては、例えばタッチパネル、タブレット、タッチパッド、トラックボール等が挙げられる。
【００２４】
ドライブ装置１０６は、例えば、光の反射によって読み取り可能なようにデータが記録された光ディスクや、ＵＳＢ（Universal Serial Bus）メモリ等の持ち運び可能な記録媒体に記録されたデータの読み取りを行う。例えば、ドライブ装置１０６が光学ドライブ装置である場合、レーザ光等を利用して、光ディスク２００に記録されたデータの読み取りを行う。光ディスク２００には、Ｂｌｕ−ｒａｙ（登録商標）、ＤＶＤ（Digital Versatile Disc）、ＤＶＤ−ＲＡＭ、ＣＤ−ＲＯＭ（Compact Disc Read Only Memory）、ＣＤ−Ｒ（Recordable）／ＲＷ（ReWritable）等が挙げられる。
【００２５】
通信インタフェース１０７は、ネットワーク５０に接続されている。通信インタフェース１０７は、ネットワーク５０を介して、他のコンピュータまたは通信機器との間でデータを送受信する。
【００２６】
以上のようなハードウェア構成によって、本実施の形態の処理機能を実現することができる。
図２に示すようなハードウェア構成の情報処理装置１０内には、以下のような機能が設けられる。
【００２７】
図３は、第２の実施の形態の情報処理装置の機能を示すブロック図である。
情報処理装置１０は、第１のチェッカ記憶部１１と、チェッカ読み込み部１２と、生成部１３と、第２のチェッカ記憶部１４と、インタフェース部１５と、ＤＢ入出力部１６とを有している。
【００２８】
第１のチェッカ記憶部１１には、設計対象の論理回路の正当性を検証するのに用いる少なくとも１つの第１のチェッカが記憶されている。以下の説明では、第１の実施の形態の第１のチェッカ２ａと同じ内容の第１のチェッカが第１のチェッカ記憶部１１に記憶されているものとして説明する。
【００２９】
チェッカ読み込み部１２は、インタフェース部１５により指定された第１のチェッカから必要な情報を取得し、チェッカデータモデル１２１へセットする。
図４は、チェッカ読み込み部の処理を説明する図である。
【００３０】
図４に示す第１のチェッカ１１１は、第１の実施の形態の第１のチェッカ２ａと同じ内容になっている。
チェッカデータモデル１２１は、第１のチェッカ１１１の各情報をメンバとした構造体になっている。
【００３１】
チェッカ読み込み部１２は、チェッカデータモデル１２１の適切なメンバに各情報を格納する。チェッカデータモデル１２１の右側に点線で示した矢印の先には、第１のチェッカ１１１を入力した場合にチェッカデータモデル１２１のメンバに格納される各情報を示している。
【００３２】
生成部１３は、このチェッカデータモデル１２１にセットされた情報を基に、事前条件チェッカ１３１ａを生成する。生成部１３は、事前条件チェッカ１３１ａを生成する際に、まず定型文を設定する。定型文は、図４に示す事前条件チェッカ１３１ａの斜体で表記した箇所以外の箇所である。そして、チェッカデータモデル１２１に格納された情報を、定型文に挿入する。挿入された情報は、図４に示す事前条件チェッカ１３１ａの斜体で表記した箇所である。ここで、事前条件チェッカ１３１ａの４行目の記述については、最小許容間隔ｎの数値を１ずつインクリメントしていき、最大許容間隔ｍに到達するまで「＄ｐａｓｔ（＜ｐｒｅｃｏｎｄ＿ｅｘｐｒ＞，ｄｅｌａｙ）」の記述を論理和（ｏｒ）で繋ぐことで生成する。また、生成部１３は、事前条件チェッカ１３１ａが情報処理装置１０によって生成されたものであることと、入力したチェッカ内のどのアサーションから生成されたものであるかを示す情報を、事前条件チェッカ１３１ａの行頭にコメント形式で記述する。
【００３３】
このようにして生成される第２のチェッカ１３１は、第１のチェッカ１１１に記述されていたアサーション「ｃｈｋ＿ｘｘ」に加え、生成部１３により定義されたアサーション「ｃｈｋ＿ｘｘ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」が記述されている。このアサーション「ｃｈｋ＿ｘｘ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」は、事後条件Ｂ１が１になったら２〜４サイクル前に事前条件Ａ１が１になっていたことを検査するアサーションである。
【００３４】
また、生成されたアサーションの１行前には、アサーション「ｃｈｋ＿ｘｘ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」が、アサーション「ｃｈｋ＿ｘｘ」に基づき情報処理装置１０が生成したアサーションであることを示すコメント「／／ＣＡＧＳ  Ｉｎｆｏ：Ｇｅｎｅｒａｔｅｄ  ｆｒｏｍ  ｃｈｋ＿ｘｘ」が挿入されている。
【００３５】
生成部１３は、生成した事前条件チェッカ１３１ａと、第１のチェッカ１１１とをまとめた第２のチェッカ１３１を第２のチェッカ記憶部１４に記憶する。
インタフェース部１５は、ユーザの入力内容に応じて情報処理装置１０を制御する。例えば、インタフェース部１５は、ユーザの入力に応じて第１のチェッカ記憶部１１に記憶されている第１のチェッカ１１１を指定する。すると前述したように、チェッカ読み込み部１２は、インタフェース部１５により指定された第１のチェッカ１１１から必要な情報を取得し、チェッカデータモデル１２１へセットする。
【００３６】
また、インタフェース部１５は、ＤＢ入出力部１６によりデータベース化された情報をモニタ１０４ａに表示することができる。ユーザがモニタ１０４ａに表示された情報を書き換えると、インタフェース部１５は、書き換えた情報をチェッカデータモデル１２１に反映する。また、インタフェース部１５は、ＤＢ入出力部１６にデータベースの更新を指示する。
【００３７】
ＤＢ入出力部１６は、チェッカデータモデル１２１にセットされる情報をデータベース化する。この情報は、インタフェース部１５によりユーザが変更しやすいフォーマットで表示され、編集可能である。この機能を使用することで、チェッカデータモデル１２１にセットされる情報をユーザが操作し、所望のチェッカを生成することができる。また逆に、ＤＢ入出力部１６は、データベース２０に格納された情報を抽出することもできる。
【００３８】
図５は、データベースに格納されている情報を示す図である。
図５に示すテーブル２０ａは、データベース２０に格納された情報を示している。
テーブル２０ａには、第１のチェッカ１１１に記述された情報を格納する各欄が設定されている。
【００３９】
次に、図４に示す生成部１３の処理を、フローチャートを用いて説明する。
図６は、第２の実施の形態の生成部の処理を示すフローチャートである。
［ステップＳ１］  生成部１３は、定型文を作成する。その後、ステップＳ２に遷移する。
【００４０】
［ステップＳ２］  生成部１３は、チェッカデータモデル１２１を参照し、ステップＳ１にて作成した定型文にアサーション名、同期条件、アボート条件、事後条件を挿入する。その後、ステップＳ３に遷移する。
【００４１】
［ステップＳ３］  生成部１３は、チェッカデータモデル１２１を参照し、用意したパラメータｋに最小許容間隔ｎをセットする。その後、ステップＳ４に遷移する。
［ステップＳ４］  生成部１３は、パラメータｋの値が、最大許容間隔ｍに一致するか否かを判断する。パラメータｋの値が、最大許容間隔ｍに一致する場合（ステップＳ４のＹｅｓ）、ステップＳ６に遷移する。パラメータｋの値が、最大許容間隔ｍに一致しない場合（ステップＳ４のＮｏ）、ステップＳ５に遷移する。
【００４２】
［ステップＳ５］  生成部１３は、「＄ｐａｓｔ（＜ｐｒｅｃｏｎｄ＿ｅｘｐｒ＞，ｄｅｌａｙ）」の記述を論理和で繋ぐ。その後、ステップＳ５ａに遷移する。
［ステップＳ５ａ］  生成部１３は、パラメータｋの値をインクリメントする。その後、ステップＳ４に遷移する。
【００４３】
［ステップＳ６］  生成部１３は、ステップＳ５にて生成した論理和の結合を定型文の後に挿入する。その後、ステップＳ７に遷移する。
［ステップＳ７］  生成部１３は、事前条件チェッカ１３１ａ生成の終了を示す「；）」を挿入する。その後、ステップＳ８に遷移する。
【００４４】
［ステップＳ８］  生成部１３は、事前条件チェッカ１３１ａに第１のチェッカ１１１を追加し、第２のチェッカ１３１を生成する。その後、ステップＳ９に遷移する。
［ステップＳ９］  生成部１３は、ステップＳ８にて生成した第２のチェッカ１３１を第２のチェッカ記憶部１４に記憶する。その後、図６の処理を終了する。
【００４５】
以上述べたように、情報処理装置１０によれば、事後条件の発生を起因として事前条件が過去に発生していたことを検査できる事前条件チェッカ１３１ａを含む第２のチェッカ１３１を生成する。この第２のチェッカ１３１を用いて論理回路の正当性を検証することで、事前条件が発生していないにもかかわらず、事後条件が発生した場合をエラーとして検出できる。このエラーをログファイルに残すことにより、ユーザは、ログファイルを確認するだけでエラーの有無（障害の有無）を判別できる。
【００４６】
従って、仕様書に記載されていないことのチェック（事前条件に因らない事後条件の発生の検出）を網羅することができ、論理障害による意図しない動作の発生や、仕様書に記載の無い条件における動作の発生（仕様書の記載漏れ）が生じてもチェッカで検出できるようになる。これにより従来よりもチェッカの網羅性が向上し、検証品質の向上に繋がる。
【００４７】
＜第３の実施の形態＞
次に、第３の実施の形態の情報処理装置について説明する。
以下、第３の実施の形態の情報処理装置について、前述した第２の実施の形態との相違点を中心に説明し、同様の事項については、その説明を省略する。
【００４８】
第２の実施の形態では、入力する第１のチェッカ１１１に１種類のアサーション「ｃｈｋ＿ｘｘ」しか存在しない場合について説明した。しかし、第１のチェッカに複数のアサーションが記述されていた場合には、第２の実施の形態の情報処理装置１０は、それぞれに対して事前条件チェッカを生成する。ここで、事後条件が同じで事前条件が異なるアサーションが第１のチェッカに記載されていると、第２の実施の形態の情報処理装置１０が生成した第２のチェッカではカバーできないチェックパターンが存在する。
【００４９】
図７は、第２の実施の形態の第２のチェッカではカバーできないチェックパターンを説明する図である。
図７に示す事前条件チェッカ１３２ａを生成する元となる第１のチェッカ１１２には、「事後条件Ｂ１が１になる条件は事前条件Ａ１または事前条件Ａ２が１になること」という仕様が記述されている。また、入力する第１のチェッカ１１２には、事前条件Ａ１が１になったら２〜４サイクル後に事後条件Ｂ１が１になることを検査するアサーション「ｃｈｋ＿ｘｘ」と、事前条件Ａ２が１になったら２〜４サイクル後に事後条件Ｂ１が１になることを検査するアサーション「ｃｈｋ＿ｙｙ」が記述されている。
【００５０】
アサーション「ｃｈｋ＿ｘｘ」とアサーション「ｃｈｋ＿ｙｙ」は共に「Ｂ１＝＝１」が事後条件に定義されている。この第１のチェッカ１１２をこのまま第２の実施の形態の情報処理装置１０に入力すると、アサーション「ｃｈｋ＿ｘｘ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」とアサーション「ｃｈｋ＿ｙｙ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」が記述された事前条件チェッカ１３２ａが生成される。
【００５１】
前述したように、第１のチェッカ１１２には、「事後条件Ｂ１が１になる条件は事前条件Ａ１または事前条件Ａ２が１になること」という仕様が記述されている。このため、事後条件（Ｂ１＝＝１）発生時、事前条件のいずれかが発生していれば、正しい動作であると、判断できればよい。しかし、この生成された事前条件チェッカ１３２ａは、事後条件発生時に、複数ある事前条件すべてが発生していない限り、エラーを通知してしまう。すなわち、検証対象が正しい動作をしているにもかかわらず、違反動作としてチェッカがエラーを検出してしまう。
【００５２】
第３の実施の形態の情報処理装置は、第２の実施の形態の第２のチェッカの生成方法ではカバーできないチェックパターンを解決する機能（グルーピング機能）を備える。
図８は、第３の実施の形態のチェッカ読み込み部の処理を説明する図である。
【００５３】
図８の第１のチェッカ記憶部１１には、図７と同様の第１のチェッカ１１２が記憶されている。第１のチェッカ１１２には、アサーション「ｃｈｋ＿ｘｘ」とアサーション「ｃｈｋ＿ｙｙ」が記述されている。
【００５４】
第３の実施の形態のチェッカ読み込み部１２は、入力されたアサーション「ｃｈｋ＿ｘｘ」とアサーション「ｃｈｋ＿ｙｙ」の事後条件を文字列比較し、先に入力されたアサーションに事後条件が等価であるものが存在した場合に、これらのアサーション「ｃｈｋ＿ｘｘ」とアサーション「ｃｈｋ＿ｙｙ」がグルーピング対象のアサーションであると判断する。
【００５５】
チェッカ読み込み部１２は、この判断結果に基づき、第１のチェッカ１１２に記述された情報をグルーピング用のチェッカデータモデル１２２に設定する。
図８に示すように、チェッカデータモデル１２２の右側に点線で示した矢印の先には、第１のチェッカ１１２を入力した場合にチェッカデータモデル１２２のメンバに格納される各情報を示している。
【００５６】
また、チェッカ読み込み部１２は、アサーション「ｃｈｋ＿ｘｘ」とアサーション「ｃｈｋ＿ｙｙ」は共に事後条件「Ｂ１＝＝１」が定義されていることから同じグループであると判断する。そして、チェッカ読み込み部１２は、事後条件の情報を変換してグループ名を生成する。具体的には、事後条件が「ｓｉｇｎａｌ＝＝ｎ」の場合、グループ属性は「Ｇｒｐ＿“ｓｉｇｎａｌ”ｅｑ“ｎ”」となり、「ｓｉｇｎａｌ！＝ｎ」の場合は「Ｇｒｐ＿“ｓｉｇｎａｌ”ｎｅ“ｎ”」となる。これを図８に示す例に当てはめると、グループ名は、「Ｇｒｐ＿Ｂ１ｅｑ１」となる。
【００５７】
生成部１３は、チェッカデータモデル１２２に基づいてチェッカ１１２ａと事前条件チェッカ１３３ａとを含む第２のチェッカ１３３を生成する。
チェッカ１１２ａは、第１のチェッカ１１２の各アサーションの前の行に、アサーション「ｃｈｋ＿ｘｘ」とアサーション「ｃｈｋ＿ｙｙ」がグルーピング対象のアサーションであると判断されたことを示すコメント「ＣＡＧＳ  Ｉｎｆｏ：Ｍｅｍｂｅｒ  ｏｆ  “Ｇｒｐ＿Ｂ１ｅｑ１”  Ｇｒｏｕｐ．」が挿入されている。このコメントは、コメントの形式が「ＣＡＧＳ  Ｉｎｆｏ：Ｍｅｍｂｅｒ  ｏｆ  ××  Ｇｒｏｕｐ．」と決まっており、生成部１３が、「××」の部分にグループ名を挿入したものである。
【００５８】
事前条件チェッカ１３３ａは、事後条件Ｂ１が１になったときに事前条件Ａ１または事前条件Ａ２のいずれかが以前に発生していたことをチェックすることができる。なお、事前条件チェッカ１３３ａの生成方法については、後述する。
【００５９】
ＤＢ入出力部１６は、チェッカデータモデル１２２に設定される情報をデータベース２０に格納する。
図９は、第３の実施の形態のデータベースに格納されている情報を示す図である。
【００６０】
図９に示すテーブル２０ｂは、データベース２０に格納された情報を示している。
テーブル２０ｂには、テーブル２０ａに加え、さらにグループ属性、および同グループアサーションの欄が設けられている。
【００６１】
グループ属性の欄には、チェッカ読み込み部１２によりグルーピングされたアサーションのグループ名が設定される。
同グループアサーションの欄には、入力されたアサーションの事後条件を文字列比較し、先に入力されたアサーションに事後条件が等価であるものが存在した場合に、そのアサーション名が設定される。
【００６２】
インタフェース部１５が、テーブル２０ｂに設定された情報をモニタ１０４ａに表示することにより、アサーション「ｃｈｋ＿ｘｘ」とアサーション「ｃｈｋ＿ｙｙ」は共にグループ名「Ｇｒｐ＿Ｂ１ｅｑ１」のグループに属していることが確認できる。この方法を使用することで、第１のチェッカ１１２にユーザが手動でグルーピングの情報を書き加えることなく（ユーザの手を煩わせることなく）グルーピング機能を有効化できる。このため、同じグループに属すべきアサーションの見逃しも防ぐことができる。
【００６３】
次に、図８に示すチェッカ読み込み部１２がグルーピング対象のアサーションを検出する処理（グルーピング検出処理）を説明する。
図１０は、グルーピング検出処理を説明するフローチャートである。
【００６４】
［ステップＳ１１］  チェッカ読み込み部１２は、第１のチェッカ１１２を取得する。その後、ステップＳ１２に遷移する。
［ステップＳ１２］  チェッカ読み込み部１２は、取得した第１のチェッカ１１２に含まれるアサーション数ｎを計算する。その後、ステップＳ１３に遷移する。
【００６５】
［ステップＳ１３］  チェッカ読み込み部１２は、パラメータｋ＝０に設定する。その後、ステップＳ１４に遷移する。
［ステップＳ１４］  チェッカ読み込み部１２は、パラメータｋがアサーション数ｎに一致するか否かを判断する。パラメータｋがアサーション数ｎに一致する場合（ステップＳ１４のＹｅｓ）、図１０の処理を終了する。パラメータｋがアサーション数ｎに一致しない場合（ステップＳ１４のＮｏ）、ステップＳ１５に遷移する。
【００６６】
［ステップＳ１５］  チェッカ読み込み部１２は、ステップＳ１１にて取得した第１のチェッカ１１２の中に事後条件が一致するアサーションが存在するか否かを判断する。事後条件が一致するアサーションが存在する場合（ステップＳ１５のＹｅｓ）、ステップＳ１６に遷移する。事後条件が一致するアサーションが存在しない場合（ステップＳ１５のＮｏ）、ステップＳ１８に遷移する。
【００６７】
［ステップＳ１６］  チェッカ読み込み部１２は、事後条件が一致するアサーションが、グルーピング対象のアサーションであると判断する。その後、ステップＳ１７に遷移する。
【００６８】
［ステップＳ１７］  チェッカ読み込み部１２は、事前条件名に基づきグルーピング対象のアサーションのグループ属性名を生成する。その後、ステップＳ１８に遷移する。
［ステップＳ１８］  チェッカ読み込み部１２は、パラメータｋをインクリメントする。その後、ステップＳ１４に遷移する。
【００６９】
次に、図８に示す生成部１３の処理を、フローチャートを用いて説明する。
図１１は、第３の実施の形態の生成部の処理を説明するフローチャートである。
［ステップＳ２１］  生成部１３は、定型文を作成する。その後、ステップＳ２２に遷移する。
【００７０】
［ステップＳ２２］  生成部１３は、チェッカデータモデル１２２を参照し、ステップＳ２１にて作成した定型文にアサーション名、同期条件、アボート条件、事後条件を挿入する。その後、ステップＳ２３に遷移する。
【００７１】
［ステップＳ２３］  生成部１３は、「ｃｈｅｃｋｅｒ＿ｇｒｏｕｐ．ｃｈｅｃｋｅｒｓ［］」の要素を１つ取り出す。その後、ステップＳ２４に遷移する。
［ステップＳ２４］  生成部１３は、チェッカデータモデル１２２を参照し、用意したパラメータｋに最小許容間隔ｎをセットする。その後、ステップＳ２５に遷移する。
【００７２】
［ステップＳ２５］  生成部１３は、パラメータｋの値が、最大許容間隔ｍに一致するか否かを判断する。パラメータｋの値が、最大許容間隔ｍに一致する場合（ステップＳ２５のＹｅｓ）、ステップＳ２７に遷移する。パラメータｋの値が、最大許容間隔ｍに一致しない場合（ステップＳ２５のＮｏ）、ステップＳ２６に遷移する。
【００７３】
［ステップＳ２６］  生成部１３は、「＄ｐａｓｔ（＜ｐｒｅｃｏｎｄ＿ｅｘｐｒ＞，ｄｅｌａｙ）」の記述を論理和で繋ぐ。その後、ステップＳ２６ａに遷移する。
［ステップＳ２６ａ］  生成部１３は、パラメータｋの値をインクリメントする。その後、ステップＳ２５に遷移する。
【００７４】
［ステップＳ２７］  生成部１３は、「ｃｈｅｃｋｅｒ＿ｇｒｏｕｐ．ｃｈｅｃｋｅｒｓ［］」に設定されている全ての要素を取り出したか否かを判断する。全ての要素を取り出した場合（ステップＳ２７のＹｅｓ）、ステップＳ２８に遷移する。全ての要素を取り出していない場合（ステップＳ２７のＮｏ）、ステップＳ２３に遷移し、ステップＳ２４〜Ｓ２６の処理を実行していない要素を取り出し、ステップＳ２４以降の処理を実行する。
【００７５】
［ステップＳ２８］  生成部１３は、ステップＳ２６にて生成した論理和の結合を定型文の後に挿入する。その後、ステップＳ２９に遷移する。
［ステップＳ２９］  生成部１３は、事前条件チェッカ１３３ａ生成の終了を示す「；）」を挿入する。その後、ステップＳ３０に遷移する。
【００７６】
［ステップＳ３０］  生成部１３は、第１のチェッカ１１２にコメントを追加したチェッカ１１２ａを事前条件チェッカ１３３ａに追加し、第２のチェッカ１３３を生成する。その後、ステップＳ３１に遷移する。
【００７７】
［ステップＳ３１］  生成部１３は、ステップＳ３０にて生成した第２のチェッカ１３３を第２のチェッカ記憶部１４に記憶する。その後、図１１の処理を終了する。
図１２は、第３の実施の形態の処理結果を説明する図である。
【００７８】
第３の実施の形態の情報処理装置１０により生成された第２のチェッカ１３３によれば、事後条件（Ｂ１==１）発生時、事前条件Ａ１、Ａ２のいずれかが発生していれば、正しい動作であると、判断することができる。これにより、同じグループに属すべきアサーションの見逃しも防ぐことができる。
【００７９】
＜第４の実施の形態＞
次に、第４の実施の形態の情報処理装置について説明する。
以下、第４の実施の形態の情報処理装置について、前述した第２の実施の形態および第３の実施の形態との相違点を中心に説明し、同様の事項については、その説明を省略する。
【００８０】
第４の実施の形態の情報処理装置１０は、チェッカデータモデル１２１にセットする情報をインタフェース部１５からの入力によって取得し、セットした情報に基づいて第２のチェッカを生成する点が異なっている。
【００８１】
本実施の形態では、第２の実施の形態、および第３の実施の形態で入力としてきた第１のチェッカのアサーション「ｃｈｋ＿ｘｘ」と、その事前条件をチェックするアサーション「ｃｈｋ＿ｘｘ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」を生成する例を挙げる。
【００８２】
ユーザは、インタフェース部１５の入力フォーマットに従い、アサーション「ｃｈｋ＿ｘｘ」を生成するための情報を入力する。その後は第２の実施の形態にて述べたのと同様に、この入力情報をデータベース２０に保存してチェッカデータモデル１２１に反映させる。
【００８３】
生成部１３は、事前条件チェッカについては第２の実施の形態と同様のアルゴリズムでアサーション「ｃｈｋ＿ｘｘ＿ｐｒｅｃｏｎｄ＿ｃｈｋ」を生成する。さらに生成部１３は、図４に示したように、斜体の箇所にチェッカデータモデル１２１の情報を埋め込む形で第１のチェッカのアサーション「ｃｈｋ＿ｘｘ」も生成してこれらをまとめた第２のチェッカを第２のチェッカ記憶部１４に記憶する。
【００８４】
ところで、ユーザは、事後条件が同じアサーションをグルーピングさせる情報を第１のチェッカに手動で入力することもできる。
事後条件が同じアサーションをグルーピングさせるためには、ユーザがキーボード１０５ａやマウス１０５ｂを用いてアサーションの前行に専用のコメントを挿入する。この形式のコメントを挿入した第１のチェッカを情報処理装置１０に入力することで、アサーション「ｃｈｋ＿ｘｘ」とアサーション「ｃｈｋ＿ｙｙ」が共に事後条件「Ｂ１＝＝１」を持つ同じグループであることをチェッカ読み込み部１２が認識する。チェッカ読み込み部１２では、同じグループであるものは事前条件チェッカを生成する際に１つのアサーションにまとめて出力される。
【００８５】
図１３は、第４の実施の形態の第１のチェッカを説明する図である。
本実施の形態の第１のチェッカ１１３のグルーピング用コメントの形式は「ＣＡＧＳ  Ｉｎｆｏ：Ｍｅｍｂｅｒ  ｏｆ  ××  Ｇｒｏｕｐ．」と決まっており、××の部分はユーザが任意に指定することができる。このとき生成されるアサーションのラベルは「××＿ｐｒｅｃｏｎｄ＿ｃｈｋ」となる。図１３に示す例では「Ｇｒｐ＿Ｂ１＿ｐｒｅｃｏｎｄ＿ｃｈｋ」として生成される。これによって、第３の実施の形態と同等の機能を備える第２のチェッカを生成することができる。
【００８６】
以上、本発明の情報処理装置、情報処理方法およびプログラムを、図示の実施の形態に基づいて説明したが、本発明はこれに限定されるものではなく、各部の構成は、同様の機能を有する任意の構成のものに置換することができる。また、本発明に、他の任意の構成物や工程が付加されていてもよい。
【００８７】
また、本発明は、前述した各実施の形態のうちの、任意の２以上の構成（特徴）を組み合わせたものであってもよい。
なお、情報処理装置１０が行った処理が、複数の装置によって分散処理されるようにしてもよい。例えば、１つの装置が、チェッカデータモデル１２１を生成しておき、他の装置が、そのチェッカデータモデル１２１を用いて第２のチェッカ１３１を生成するようにしてもよい。
【００８８】
なお、上記の処理機能は、コンピュータによって実現することができる。その場合、情報処理装置１、１０が有する機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータで実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体に記録しておくことができる。コンピュータで読み取り可能な記録媒体としては、磁気記憶装置、光ディスク、光磁気記録媒体、半導体メモリ等が挙げられる。磁気記憶装置には、ハードディスクドライブ、フレキシブルディスク（ＦＤ）、磁気テープ等が挙げられる。光ディスクには、ＤＶＤ、ＤＶＤ−ＲＡＭ、ＣＤ−ＲＯＭ／ＲＷ等が挙げられる。光磁気記録媒体には、ＭＯ（Magneto-Optical disk）等が挙げられる。
【００８９】
プログラムを流通させる場合には、例えば、そのプログラムが記録されたＤＶＤ、ＣＤ−ＲＯＭ等の可搬型記録媒体が販売される。また、プログラムをサーバコンピュータの記憶装置に格納しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。
【００９０】
プログラムを実行するコンピュータは、例えば、可搬型記録媒体に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶装置に格納する。そして、コンピュータは、自己の記憶装置からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、可搬型記録媒体から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、ネットワークを介して接続されたサーバコンピュータからプログラムが転送される毎に、逐次、受け取ったプログラムに従った処理を実行することもできる。
【００９１】
また、上記の処理機能の少なくとも一部を、ＤＳＰ（Digital Signal Processor）、ＡＳＩＣ（Application Specific Integrated Circuit）、ＰＬＤ（Programmable Logic Device）等の電子回路で実現することもできる。
【符号の説明】
【００９２】
１、１０  情報処理装置
１ａ、１ｄ  記憶部
１ｂ  読み込み部
１ｃ、１３  生成部
２ａ、１１１、１１２、１１３  第１のチェッカ
２ｂ、１３１、１３３  第２のチェッカ
２ｂ１、１３１ａ、１３２ａ、１３３ａ  事前条件チェッカ
１１  第１のチェッカ記憶部
１２  チェッカ読み込み部
１２１、１２２  チェッカデータモデル
１４  第２のチェッカ記憶部
１５  インタフェース部
１６  ＤＢ入出力部
２０  データベース
２０ａ、２０ｂ  テーブル
【図１】
2013200745.tif 000003
【図２】
2013200745.tif 000004
【図３】
2013200745.tif 000005
【図４】
2013200745.tif 000006
【図５】
2013200745.tif 000007
【図６】
2013200745.tif 000008
【図７】
2013200745.tif 000009
【図８】
2013200745.tif 000010
【図９】
2013200745.tif 000011
【図１０】
2013200745.tif 000012
【図１１】
2013200745.tif 000013
【図１２】
2013200745.tif 000014
【図１３】
2013200745.tif 000015