(57)【要約】【課題】プログラムと表明を入力としモデル検査技術を用いたプログラムの検証において、検査対象プログラムの動作コンテキストを与える仮定の誤りの可能性を示すことを可能にする。【解決手段】条件分岐箇所へ到達確認用のコードを埋め込む等の既存技術を用いてモデル検査技術で検証した範囲を網羅度として測定し、検証結果とともにその測定結果を示すことにより、作業者に仮定の誤りの可能性を示す。網羅度が１００％未満の場合（＝未検査の分岐が存在する場合）には、仮定に誤りがある可能性があると判断する。【選択図】図２
2010072883.tif 000002
【特許請求の範囲】
【請求項１】
検証対象プログラム、及び前記検証対象プログラムの動作コンテキストとして与えられる仮定に関する情報を記憶する二次記憶装置と、
前記検証対象プログラムの条件分岐箇所へ到達確認用のコードを埋め込んで検証し、検証された範囲を網羅度として測定し、検証結果と共に測定結果を出力し、前記検証対象プログラムの動作コンテキストとして与えられる仮定の誤りの可能性を示す中央処理装置と
を具備する
プログラム検証装置。
【請求項２】
請求項１に記載のプログラム検証装置であって、
前記二次記憶装置は、
前記検証対象プログラムを記憶するプログラム記憶手段と、
前記検証対象プログラムの動作コンテキストとして与えられる仮定を含む表明を記憶する表明記憶手段と
を具備する
プログラム検証装置。
【請求項３】
請求項２に記載のプログラム検証装置であって、
前記中央処理装置は、
前記プログラム記憶手段から前記検証対象プログラムを読み取り、前記表明記憶手段から前記仮定を読み取り、予め定義されたエラーについての網羅的な検証を行い、検証結果を出力するモデル検査手段と、
前記プログラム記憶手段から前記検証対象プログラムを読み取り、前記検証対象プログラムの条件分岐箇所へ到達確認用のコードとして必ず不成立となるアサーション記述を埋め込み、前記表明記憶手段から前記仮定を読み取り、前記検証対象プログラムの条件分岐箇所への到達を確認し、確認結果から前記網羅度を算出し、前記仮定、前記網羅度、及び到達箇所・不到達箇所の情報を出力する網羅度測定手段と
を具備する
プログラム検証装置。
【請求項４】
請求項３に記載のプログラム検証装置であって、
前記中央処理装置は、
外手段から入力された検証対象プログラムを読み取り、前記プログラム記憶手段に格納するプログラム入力手段と、
ユーザが定義した表明を読み取り、前記表明記憶手段に格納する表明入力手段と
を更に具備する
プログラム検証装置。
【請求項５】
請求項１乃至４のいずれか一項に記載のプログラム検証装置であって、
前記中央処理装置は、前記網羅度が１００％未満であり、未検査の分岐が存在する場合、前記仮定に誤りがある可能性があると判断する
プログラム検証装置。
【請求項６】
検証対象プログラム、及び前記検証対象プログラムの動作コンテキストとして与えられる仮定に関する情報を参照するステップと、
前記検証対象プログラムの条件分岐箇所へ到達確認用のコードを埋め込んで検証し、検証された範囲を網羅度として測定し、検証結果と共に測定結果を出力し、前記検証対象プログラムの動作コンテキストとして与えられる仮定の誤りの可能性を示すステップと
を含む
プログラム検証方法。
【請求項７】
請求項６に記載のプログラム検証方法であって、
前記検証対象プログラムを保持するステップと、
前記検証対象プログラムの動作コンテキストとして与えられる仮定を含む表明を保持するステップと
を更に含む
プログラム検証方法。
【請求項８】
請求項７に記載のプログラム検証方法であって、
前記検証対象プログラムを読み取り、前記仮定を読み取り、予め定義されたエラーについての網羅的な検証を行い、検証結果を出力するステップと、
前記検証対象プログラムを読み取り、前記検証対象プログラムの条件分岐箇所へ到達確認用のコードとして必ず不成立となるアサーション記述を埋め込み、前記仮定を読み取り、前記検証対象プログラムの条件分岐箇所への到達への到達を確認し、確認結果から前記網羅度を算出し、前記仮定、前記網羅度、及び到達箇所・不到達箇所の情報を出力するステップと
を更に含む
プログラム検証方法。
【請求項９】
請求項８に記載のプログラム検証方法であって、
外部から入力された検証対象プログラムを読み取り、二次記憶装置に格納するステップと、
ユーザが定義した表明を読み取り、前記二次記憶装置に格納するステップと
を更に含む
プログラム検証方法。
【請求項１０】
請求項６乃至９のいずれか一項に記載のプログラム検証方法であって、
前記網羅度が１００％未満であり、未検査の分岐が存在する場合、前記仮定に誤りがある可能性があると判断するステップ
を更に含む
プログラム検証方法。
【請求項１１】
検証対象プログラム、及び前記検証対象プログラムの動作コンテキストとして与えられる仮定に関する情報を参照するステップと、
前記検証対象プログラムの条件分岐箇所へ到達確認用のコードを埋め込んで検証し、検証された範囲を網羅度として測定し、検証結果と共に測定結果を出力し、前記検証対象プログラムの動作コンテキストとして与えられる仮定の誤りの可能性を示すステップと
をコンピュータに実行させるための
プログラム。
【請求項１２】
請求項１１に記載のプログラムであって、
前記検証対象プログラムを保持するステップと、
前記検証対象プログラムの動作コンテキストとして与えられる仮定を含む表明を保持するステップと
を更にコンピュータに実行させるための
プログラム。
【請求項１３】
請求項１２に記載のプログラムであって、
前記検証対象プログラムを読み取り、前記仮定を読み取り、予め定義されたエラーについての網羅的な検証を行い、検証結果を出力するステップと、
前記検証対象プログラムを読み取り、前記検証対象プログラムの条件分岐箇所へ到達確認用のコードとして必ず不成立となるアサーション記述を埋め込み、前記仮定を読み取り、前記検証対象プログラムの条件分岐箇所への到達への到達を確認し、確認結果から前記網羅度を算出し、前記仮定、前記網羅度、及び到達箇所・不到達箇所の情報を出力するステップと
を更にコンピュータに実行させるための
プログラム。
【請求項１４】
請求項１３に記載のプログラムであって、
外部から入力された検証対象プログラムを読み取り、二次記憶装置に格納するステップと、
ユーザが定義した表明を読み取り、前記二次記憶装置に格納するステップと
を更にコンピュータに実行させるための
プログラム。
【請求項１５】
請求項１１乃至１４のいずれか一項に記載のプログラムであって、
前記網羅度が１００％未満であり、未検査の分岐が存在する場合、前記仮定に誤りがある可能性があると判断するステップ
を更にコンピュータに実行させるための
プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラム検証装置に関し、特にモデル検査技術を用いたプログラム検証装置に関する。
【背景技術】
【０００２】
プログラムの正しさ検証するために、ヌルポインタ参照、配列境界違反、或いはゼロ除算等の実行時エラーや、ユーザ定義のアサーション違反の有無をチェックする技術の１つに、状態空間を網羅的に探索するモデル検査技術を用いたプログラム検証がある。
【０００３】
モデル検査技術を用いて開放システムの検証を行う場合、検証対象システムの動作コンテキストを与える外部の環境モデリングが検証精度及び検証性能に大きな影響を与えるため、正しく環境モデリングを行うことが重要となる。モデル検査技術を用いたプログラムの検証でも、プログラム、特に関数・モジュール等により構成される部分プログラムは基本的に開放システムとなるので、外部の環境モデリングが事実上必須となる。
【０００４】
検証対象プログラムの外部環境をモデリングする方法としては、検証対象プログラムが実行される時点で前提となる条件（事前条件）を仮定として定義する手法が一般的に用いられている。
【０００５】
例えば、非特許文献１では、Ｊａｖａ（登録商標）プログラムのモデル検査の環境を構築する技術の中で仮定（該文献中では「ａｓｓｕｍｐｔｉｏｎ」と表記）が用いられている。
【０００６】
また、モデル検査技術を用いたプログラム検証においては、検査対象プログラムの動作コンテキストを与える仮定（主に、プログラムに対する入力の値域を制限する条件）や検査対象プログラムの振る舞いに関する制約等を表明として定義し、その正しさを確認するために、従来は、主に検証作業者（以下、作業者と表す）及び関係者によるレビューが行われていた。そのため、表明に含まれる仮定の誤りを見逃すことがあり、正しい検証結果を得られないことがあった。
【０００７】
非特許文献２、非特許文献３に、この問題を解決する方法として、検証結果の一部として出力される、誤った弱い仮定（入力の値域を弱く制限する条件）により誤検出された問題に着目し、検証の過程で誤った弱い仮定を修正する手法（以下、ＣＥＧＥＲと表す）が提案されている。ところが、該手法（ＣＥＧＥＲ）では、問題の見逃しを引き起こす、誤った強い仮定（入力の値域を強く制限する条件）が存在することを知り、仮定を修正することはできない。
【０００８】
例えば、図１に示すＣ言語プログラムに対してモデル検査技術を用いたゼロ除算エラーのプログラム検証を行う場合を考える。
【０００９】
モデル検査技術では状態空間を網羅的に探索して検査するので、プログラムの実行箇所とその時点での全変数の値の組み合わせを状態として定義した場合には、全変数値の取り得る組合せ、及び、その組合せで到達可能な全実行パスについて検査することができる。また、外部からの入力は非決定な任意値として扱われるので、該プログラムでは関数の引数ｎ１、ｎ２、ａが任意値として扱われる。この場合、任意値は、最小値「ＩＮＴ＿ＭＩＮ」から最大値「ＩＮＴ＿ＭＡＸ」までの値である。
【００１０】
該プログラムでは、１〜５行目のコメントにある条件を前提としているので、動作コンテキストとして与えられる仮定は、引数ｎ１に対する条件「ｎ１＝＝  ０｜｜ｎ１  ＝＝  １」が正しい。その仮定を用いてプログラム検証をした場合、２２行目のローカル変数ｙの値の設定ミスを原因とする２６行目のｙでのゼロ除算エラーが検出される。２５行目にもローカル変数ｘでの除算があるが、前記の仮定のもとでは必ずｘに０以外の値が設定されるので、ゼロ除算エラーは検出されない。
【００１１】
これに対して、誤って弱い仮定、例えば「ｎ１  ＞＝  ０」という仮定が与えられた場合、ｎ１の値が１以外の正値の場合には、ｘの値は０に初期化されたままで２５行目に到達するので、そこで発生するゼロ除算エラーも問題として検出される。ＣＥＧＥＲでは、検出された問題が誤検出と判断された場合に誤検出の原因を作業者が分析し、その分析結果にもとづき仮定を修正することができる。
【００１２】
ところが、誤って強い仮定、例えば「（ｎ１  ＝＝  ０｜｜ｎ１  ＝＝  １）＆＆  ｎ２  ＞＝０」という仮定が与えられた場合、ｎ２は負値になることがなく、２１〜２３行の「ｅｌｓｅ」節に到達する実行パスは検査されないので、本来発生する可能性のある２５行目のゼロ除算エラーは問題として検出されない。この場合、検証結果だけでは仮定の誤りを知る手がかりがないので、仮定を修正することができない。
【００１３】
関連する技術として、特開２００８−０７１１３５号公報（特許文献１）に検証処理装置が開示されている。
この関連技術では、モデル検査は、状態遷移図(状態遷移グラフ)の全ての状態と全てのパスの検査を行い、指定された特徴を持つ状態や遷移パスが存在するか否かを判定する。モデル検査を用いた検証処理装置では、検証対象であるデータ処理システムの動作を状態遷移グラフに変換し、また検証対象であるデータ処理システムの機能仕様を状態遷移グラフ上の状態または遷移パスの特徴に変換する。このとき、検証対象であるデータ処理システムの状態遷移グラフを取得し、データ処理システムへの要求を取得し、データ処理システムの検証範囲に含まれるべき動作を示すカバレッジ指標を取得する。取得された状態遷移グラフが要求を満足するか検証し、取得されたカバレッジ指標に対応して状態遷移グラフのカバレッジを測定し、結果を出力する。
【００１４】
【非特許文献１】Ｏ．  Ｔｋａｃｈｕｋ，  Ｍ．  Ｂ．  Ｄｗｙｅｒ，  ａｎｄ  Ｃ．  Ｓ．  Ｐａｓａｒｅａｎｕ．  “Ａｕｔｏｍａｔｅｄ  Ｅｎｖｉｒｏｎｍｅｎｔ  Ｇｅｎｅｒａｔｉｏｎ  ｆｏｒ  Ｓｏｆｔｗａｒｅ  Ｍｏｄｅｌ  Ｃｈｅｃｋｉｎｇ．”  Ｉｎ  Ｐｒｏｃｅｅｄｉｎｇｓ  ｏｆ  ｔｈｅ  １８ｔｈ  ＩＥＥＥ  Ｉｎｔｅｒｎａｔｉｏｎａｌ  Ｃｏｎｆｅｒｅｎｃｅ  ｏｎ  Ａｕｔｏｍａｔｅｄ  Ｓｏｆｔｗａｒｅ  Ｅｎｇｉｎｅｅｒｉｎｇ，  Ｏｃｔ．  ２００３．  ＜ｈｔｔｐ：／／ｔｉ．ａｒｃ．ｎａｓａ．ｇｏｖ／ｍ／ｐｕｂ／５９８ｈ／０５９８％２０（Ｔｋａｃｈｕｋ）．ｐｄｆ＞
【非特許文献２】Ａ．  Ｇｕｐｔａ，  “Ｆｒｏｍ  Ｈａｒｄｗａｒｅ  Ｖｅｒｉｆｉｃａｔｉｏｎ  ｔｏ  Ｓｏｆｔｗａｒｅ  Ｖｅｒｉｆｉｃａｔｉｏｎ：  Ｒｅ−ｕｓｅ  ａｎｄ  Ｒｅ−ｌｅａｒｎ”，  Ｈａｒｄｗａｒｅ  ａｎｄ  Ｓｏｆｔｗａｒｅ：  Ｖｅｒｉｆｉｃａｔｉｏｎ  ａｎｄ  Ｔｅｓｔｉｎｇ，  Ｔｈｉｒｄ  Ｉｎｔｅｒｎａｔｉｏｎａｌ  Ｈａｉｆａ  Ｖｅｒｉｆｉｃａｔｉｏｎ  Ｃｏｎｆｅｒｅｎｃｅ，  ＨＶＣ  ２００７，  Ｈａｉｆａ，  Ｉｓｒａｅｌ，  Ｏｃｔｏｂｅｒ  ２３−２５，  ２００７．  Ｐｒｏｃｅｅｄｉｎｇｓ，  ｐｐ．１４−１５
【非特許文献３】プレゼンテーション資料  ＜ｈｔｔｐ：／／ｗｗｗ．ｈａｉｆａ．ｉｂｍ．ｃｏｍ／Ｗｏｒｋｓｈｏｐｓ／ｖｅｒｉｆｉｃａｔｉｏｎ２００７／ｐｒｅｓｅｎｔ／Ａａｒｔｉ＿Ｇｕｐｔａ＿ｋｅｙｎｏｔｅ＿ｗｅｂ．ｐｄｆ＞
【特許文献１】特開２００８−０７１１３５号公報
【発明の開示】
【発明が解決しようとする課題】
【００１５】
仮定を用いてプログラムのモデル検査を行う場合、仮定が誤っていると検証結果も誤ったものとなる。具体的には、誤った弱い仮定が用いられた場合には本来問題とならない箇所が問題として検出され、誤った強い仮定が用いられた場合には本来問題となる箇所が問題として検出されない。すなわち、「誤検出」と「見逃し」が発生する。そのため、モデル検査により正しい検証結果を得るためには、検証前に、若しくは、検証の過程で、仮定を正しく定義する必要がある。
【課題を解決するための手段】
【００１６】
本発明のプログラム検証装置は、検証対象プログラム、及び検証対象プログラムの動作コンテキストとして与えられる仮定に関する情報を記憶する二次記憶装置と、検証対象プログラムの条件分岐箇所へ到達確認用のコードを埋め込んで検証し、検証された範囲を網羅度として測定し、検証結果と共に測定結果を出力し、検証対象プログラムの動作コンテキストとして与えられる仮定の誤りの可能性を示す中央処理装置とを具備する。
【００１７】
本発明のプログラム検証方法は、検証対象プログラム、及び検証対象プログラムの動作コンテキストとして与えられる仮定に関する情報を参照するステップと、検証対象プログラムの条件分岐箇所へ到達確認用のコードを埋め込んで検証し、検証された範囲を網羅度として測定し、検証結果と共に測定結果を出力し、検証対象プログラムの動作コンテキストとして与えられる仮定の誤りの可能性を示すステップとを含む。
【００１８】
本発明のプログラムは、検証対象プログラム、及び検証対象プログラムの動作コンテキストとして与えられる仮定に関する情報を参照するステップと、検証対象プログラムの条件分岐箇所へ到達確認用のコードを埋め込んで検証し、検証された範囲を網羅度として測定し、検証結果と共に測定結果を出力し、検証対象プログラムの動作コンテキストとして与えられる仮定の誤りの可能性を示すステップとをコンピュータに実行させるためのプログラムである。
【００１９】
このように、条件分岐箇所へ到達確認用のコードを埋め込む等の既存技術を用いてモデル検査技術で検証した範囲を網羅度として測定し、検証結果とともにその測定結果を示すことにより、作業者に仮定の誤りの可能性を示す。網羅度が１００％未満の場合、すなわち、未検査の分岐が存在する場合には、仮定に誤りがある可能性がある。
【００２０】
例えば、図１に示すＣ言語プログラムに対して「（ｎ１  ＝＝  ０｜｜ｎ１  ＝＝  １）＆＆  ｎ２  ＞＝  ０」という仮定を用いてプログラム検証を行い、「問題無し」と言う検証結果とともに、網羅度８６％（「ｄｅｃｉｓｉｏｎ  ｃｏｖｅｒａｇｅ」での数値）を示す。これにより、作業者は仮定に誤りがある可能性があることがわかる。
【発明の効果】
【００２１】
モデル検査技術を用いたプログラムの検証において、プログラム検証に用いる仮定の誤りの可能性を明示し、仮定を正しく定義することを可能にする。
【発明を実施するための最良の形態】
【００２２】
以下に、本発明の第１実施形態について添付図面を参照して説明する。
図２に示すように、本実施形態におけるプログラム検証装置は、中央処理装置１０と、二次記憶装置２０と、入力装置３０と、出力装置４０を備える。
【００２３】
中央処理装置１０は、プログラム入力部１１と、表明入力部１２と、モデル検査部１３と、網羅度測定部１４を備える。
【００２４】
二次記憶装置２０は、プログラム記憶部２１と、表明記憶部２２を備える。
【００２５】
プログラム入力部１１は、入力装置３０から検証対象プログラムを読み取り、二次記憶装置２０のプログラム記憶部２１に格納する。
【００２６】
表明入力部１２は、入力装置３０から作業者等のユーザが定義した表明を読み取り、二次記憶装置２０の表明記憶部２２に格納する。
【００２７】
モデル検査部１３は、プログラム記憶部２１から検証対象プログラムを読み取り、表明記憶部２２から検証対象プログラムの動作コンテキストとして与えられる仮定を読み取り、予め定義されたエラーについての網羅的な検証を行い、出力装置４０に検証結果を出力する。
【００２８】
網羅度測定部１４は、プログラム記憶部２１から検証対象プログラムを読み取り、条件分岐箇所へ到達確認用のコードを埋め込み、表明記憶部２２から検証対象プログラムの動作コンテキストとして与えられる仮定を読み取り、モデル検査部１３を用いて条件分岐箇所への到達を確認し、その確認結果から網羅度を算出し、出力装置４０に仮定と網羅度と到達箇所・不到達箇所の情報を出力する。このとき、網羅度測定部１４は、網羅度が１００％未満であり、未検査の分岐が存在する場合、前記仮定に誤りがある可能性があると判断し、その旨を示す情報を出力するようにしても良い。
【００２９】
プログラム記憶部２１は、検証対象プログラムを記憶する。
【００３０】
表明記憶部２２は、検証対象プログラムの動作コンテキストとして与えられる仮定を含む表明を記憶する。
【００３１】
中央処理装置１０の例として、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）やマイクロプロセッサ（ｍｉｃｒｏｐｒｏｃｅｓｓｏｒ）等の処理装置、又は同様の機能を有する半導体集積回路（Ｉｎｔｅｇｒａｔｅｄ  Ｃｉｒｃｕｉｔ（ＩＣ））等が考えられる。なお、プログラム入力部１１、表明入力部１２、モデル検査部１３、及び網羅度測定部１４は、各々の機能をコンピュータに実行させるためのプログラムでも良い。但し、実際には、これらの例に限定されない。
【００３２】
二次記憶装置２０の例として、メモリ等の半導体記憶装置、ハードディスク等の外部記憶装置（ストレージ）、又は、記憶媒体（メディア）等が考えられる。但し、実際には、これらの例に限定されない。
【００３３】
入力装置３０の例として、キーボードやキーパッド、画面上のキーパッド、タッチパネル（ｔｏｕｃｈ  ｐａｎｅｌ）、タブレット（ｔａｂｌｅｔ）、又は、記憶媒体（メディア）等の読取装置等が考えられる。或いは、入力装置３０は、外部の入力装置や記憶装置から情報を取得するためのインターフェース（Ｉ／Ｆ：ｉｎｔｅｒｆａｃｅ）でも良い。但し、実際には、これらの例に限定されない。
【００３４】
出力装置４０の例として、ＬＣＤ（液晶ディスプレイ）やＰＤＰ（プラズマディスプレイ）、有機ＥＬディスプレイ（ｏｒｇａｎｉｃ  ｅｌｅｃｔｒｏｌｕｍｉｎｅｓｃｅｎｃｅ  ｄｉｓｐｌａｙ）等の表示装置、又は、表示内容を壁やスクリーンに投影するプロジェクタ等の映写装置、表示内容を用紙等に印刷するプリンタ等の印刷装置等が考えられる。或いは、出力装置４０は、外部の表示装置や記憶装置に情報を出力するためのインターフェースでも良い。但し、実際には、これらの例に限定されない。
【００３５】
次に、図３のフローチャートを参照して、中央処理装置１０が行う動作について、実際のデータを用いて詳細に説明する。ここでは、図１に示すＣ言語プログラムに対して、「（ｎ１＝＝  ０｜｜ｎ１  ＝＝  １）＆＆  ｎ２  ＞＝  ０」と言う仮定を用いてゼロ除算エラーのプログラム検証をすることとする。
【００３６】
（１）ステップＳＴ１
まず、プログラム入力部１１は、入力装置３０から検証対象プログラムを読み取り、二次記憶装置２０のプログラム記憶１３１に格納する。ここでは、プログラム入力部１１は、入力装置３０から図１に示すＣ言語プログラムを読み取り、二次記憶装置２０のプログラム記憶１３１に格納する。
【００３７】
（２）ステップＳＴ２
表明入力部１２は、入力装置３０からユーザが定義した表明を読み取り、二次記憶装置２０の表明記憶部２２に格納する。ここでは、表明入力部１２は、入力装置３０から「（ｎ１＝＝  ０｜｜ｎ１  ＝＝  １）＆＆  ｎ２  ＞＝  ０」と言う仮定だけからなる表明を読み取り、二次記憶装置２０の表明記憶部２２に格納する。
【００３８】
（３）ステップＳＴ３
次に、モデル検査部１３は、プログラム記憶部２１から検証対象プログラムを、表明記憶部２２から検証対象プログラムの動作コンテキストとして与えられる仮定を読み取り、予め定義されたエラーについての網羅的な検証を行う。ここでは、モデル検査部１３は、プログラム記憶部２１に格納された検証対象プログラムを読み取り、表明記憶部２２に格納された仮定を読み取り、ゼロ除算エラーについての網羅的な検証を行い、「問題なし」と言う結果を得る。
【００３９】
（４）ステップＳＴ４
網羅度測定部１４は、プログラム記憶部２１から検証対象プログラムを読み取り、条件分岐箇所へモデル検査部１３の仕様や実装に依存した形式の到達確認用のコードを埋め込み、表明記憶部２２から仮定を読み取り、モデル検査部１３を用いて条件分岐箇所への到達を確認し、その結果から網羅度を算出する。ここでは、網羅度測定部１４は、プログラム記憶部２１から検証対象プログラムを読み取り、条件分岐箇所へ到達確認用のコードを埋め込み、図４のようなプログラムを作成する。なお、到達確認用のコードは、必ず不成立となるアサーション記述（ＡＳＳＥＲＴ（０）等）であるものとする。モデル検査部１３は、アサーション記述毎にモデル検査を行い、検証対象プログラムの条件分岐箇所への到達への到達を確認する。このとき、モデル検査部１３は、アサーションの不成立が検出されれば到達、検出されなければ不到達と判断する。この事例では、モデル検査部１３は、条件分岐箇所への到達を確認すると、「１１、１５、１８、２０、２６、２９行目」は到達し、「３２行目」は到達しないことが分かるので、その結果から網羅度を「８６％」と算出する。すなわち、モデル検査部１３は、７つの条件分岐箇所「１１、１５、１８、２０、２６、２９、３２行目」のうち、６つの条件分岐箇所「１１、１５、１８、２０、２６、２９行目」に到達しているため、網羅度を「（６÷７）×１００≒８６％」と算出する。
【００４０】
（５）ステップＳＴ５
最後に、網羅度測定部１４は、検証に用いた仮定、算出された網羅度、及び到達箇所・不到達箇所の情報を出力装置４０に出力し、モデル検査部１３は、検証した結果を出力装置４０に出力し、終了する。ここでは、網羅度測定部１４は、検証に用いた仮定「（ｎ１＝＝  ０｜｜ｎ１  ＝＝  １）＆＆  ｎ２  ＞＝  ０」と、算出された網羅度「８６％」と、不到達箇所として「３２行目」を出力装置４０に出力し、モデル検査部１３は、検証した結果として「問題なし」を出力装置４０に出力し、終了する。
【００４１】
作業者は、出力装置４０に出力された網羅度が１００％未満であることから、入力した仮定「（ｎ１＝＝  ０｜｜ｎ１  ＝＝  １）＆＆  ｎ２  ＞＝  ０」に誤りがある可能性があることがわかる。
【００４２】
本発明の第１の効果は、プログラム検証に用いる仮定の誤りを見逃さなくなることにある。その理由は、検証に用いた仮定と一緒に網羅度が表示されることにより作業者に仮定の誤りがある可能性を示すことができるためである。
【００４３】
本発明の第２の効果は、不到達コード（デッドコード）を検出できることにある。その理由は、誤りの可能性を指摘された仮定について精査した結果、仮定に誤りがないことが判明した場合、不到達箇所として示された分岐箇所は不到達コードと判断できるためである。
【００４４】
以下に、本発明の第２実施形態について説明する。
図２に示す装置の構成において、入力装置１１２、プログラム入力部１１、表明入力部１２が無くても良い。例えば、二次記憶装置２０がリポジトリとして使われている等、検証対象プログラム及び表明が二次記憶装置２０に事前に格納されている場合、中央処理装置１０は、検証対象プログラム及び表明を、二次記憶装置２０から直接読み取る。この場合、中央処理装置１０は、事前設定に基づき自動的に、或いは、ユーザ操作に応じて、検証対象プログラム及び表明を、二次記憶装置２０から直接読み取る。
【００４５】
以下に、本発明の第３実施形態について説明する。
図２に示す装置の構成において、網羅度測定部１４がモデル検査部１３と分離しておらず、統合されていても良い。その場合、統合されたモデル検査部１３が、図３のフローチャートのステップＳＴ３、ステップＳＴ４、ステップＳＴ５の全てを行うことになる。
【００４６】
以下に、本発明の第４実施形態について説明する。
図３に示すフローチャートにおいて、ステップＳＴ３のモデル検査処理が無くても良い。その場合、ステップＳＴ５では検証結果は出力できず、網羅度により誤った強い仮定になっている可能性は示せるが、問題の誤検出を引き起こす誤った弱い仮定の可能性を示すことはできない。すなわち、ＣＥＧＥＲは行えない。また、ステップＳＴ３のモデル検査処理とステップＳＴ４の網羅度測定処理は順序が逆でも並行して行われても良い。
【００４７】
以上のように、本発明は、プログラムと表明を入力としモデル検査技術を用いたプログラムの検証において、検査対象プログラムの動作コンテキストを与える仮定の誤りの可能性を示すことを可能にする。
【００４８】
本発明によれば、モデル検査技術を用いたプログラム検証における仮定の修正や、プログラムの不具合検出といった用途に適用できる。
【００４９】
以上、本発明の実施形態を詳述してきたが、実際には上記の実施形態に限られるものではなく、本発明の要旨を逸脱しない範囲の変更があっても本発明に含まれる。
【図面の簡単な説明】
【００５０】
【図１】図１は、検証対象プログラムの例を示す図である。
【図２】図２は、本発明の第１実施形態におけるプログラム検証装置の構成例を示す図である。
【図３】図３は、中央処理装置の動作を示すフローチャートである。
【図４】図４は、条件分岐箇所へ到達確認用のコードを埋め込んだプログラムの例を示す図である。
【符号の説明】
【００５１】
１０…  中央処理装置
１１…  プログラム入力部
１２…  表明入力部
１３…  モデル検査部
１４…  網羅度測定部
２０…  二次記憶装置
２１…  プログラム記憶部
２２…  表明記憶部
３０…  入力装置
４０…  出力装置
【図１】
2010072883.tif 000003
【図２】
2010072883.tif 000004
【図３】
2010072883.tif 000005
【図４】
2010072883.tif 000006