(57)【要約】      （修正有）【課題】並行処理を行う検証対象プログラムを効率よく検証することができるようにする。【解決手段】検証対象プログラム記憶部２１２に格納された検証対象プログラムとリファレンスプログラム記憶部２１１に格納されたリファレンスプログラムには、ユーザがそれぞれ同期点を設定している。処理部２００は、リファレンスプログラムと、検証対象プログラムの同期点にそれぞれ同期コマンドを挿入する。次に処理部２００は、同期コマンドを挿入したリファレンスプログラムおよび検証対象プログラムと、アサーション記憶部２１３へ格納された、同期点でのアサーションを基にして生成された比較プログラム、入力データ供給プログラム記憶部２１６に格納されている入力データ供給プログラムとをひとつの並行プログラムとして、拡大プログラムを生成する。処理部２００は、生成した拡大プログラムについてアサーションチェックとデッドロック検出を行って検証する。【選択図】図２
2010165121.tif 000002
【特許請求の範囲】
【請求項１】
リファレンスプログラムを用いて検証対象プログラムの検証を行うためのプログラムであって、前記検証対象プログラムが、前記リファレンスプログラムから生成されたプログラムであり、
コンピュータに、
前記リファレンスプログラムおよび前記検証対象プログラムに設定された任意の同期点と、前記同期点に関するアサーションとを元に、比較プログラムを生成する手順と、
生成した前記比較プログラム、前記リファレンスプログラム、前記検証対象プログラムとを含む拡大プログラムを生成する手順と
を実行させるためのプログラム。
【請求項２】
前記比較プログラムが、前記リファレンスプログラムおよび前記検証対象プログラムの入出力に関するアサーションをさらに含む
ことを特徴とする請求項１記載のプログラム。
【請求項３】
前記拡大プログラムが、入力データ供給プログラムをさらに含む
ことを特徴とする請求項１記載のプログラム。
【請求項４】
前記入力データ供給プログラムが、前記リファレンスプログラムおよび前記検証対象プログラムに同じデータを入力データとしてそれぞれ入力し、
前記比較プログラムは、前記リファレンスプログラムおよび前記検証対象プログラムから出力される前記同期点に関するアサーションの真偽判定によって前記検証対象プログラムの検証を行う
ことを特徴とする請求項１に記載のプログラム。
【請求項５】
リファレンスプログラムを用いて検証対象プログラムの検証を行うためのプログラムであって、前記検証対象プログラムが、前記リファレンスプログラムから生成されたプログラムであり、
コンピュータに、
前記リファレンスプログラムおよび前記検証対象プログラムに設定された同期点と、前記同期点に関するアサーションとを元に、比較プログラムを生成する手順と、
生成した前記比較プログラム、前記リファレンスプログラム、前記検証対象プログラムとを含む拡大プログラムを生成する手順と
を実行させるためのプログラムを記録したコンピュータ読み取り可能な記録媒体。
【請求項６】
リファレンスプログラムを用いて検証対象プログラムの検証を行うプログラム検証方法であって、前記検証対象プログラムが、前記リファレンスプログラムから生成されたプログラムであり、
前記リファレンスプログラムおよび前記検証対象プログラムに設定された任意の同期点と、前記同期点に関するアサーションとを元に、比較プログラムを生成するステップと、
生成した前記比較プログラム、前記リファレンスプログラム、前記検証対象プログラムとを含む拡大プログラムを生成するステップと、
前記拡大プログラムの動作検証を行うステップと
を特徴とするプログラム検証方法。
【請求項７】
前記拡大プログラムの動作検証が、アサーションチェックとデッドロック検出である
ことを特徴とする請求項６記載のプログラム検証方法。
【請求項８】
前記アサーションチェックが形式的検証を含み、
前記拡大プログラムを、前記形式的検証が可能な言語に変換する
ことを特徴とする請求項６記載のプログラム検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、並行処理を行うプログラムを検証するためのプログラム及びプログラム検証方法に関する。
【背景技術】
【０００２】
プログラムの検証とは、実装されたプログラムが正しく動作するかを、仕様を根拠として示す作業であり、具体的にはテストや形式的検証などを実施することである。テストとは実際にプログラムを実行して動作確認することである。形式的検証とは論理式に対する記号的な操作によって正当性を証明する方法である。
【０００３】
ある並行処理を行うプログラムにおいて、起こり得る主なエラーとして、レース状態とデッドロックが考えられる。レース状態とは、複数のプロセスの実行順序によって計算結果が異なることをいう。デッドロックとは、共有リソースを複数のプロセスが取り合い、互いに他のプロセスによるリソースの解放を待ちつづけて、処理の進行が止まってしまうことである。
【０００４】
並行処理を行うプログラム（以後、検証対象プログラムと呼ぶ）を検証する際、リファレンスプログラムを用い、検証対象プログラムとリファレンスプログラムとを並行化する（並行プログラムに書き換える）という手順をとることがある。リファレンスプログラムとは、実装する検証対象プログラムの見本となるプログラムである。
【０００５】
しかし、一般に検証対象プログラムの検証は難しい。テストによってプログラムの不具合が発見できても、非決定性のために現象が再現できないことが多く、原因究明を難しくしている。モデル検査などの形式的検証を使えば、あらゆるスケジューリングの可能性を網羅した検証が可能であるが、適用可能なプログラムの規模には限界があり、実装するプログラムの検証には困難が伴う。
【０００６】
また、プログラムを検証するための仕様の一種としてアサーションが用いられる。アサーションとは、プログラム実行中に成立する条件や、あるいはそのような条件の間の関係を表すための論理式である。条件の種類としては、事前条件、事後条件、ループ不変条件などがある。テストにおいてアサーションは、プログラムの実行中にアサーションの条件をチェックすることによって、動作確認に用いることができる。形式的検証においてアサーションは、プログラムの正当性の証明のために用いることができる。
【０００７】
プログラムの検証に関して、並行プログラムのためのデバッガについての技術が知られている。このデバッガでは、複数のプロセスにそれぞれ設定したブレークポイントをまとめてcollective breakpointとして扱う。また、時相論理で記述されたアサーションが与えられたときに、そこからデバッグ対象のプログラムの動作を監視するためのプログラムを生成してデバッグに用いる方法を示している。しかし、リファレンスプログラムと検証対象プログラムの動作を対比する方法を論じたものではない。また、ブレークポイントとアサーションの間の関連づけはされていない（例えば、非特許文献１参照）。
【先行技術文献】
【非特許文献】
【０００８】
【非特許文献１】Kovacs, J., Kusper, G., Lovas, R., and Schreiner, W., “Integrating Temporal Assertions into a Parallel Debugger”, Proceedings of the 8th international Euro-Par Conference on Parallel Processing, August 27-30, 2002
【発明の概要】
【発明が解決しようとする課題】
【０００９】
最終的に実装するのは検証対象プログラムだけであるから、リファレンスプログラムと検証対象プログラムは、それぞれ独立して動作するプログラムである。順序としてはリファレンスプログラムを参考にして検証対象プログラムを作成することになるが、その際にプロセスの数を追加したり、同期や通信を扱う命令を追加したりするなどの変更が行われる。あるいは、計算機のハードウェア構成にあわせて計算手順や演算命令の変更も行う可能性がある。たとえばリファレンスプログラムにはないSIMD演算命令を検証対象プログラムでは利用することもある。
【００１０】
このような変更を加えられた結果、検証対象プログラムとリファレンスプログラムとの関係は分かりにくくなる。その関係は、その作業を行った設計者は内容を理解しているが、ソースコードだけからツールが自動的に関係を抽出することは困難である。検証のためには、関連性を自動的には判別しにくい二つのプログラム（検証対象プログラムとリファレンスプログラム）を比較しなければならない。そのため、テスト結果を解析する作業が、一般のプログラムよりも困難になりやすい。また、複数プロセスの実行順序やログ出力が入り組んでしまい、不具合の兆候を見逃しやすい。更に、不具合の再現性がなく、原因追求が困難になってしまう。
【００１１】
形式的検証を用いて大規模な検証を行う場合、アサーションを使ったモジュラー検証という方法がある。これは、検証対象を複数の部分（モジュール）に分割して、モジュールをそれぞれ個別に検証し、その結果を組み合わせて全体の正しさを判定するという方法である。これを行うためには、モジュールごとに、動作の前提となる条件と、動作結果が満たすべき条件を記述しなければならない。その条件の記述がアサーションである。
【００１２】
単一の逐次プログラムの場合は、手続きやループなどといった構文要素と処理の過程が一致しているため、構文要素ごとにアサーションを記述してモジュラー検証することが可能であった。しかし、リファレンスプログラムと検証対象プログラムは独立したプログラムであるため、処理の過程と構文要素が一致しておらず、モジュール分割に伴う形でアサーションを記述することはできない。そのため、モジュラー検証も適用できないことになる。
【００１３】
他にも効率向上のために抽象化という方法がある。抽象化とは、複数の状態をまとめて1個の状態とみなし、検証対象の状態数を減らすことによって、検証に必要なメモリや時間を減少させる方法である。ところが、検証対象プログラムとリファレンスプログラムをそれぞれ個別に抽象化しようとしても、両者の出力が一致しない場合に指摘する必要があるため、抽象化後のモデルも詳細度を保つ必要がある。たとえば出力が0から65535 までの整数値をとりうる場合、抽象化したモデルにおいても0から65535 までの出力を区別しないと、出力の不一致を指摘できない。つまり、抽象化しても出力を再現しなくてはならない。そのためには抽象化前のプログラムの計算過程を抽象化後もほとんど同じようになぞる必要があるので、抽象度を上げる余地があまりないことになる。
【００１４】
本発明はこのような事情を考慮してなされたもので、並行処理を行う検証対象プログラムを効率よく検証することができるプログラムおよびプログラム検証方法を提供することを目的とする。
【課題を解決するための手段】
【００１５】
上記した目的を達成するために、請求項１記載のプログラムは、リファレンスプログラムを用いて検証対象プログラムの検証を行うためのプログラムであって、前記検証対象プログラムが、前記リファレンスプログラムから生成されたプログラムであり、コンピュータに、前記リファレンスプログラムおよび前記検証対象プログラムに設定された同期点と、前記同期点に関するアサーションとを元に、比較プログラムを生成する手順と、生成した前記比較プログラム、前記リファレンスプログラム、前記検証対象プログラムとを含む拡大プログラムを生成する手順とを実行させる。
【００１６】
請求項２記載の発明は、請求項１記載のプログラムにおいて、前記比較プログラムが、前記リファレンスプログラムおよび前記検証対象プログラムの入出力に関するアサーションをさらに含むことを特徴とする。
【００１７】
請求項３記載の発明は、請求項１記載のプログラムにおいて、前記拡大プログラムが、入力データ供給プログラムをさらに含むことを特徴とする。
【００１８】
請求項４記載の発明は、請求項１記載のプログラムにおいて、前記入力データ供給プログラムが、前記リファレンスプログラムおよび前記検証対象プログラムに同じデータを入力データとしてそれぞれ入力し、前記比較プログラムは、前記リファレンスプログラムおよび前記検証対象プログラムから出力される前記同期点に関するアサーションの真偽判定によって前記検証対象プログラムの検証を行うことを特徴とする。
【００１９】
請求項５記載のコンピュータ読み取り可能な記録媒体は、リファレンスプログラムを用いて検証対象プログラムの検証を行うためのプログラムであって、前記検証対象プログラムが、前記リファレンスプログラムから生成されたプログラムであり、コンピュータに、前記リファレンスプログラムおよび前記検証対象プログラムに設定された同期点と、前記同期点に関するアサーションとを元に、比較プログラムを生成する手順と、生成した前記比較プログラム、前記リファレンスプログラム、前記検証対象プログラムとを含む拡大プログラムを生成する手順とを実行させるためのプログラムを記録する。
【００２０】
請求項６記載のプログラム検証方法は、リファレンスプログラムを用いて検証対象プログラムの検証を行うプログラム検証方法であって、前記検証対象プログラムが、前記リファレンスプログラムから生成されたプログラムであり、前記リファレンスプログラムおよび前記検証対象プログラムに設定された同期点と、前記同期点に関するアサーションとを元に、比較プログラムを生成するステップと、生成した前記比較プログラム、前記リファレンスプログラム、前記検証対象プログラムとを含む拡大プログラムを生成するステップと、前記拡大プログラムの動作検証を行うステップとを特徴とする。
【００２１】
請求項７記載の発明は、請求項６記載のプログラム検証方法において、前記拡大プログラムの動作検証が、アサーションチェックとデッドロック検出であることを特徴とする。
【００２２】
請求項８記載の発明は、請求項６記載のプログラム検証方法において、前記アサーションチェックが形式的検証を含み、前記拡大プログラムを、前記形式的検証が可能な言語に変換することを特徴とする。
【発明の効果】
【００２３】
本発明に係るプログラムによれば、同期点に関するアサーションを元に比較プログラムを生成し、リファレンスプログラム、検証対象プログラム、比較プログラムとを含む拡大プログラムを生成する。よって、同期点に関するアサーションが比較プログラムに記述されているため、リファレンスプログラムおよび検証対象プログラムの途中結果を確認することができ、リファレンスプログラムと検証対象プログラムのみを並行プログラムとして検証対象プログラムの検証をさせた場合よりも、検証結果の解析がしやすくなる。その結果、検証対象プログラムの検証時間を短縮することができる。また、同期によって不必要な状態遷移を制限できるのと同時に、アサーションによって問題を分割できるので、検証に要する時間とメモリ量を減らすことができる。
【００２４】
請求項２記載の本発明によれば、リファレンスプログラムおよび検証対象プログラムの入出力に関するアサーションが比較プログラムに記述されているため、リファレンスプログラムおよび検証対象プログラムの入出力関係を確認することができ、結果、検証対象プログラムの検証時間を短縮することができる。
【００２５】
請求項３記載の本発明によれば、拡大プログラムが入力データ供給プログラムを含むため、実際の入力データを用いることによるプログラムの検証を行うことができる。
【００２６】
請求項４記載の本発明によれば、入力データ供給プログラムがデータを入力するため、より実際の入力データに即したプログラムの検証を行うことができる。
【００２７】
請求項５記載のコンピュータ読み取り可能な記録媒体によれば、同期点に関するアサーションを元に比較プログラムを生成し、リファレンスプログラム、検証対象プログラム、比較プログラムとを含む拡大プログラムを生成する。よって、同期点に関するアサーションが比較プログラムに記述されているため、リファレンスプログラムおよび検証対象プログラムの途中結果を確認することができ、リファレンスプログラムと検証対象プログラムのみを並行プログラムとして検証対象プログラムの検証をさせた場合よりも、検証結果の解析がしやすくなる。その結果、検証対象プログラムの検証時間を短縮することができる。また、同期によって不必要な状態遷移を制限できるのと同時に、アサーションによって問題を分割できるので、検証に要する時間とメモリ量を減らすことができる。
【００２８】
請求項６記載のプログラム検証方法によれば、同期点に関するアサーションを元に比較プログラムを生成し、リファレンスプログラム、検証対象プログラム、比較プログラムとを含む拡大プログラムを生成し、拡大プログラムの動作検証を行う。よって、同期点に関するアサーションが比較プログラムに記述されているため、リファレンスプログラムおよび検証対象プログラムの途中結果を確認することができ、リファレンスプログラムと検証対象プログラムのみを並行プログラムとして検証対象プログラムの検証をさせた場合よりも、検証結果の解析がしやすくなる。その結果、検証対象プログラムの検証時間を短縮することができる。また、同期によって不必要な状態遷移を制限できるのと同時に、アサーションによって問題を分割できるので、検証に要する時間とメモリ量を減らすことができる。
【００２９】
請求項７記載のプログラム検証方法によれば、アサーションチェックとデッドロック検出を行うことにより、拡大プログラムの検証を効果的に行うことができる。
【００３０】
請求項８記載のプログラム検証方法によれば、アサーションチェックが形式的検証を含み、拡大プログラムを形式的検証が可能な言語に変換するため、入力データを必要とせずにプログラムの検証を行うことができる。
【図面の簡単な説明】
【００３１】
【図１】本発明の一実施形態に係るプログラムを適用した、検証対象プログラムとリファレンスプログラムとの等価性検証を行うためのプログラム構造を示すブロック図。
【図２】同上の実施形態における汎用計算機内の機能ブロック図。
【図３】同上の実施形態における拡大プログラムを生成するまでの動作を示すフローチャート。
【図４】(Ａ)同上の実施形態におけるリファレンスプログラムのブロックチャートを示す図である。(Ｂ)同上の実施形態におけるリファレンスプログラム。
【図５】(Ａ)同上の実施形態における検証対象プログラムのブロックチャートを示す図である。(Ｂ)同上の実施形態における検証対象プログラム。
【図６】(Ａ)同上の実施形態におけるアサーション、(Ｂ)同上の実施形態における拡大プログラム中の各プログラムにおける変数の入出力関係を示す図。
【図７】同上の実施形態における比較プログラム。
【図８】同上の実施形態における拡大プログラム生成の詳細についての動作を示すフローチャート。
【図９】同上の実施形態における拡大プログラム。
【図１０】同上の実施形態における入力データ供給プログラム。
【図１１】同上の実施形態における、拡大プログラムの検証についての動作を示すフローチャート。
【図１２】同上の実施形態におけるNuSMVを用いたアサーションチェックのプログラム。
【発明を実施するための形態】
【００３２】
以下、本発明の実施形態を添付図面に基づいて説明する。
【００３３】
図１は、本発明の一実施形態に係るプログラムを適用した、検証対象プログラムとリファレンスプログラムとの等価性検証を行うためのプログラム（以下、このプログラムを拡大プログラム１０４という）の構造を示すブロック図である。
【００３４】
拡大プログラム１０４は、検証対象プログラム１００、リファレンスプログラム１０１、入力データ供給プログラム１０２、及び比較プログラム１０３を有している。
【００３５】
検証対象プログラム１００は、リファレンスプログラム１０１を見本として生成された並行プログラムであり、検証後に製品として出荷されるプログラムである。検証対象プログラム１００とリファレンスプログラム１０１はいずれも入力データ供給プログラム１０２からデータが入力され、両者の出力は比較プログラム１０３に送られる。
【００３６】
入力データ供給プログラム１０２と比較プログラム１０３は、別個の並行プログラムであってもよく、または検証対象プログラム１００やリファレンスプログラム１０１に後から埋め込んだプログラムの断片であってもよい。入力データ供給プログラム１０２と比較プログラム１０３は、必要に応じて直接データのやり取りを行ってもよい。
【００３７】
図２は、本発明の一実施形態に係るプログラム検証方法を実施する計算機の機能構成例を示すブロック図である。
【００３８】
記憶部２４０は、処理部２００などのワーク領域となるもので、その機能はＲＡＭなどにより実現できる。
【００３９】
情報記憶媒体２１０（コンピュータにより読み取り可能な媒体）は、プログラムやデータなどを格納するものであり、その機能は、光ディスク（ＣＤ、ＤＶＤ）、光磁気ディスク（ＭＯ）、磁気ディスク、ハードディスク、磁気テープ、或いはメモリ（ＲＯＭ）などにより実現できる。また、情報記憶媒体２１０は、リファレンスプログラム記憶部２１１、検証対象プログラム記憶部２１２、アサーション記憶部２１３、比較プログラム記憶部２１４、拡大プログラム記憶部２１５、入力データ供給プログラム記憶部２１６を含む。また情報記憶媒体２１０には、本実施形態の各部としてコンピュータを機能させるためのプログラム（各部の処理をコンピュータに実行させるためのプログラム）が記憶されている。
【００４０】
処理部２００は、情報記憶媒体２１０に格納されているプログラム（データ）に基づいて本実施形態の種々の処理を行う。また、処理部２００は記憶部２４０内の主記憶部２４１をワーク領域として各種処理を行う。処理部２００の機能は各種プロセッサ（ＣＰＵ、ＤＳＰ等）、ＡＳＩＣ（ゲートアレイ等）などのハードウェアや、プログラムにより実現できる。
【００４１】
検証部２２０は情報記憶媒体２１０に含まれており、情報記憶媒体２１０に格納されているプログラムの検証を行う。検証部２２０は、レース状態検出部２２１、デッドロック検出部２２２、アサーションチェック部２２３を含む。検証部２２０は、既存のツールであってもよいし、検証するプログラム内に挿入されるプログラムであってもよい。
【００４２】
なお、検証対象プログラム記憶部２１２に記憶されている検証対象プログラム１００に対しては、レース状態検出部２２１にてあらかじめレース状態が発生しているか否かのチェックを行い、レース状態が発生しないことが事前に確認されているものとする。入力部２３０は、ユーザがデータやプログラム等を入力するインターフェースであり、その機能はキーボード、マウス、コントローラ等により実現できる。出力部２５０は、検証部２２０で得られた検証結果を出力する。
【００４３】
以下の説明では、Java（登録商標）言語によるプログラムの例を用いて本発明の実施例を示す。提示するJava（登録商標）言語のコードは、サン・マイクロシステムズ社のJava（登録商標） SE開発キット6（Java SEDevelopment Kit 6、JDK6とも呼ばれる）を使ってコンパイルと実行が可能であり、図２に示す計算機もこのJDK6を搭載したものである。
【実施例】
【００４４】
＜同期的アサーションをもつ拡大プログラム生成の概要＞
次に、同期的アサーションをもつ拡大プログラム生成の概要について図３のフローチャートを参照して説明する。
【００４５】
まずユーザは、入力部２３０からリファレンスプログラム１０１を入力する。入力されたリファレンスプログラム１０１は、情報記憶媒体２１０内のリファレンスプログラム記憶部２１１へ格納される（ステップＳ３０１）。次にユーザは、入力部２３０から検証対象プログラム１００を入力する。検証対象プログラム１００は、情報記憶媒体２１０内の検証対象プログラム記憶部２１２へ格納される（ステップＳ３０３）。
【００４６】
図４に本実施形態におけるリファレンスプログラム１０１のブロックチャート（図４(Ａ)）とプログラム（図４(Ｂ))（プロセスspec）、図５に検証対象プログラム１００のブロックチャート（図５(Ａ)）とプログラム（図５(Ｂ)) (プロセスproc0,proc1)を示す。
【００４７】
図４(Ｂ)のリファレンスプログラム１０１は、sxからデータを受信し、演算を行って、syに送信するという動作を無限ループで繰り返す。なお、/* sync c0: d0 */というコメントは設計者が指定した同期点c0であり、後でこの行に同期コマンドを挿入する。また、図５(Ｂ)の検証対象プログラム１００において、プロセスproc0はixからデータを受信し、i0とi1を使ってプロセスproc1にデータを送信するということを無限ループで繰り返す。i1には、i0に送信した整数値を３倍したものを同時に送信している。一方、プロセスproc1はi0とi1からデータを受信し、演算を行ってiyへデータを送信するという動作を無限ループで繰り返す。なお、プロセスproc1にある/* sync c1: d1 */というコメントも設計者が設定した同期点c1であり、後でこの行に同期コマンドを挿入する。
【００４８】
次にユーザは、同期点c0,c1について、関係式（条件式）を設定して入力部２３０より入力する（ステップＳ３０５）。これを同期的アサーションと呼ぶこととする。また、出力syおよびiyについての関係式（アサーション）も設定して入力する。
【００４９】
図６(Ａ)に本実施形態におけるアサーションを示す。（１）式が同期的アサーション、（２）式、（３）式がそれぞれsyおよびiyについてのアサーションである。図６(Ｂ)は、（１）式−（３）式に現れる変数と、拡大プログラム１０４中の各プログラムにおけるこれらの変数の入出力関係を示す図である。これら（１）〜（３）式のアサーションは、アサーション記憶部２１３へ格納される。
【００５０】
ステップＳ３０５でアサーション記憶部２１３にアサーションが格納されると、処理部２００はこのアサーションを基にした比較プログラムを生成して、比較プログラム記憶部２１４に格納する（ステップＳ３０７）。図７に本実施形態における比較プログラムを示す。
【００５１】
次に処理部２００は、拡大プログラムを生成する(ステップＳ３０９)。この動作の詳細について、図８のフローチャートを用いて説明する。
【００５２】
＜拡大プログラム生成の詳細＞
処理部２００は、図３のステップＳ３０１でリファレンスプログラム記憶部２１１に格納されたリファレンスプログラム１０１から、/* sync c0: d0*/のコメントで定義されている同期点を検出して、このコメント行をc0.send(d0);という同期コマンドに置き換える（ステップＳ４０１）。c0はプロセスspecの実行中にその同期点を制御が通過する時点でのd0の値を表す。
【００５３】
次に処理部２００は、図３のステップＳ３０３で検証対象プログラム記憶部２１２に格納された検証対象プログラム１００から、/* sync c1: d1*/のコメントで定義されている同期点を検出して、このコメント行をc1.send(d1);という同期コマンドに置き換える（ステップＳ４０３）。c1はプロセスproc1においてその同期点を制御が通過する時点におけるd1の値を表している。
【００５４】
次に処理部２００は、ステップＳ４０１およびＳ４０３でそれぞれ同期コマンドを挿入したリファレンスプログラム１０１、検証対象プログラム１００、および図３のステップＳ３０７で生成した比較プログラム１０３、入力データ供給プログラム記憶部２１６に格納されている入力データ供給プログラム１０４を、あらかじめ拡大プログラム記憶部２１５に格納されている、枠組みのみの拡大プログラムの該当する位置にそれぞれ挿入する（ステップＳ４０５）。図９に枠組みのみの拡大プログラムの例を示す。例えば、枠組みのみの拡大プログラムには、/* リファレンスプログラム定義部 */、/* 検証対象プログラム定義部 */、或いは、/*入力データ供給プログラム定義部 */等のコメント行が当初設けられている。これらのコメント行に実際のプログラムを挿入していく。例えば、拡大プログラムにある/* リファレンスプログラム定義部 */のコメント行に、同期コマンドを含んだリファレンスプログラムを挿入し、/* 検証対象プログラム定義部 */のコメント行に、同期コマンドを含んだ検証対象プログラムを挿入する。この他、/*入力データ供給プログラム定義部 */のコメント行に、図１０に例示する入力データ供給プログラム１０３を挿入する。図１０における入力データはランダムデータである。
【００５５】
このように、挿入した各プログラム全体をひとつの並行プログラムとして、拡大プログラム１０４を生成する。最終的に得られた拡大プログラム１０４は、拡大プログラム記憶部２０７に格納される（ステップＳ４０７）。
【００５６】
本実施形態では、同期コマンドをリファレンスプログラム１０１と検証対象プログラム１００のそれぞれ１箇所ずつ挿入したが、同期コマンドは、アサーションを構築可能であればいくつでも設定してよい。
【００５７】
また本実施形態では、拡大プログラムを並行プログラムとして処理を行うが、拡大プログラムを逐次プログラムに変換して処理を行ってもよい。
【００５８】
＜拡大プログラムの検証＞
次に、ステップＳ４０７で作成された拡大プログラム１０４の検証について、図１１に示す。処理部２００は、拡大プログラム記憶部２１５に記憶した拡大プログラム１０４を、検証部２２０内のアサーションチェック部２２３に送り、アサーションチェック部２２３はアサーションが成立するか否かのチェックを行う(ステップＳ５０１)。具体的には、拡大プログラム１０４のテストを行う。拡大プログラム１０４内の入力データ供給プログラム１０２にデータを入力し、拡大プログラム１０４をコンパイルして、比較プログラム１０３に記載されている、c0,c1,cx,sy,iyについてのアサーション（図６Ａの(1)、(2)、(3)式）がすべて成立するか否かをチェックする。アサーションがどれかひとつでも成立しない場合（ステップＳ５０１で「No」）、アサーションチェック部２２３は出力部２５０にエラーを出力する（ステップＳ５０５）。
【００５９】
次に、処理部２００は、拡大プログラム１０４を、検証部２２０内のデッドロック検出部２２２に送り、デッドロック検出部２２２はデッドロックが検出されるか否かのチェックを行う(ステップＳ５０３)。これは、検証対象プログラム１００とリファレンスプログラム１０１は、同期コマンドを挿入する前はそれぞれのプログラムでデッドロックが検出されなかったとしても、同期コマンドを挿入したために、挿入位置によってデッドロックが検出される可能性があるからである。具体的には、拡大プログラム１０４のテストを行う。拡大プログラム１０４をコンパイルし、デッドロックが検出されるか否かをチェックする。デッドロックが検出される場合（ステップＳ５０３で「No」）、デッドロック検出部２２２は出力部２５０にエラーを出力する（ステップＳ５０５）。
【００６０】
＜アサーションチェックの他の例＞
ステップＳ５０１におけるアサーションチェックは、形式的検証で行うことも可能である。図１２に、既存のモデル検査ツールであるNuSMVを用いたアサーションチェックのプログラムを示す。この検証方法は、拡大プログラム１０４をNuSMVの入力言語に変換した上で、図１２のプログラムを実行させる。この検証方法では、プログラム自体の論理性をチェックすることが可能であり、検証のためにわざわざデータを入力してコンパイルする必要がない。
【００６１】
なお図１２では、整数を12ビットとした場合について示している。Java言語ではint型が32ビットであるが、整数を32ビットとして扱うと処理時間が数時間程度かかってしまうため、本実施例ではビット数を減らして検証を行った。ビット数は変更可能である。
【００６２】
＜実行結果＞
本実施例の効果を測定するため、図６Ａで設定した(1)、(2)、(3)式のアサーションをNuSMVに入力したものと、リファレンスプログラムの出力syと検証対象プログラムの出力iyの関係であるAG(sy==iy)のアサーションのみ（同期的アサーションが無い)NuSMVに入力したものとについて、それぞれアサーションチェックを実行し、実行時間を計測した。動作環境は、1ギガバイトのメインメモリを持ち、インテル社のPentium（登録商標） Mプロセッサを1.5GHzで駆動する計算機において、オペレーティングシステムとしてマイクロソフト社のWindowsXP（登録商標） SP2を用いて、その上でNuSMVのバージョン2.4.3を動かした。このNuSMVはSATソルバとしてMiniSatがリンクされており、ZCHAFFはリンクされていない。
【００６３】
この実験の結果、同期的アサーションを含む３つのアサーションを入力したものの実行時間は49秒であった。一方、同期的アサーションがない、ひとつのアサーションのみでの実行時間は72秒であった。出力が一致することを言うためだけであれば、AG(sy==iy)が成立することを証明すれば十分であるが、それを本実施例ではわざわざ３個の論理式に分割したことになる。ところが、確認すべき項目が1個から3個に増えているにもかかわらず、NuSMVの実行時間は逆に72秒から49秒に減っている。これは、同期的アサーションによって1個の論理式が3個に分割され、証明すべき問題の規模が小さくなったことによる効果である。すなわち、本実施例の効果として、モデル検査にかかる時間を短縮できることが示された。
【００６４】
以上、本発明の実施形態について図面を参照して詳述してきたが、具体的な構成はこの実施形態に限られるものではなく、本発明の要旨を逸脱しない範囲の設計変更等も含まれる。
【符号の説明】
【００６５】
１００  検証対象プログラム
１０１  リファレンスプログラム
１０２  入力データ供給プログラム
１０３  比較プログラム
１０４  拡大プログラム
２００  処理部
２１０  情報記憶媒体
２１１  リファレンスプログラム記憶部
２１２  検証対象プログラム記憶部
２１３  アサーション記憶部
２１４  比較プログラム記憶部
２１５  拡大プログラム記憶部
２１６  入力データ供給プログラム記憶部
２２０  検証部
２２１  レース状態検出部
２２２  デッドロック検出部
２２３  アサーションチェック部
２３０  入力部
２４０  記憶部
２４１  主記憶部
２５０  出力部
【図１】
2010165121.tif 000003
【図２】
2010165121.tif 000004
【図３】
2010165121.tif 000005
【図４】
2010165121.tif 000006
【図５】
2010165121.tif 000007
【図６】
2010165121.tif 000008
【図７】
2010165121.tif 000009
【図８】
2010165121.tif 000010
【図９】
2010165121.tif 000011
【図１０】
2010165121.tif 000012
【図１１】
2010165121.tif 000013
【図１２】
2010165121.tif 000014