(57)【要約】【課題】モデル検証器を用いたプログラム検証において、関連性の低い部分の検証用プログラムを好適に削減することにより、モデル検証に必要な状態数を削減する仕組みを提供する。【解決手段】情報処理装置は、被検証プログラムの検証する内容を示す検証式を作成し、検証式に関連するプログラムであるか否かを所定単位の被検証プログラムごとに判定し、検証式に関連するプログラムであると判定された被検証プログラムについては、モデル検証プログラムを実行するためのプログラムに被検証プログラムを変換し、検証式に関連するプログラムでないと判定された被検証プログラムについては、予め定義されたテンプレート適用データを用いて、モデル検証プログラムで実行する簡易的なプログラムを生成し、変換されたプログラム、及び生成されたプログラムをモデル検証プログラムによって検証する。【選択図】  図１
2015156053.tif 000002
【特許請求の範囲】
【請求項１】
情報処理装置であって、
被検証プログラムの検証する内容を示す検証式を作成する作成手段と、
前記作成手段によって作成された検証式に関連するプログラムであるか否かを所定単位の被検証プログラムごとに判定する判定手段と、
前記判定手段によって前記検証式に関連するプログラムであると判定された前記被検証プログラムについては、該被検証プログラムの状態を網羅的に探索して検証するモデル検証プログラムを実行するためのプログラムに該被検証プログラムを変換する変換手段と、
前記判定手段によって前記検証式に関連するプログラムでないと判定された前記被検証プログラムについては、予め定義されたテンプレート適用データを用いて、前記モデル検証プログラムで実行する簡易的なプログラムを生成する生成手段と、
前記変換手段によって変換されたプログラム、及び前記生成手段によって生成されたプログラムを前記モデル検証プログラムによって検証する検証手段と
を備えることを特徴とする情報処理装置。
【請求項２】
前記判定手段は、初回の検証であれば、前記検証式に関連するプログラムであっても、前記検証式に関連するプログラムでないものとして判定することを特徴とする請求項１に記載の情報処理装置。
【請求項３】
前記検証手段は、前記モデル検証プログラムによって検証した検証結果が状態爆発を起こしていると判断すると、利用可能な前記テンプレート適用データがあれば、前記生成手段によって該テンプレート適用データを用いて前記簡易的なプログラムを生成させ、検証を再度行うことを特徴とする請求項２に記載の情報処理装置。
【請求項４】
前記変換手段は、さらに、前記変換した被検証プログラムに、前記検証式を埋め込むことを特徴とする請求項１乃至３の何れか１項に記載の情報処理装置。
【請求項５】
前記テンプレート適用データは、形式仕様記述言語で記述されていることを特徴とする請求項１乃至４の何れか１項に記載の情報処理装置。
【請求項６】
前記判定手段は、前記関連するプログラムであるか否かを、前記所定単位の被検証プログラムの中に前記検証式に対応するコードを含むか否かによって判定することを特徴とする請求項１乃至５の何れか１項に記載の情報処理装置。
【請求項７】
前記所定単位とは、関数であることを特徴とする請求項１乃至６の何れか１項に記載の情報処理装置。
【請求項８】
前記所定単位とは、変数であることを特徴とする請求項１乃至６の何れか１項に記載の情報処理装置。
【請求項９】
前記検証式には、関数名と、該関数内における行番号、及び検証内容を示す検証式が含まれることを特徴とする請求項７に記載の情報処理装置。
【請求項１０】
前記検証式において検証する内容は、配列外参照であることを特徴とする請求項１乃至９の何れか１項に記載の情報処理装置。
【請求項１１】
前記検証手段による検証結果をユーザーに提示する手段をさらに備えることを特徴とする請求項１乃至１０の何れか１項に記載の情報処理装置。
【請求項１２】
情報処理装置の制御方法であって、
作成手段が、被検証プログラムの検証する内容を示す検証式を作成する作成工程と、
判定手段が、前記作成工程において作成された検証式に関連するプログラムであるか否かを所定単位の被検証プログラムごとに判定する判定工程と、
変換手段が、前記判定工程において前記検証式に関連するプログラムであると判定された前記被検証プログラムについては、該被検証プログラムの状態を網羅的に探索して検証するモデル検証プログラムを実行するためのプログラムに該被検証プログラムを変換する変換工程と、
生成手段が、前記判定工程において前記検証式に関連するプログラムでないと判定された前記被検証プログラムについては、予め定義されたテンプレート適用データを用いて、前記モデル検証プログラムで実行する簡易的なプログラムを生成する生成工程と、
検証手段が、前記変換工程において変換されたプログラム、及び前記生成工程において生成されたプログラムを前記モデル検証プログラムによって検証する検証工程と
を実行することを特徴とする情報処理装置の制御方法。
【請求項１３】
請求項１乃至１０の何れか１項に記載の情報処理装置としてコンピュータを機能させるための該コンピュータで読み取り可能なプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検証プログラムを用いた情報処理装置、その制御方法、及びプログラムに関する。
【背景技術】
【０００２】
プログラムの振る舞いを自動的且つ網羅的に検証する為の方法として、モデル検証プログラムを用いたプログラム検証方法がある。検証方法では、ユーザーの作成したプログラム（以下、被検証プログラムコードと称する。）及び検証式が、ＳＰＩＮやＳＭＶのようなモデル検証プログラムを利用できる言語のプログラムコード（以下、検証用プログラムコードと称する。）に変換される。変換された上でモデル検証プログラムに入力・実行し、検証式違反の有無の確認が行われる。
【０００３】
このプログラム検証方法において、被検証プログラムコードの規模により、一般的に状態爆発と言われる状態数の多さ故にメモリ不足に陥りプログラム検証を実行できなくなってしまう問題がある。その為、モデル検証プログラムにおいては、特許文献１のように、取り扱える状態数を増加させる必要がある。また、モデル検証プログラムのユーザーは、検証を行う検証用プログラムコードをモデル検証プログラムを取り扱えるだけの、小ささに留める必要がある。
【０００４】
検証用プログラムコードを小さくする為には、被検証プログラムコードを各々の検証式毎にした検証用プログラムコードを複数生成し、且つ各々の検証に関係の無いプログラムコード及び変数シンボルを削除（以下、プログラムスライスと称する）する方法がある。或いは、使用メモリサイズを必要最小限のビット長さまで小さくする、意味的に有意性のある代表インデックス値に変換する（以下、データ抽象化と称する）等の方法がある。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開平０７−３３４５６６号公報
【発明の概要】
【発明が解決しようとする課題】
【０００６】
しかしながら、上記従来技術には以下に記載する問題がある。上記従来技術では、被検証プログラムコードの動作の検証を行うことが可能である。しかし、この方法を用いた場合、大域的な制御に対する検証を行う場合に、より多くの検証用プログラムコード・メモリが必要となり、状態爆発が発生して検証を実行することができない場合がある。
【０００７】
大域的な制御に対する検証を行う場合には、大域的な制御に含まれる全ての被検証プログラムコードから検証用プログラムコードを作成する。そのため、本来検証したい内容との関係はあるものの、関連性の低い被検証プログラムコード断片や、別の方法によって既に十分に検証が行われている被検証プログラムコード断片も検証用プログラムコードに組み込まれてしまう。したがって、検証用プログラムコードの使用するメモリ数やステップ数が増大してしまい、状態爆発が発生してしまう。
【０００８】
本発明は、上述の問題に鑑みて成されたものであり、モデル検証器を用いたプログラム検証において、関連性の低い部分の検証用プログラムを好適に削減することにより、モデル検証に必要な状態数を削減する仕組みを提供することを目的とする。
【課題を解決するための手段】
【０００９】
本発明は、情報処理装置であって、被検証プログラムの検証する内容を示す検証式を作成する作成手段と、前記作成手段によって作成された検証式に関連するプログラムであるか否かを所定単位の被検証プログラムごとに判定する判定手段と、前記判定手段によって前記検証式に関連するプログラムであると判定された前記被検証プログラムについては、該被検証プログラムの状態を網羅的に探索して検証するモデル検証プログラムを実行するためのプログラムに該被検証プログラムを変換する変換手段と、前記判定手段によって前記検証式に関連するプログラムでないと判定された前記被検証プログラムについては、予め定義されたテンプレート適用データを用いて、前記モデル検証プログラムで実行する簡易的なプログラムを生成する生成手段と、前記変換手段によって変換されたプログラム、及び前記生成手段によって生成されたプログラムを前記モデル検証プログラムによって検証する検証手段とを備えることを特徴とする。
【発明の効果】
【００１０】
本発明によれば、モデル検証器を用いたプログラム検証において、関連性の低い部分の検証用プログラムを好適に削減することにより、モデル検証に必要な状態数を削減することができる。
【図面の簡単な説明】
【００１１】
【図１】第１の実施形態に係る情報処理装置のソフトウェア構成を示すブロック図。
【図２】第１の実施形態に係る情報処理装置のハードウェア構成を示すブロック図。
【図３Ａ】、
【図３Ｂ】第１の実施形態に係る情報処理装置の処理手順を示すフローチャート。
【図４Ａ】、
【図４Ｂ】、
【図４Ｃ】、
【図４Ｄ】、
【図４Ｅ】、
【図４Ｆ】第１の実施形態に係る被検証プログラムを示す図。
【図５Ａ】、
【図５Ｂ】第２の実施形態に係る情報処理装置の処理手順を示す図。
【図６Ａ】、
【図６Ｂ】、
【図６Ｃ】、
【図６Ｄ】、
【図６Ｅ】、
【図６Ｆ】第２の実施形態に係る被検証プログラムを示す図。
【発明を実施するための形態】
【００１２】
以下、添付図面を参照して本発明の実施形態を詳しく説明する。なお、以下の実施形態は特許請求の範囲に係る本発明を限定するものでなく、また本実施形態で説明されている特徴の組み合わせの全てが本発明の解決手段に必須のものとは限らない。
【００１３】
＜第１の実施形態＞
以下では、図１乃至図４Ｆを参照して本発明の第１の実施形態について説明する。検証すべきプログラムの性質の例として、被検証コードがＣ言語で記述されたソースコードである場合、「配列外へのメモリアクセスは行ってはならない」（以下、配列外参照と称する。）等の言語仕様からもたらされる検証仕様がある。配列外参照の検証を行うには、被検証プログラムを解析して配列アクセスを行うプログラム断片の関数名と位置を求め、配列の添え字が配列に対して確保されたメモリ容量を超えないことを確認するための検証式を生成する。配列の添え字や割り算の分母が定数である場合には、静的プログラム解析のみで検証を終了することが可能である。一方、配列の添え字や割り算の分母が変数である場合には、静的プログラム解析だけで検証を終えられない場合が多い。本実施形態は、配列の添え字が定数ではなく変数である場合について、モデル検証プログラムとしてＳＰＩＮを用いて、性質についてのプログラム検証を行う場合について説明する。ＳＰＩＮとは、チャネル通信オートマトンを記述するための言語であるＰｒｏｍｅｌａによる記述を入力として、網羅的に状態を探索し、その性質を検証するモデル検証プログラムである。
【００１４】
＜ソフトウェア構成＞
まず、図１を参照して、本実施形態に係るプログラム検証装置である情報処理装置のソフトウェア構成について説明する。プログラム検証プログラム１０１は、図２に示す情報処理装置２０１において実行される。プログラム検証プログラム１０１は、動作制御ブロック１０２、被検証プログラムコード使用判断ブロック１０５、テンプレートコード生成ブロック１０６、コード縮小ブロック１０７、言語変換ブロック１０８、及びモデル検証プログラム１１０を含む。
【００１５】
動作制御ブロック１０２は、プログラム検証プログラムの様々な処理を行う為の動作制御ブロックである。被検証プログラムコード１０３は、検証を行う対象である様々なユーザープログラムである。テンプレート適用データ１０４は、プログラム検証プログラム１０１内の被検証プログラムコード使用判断ブロック１０５及びテンプレートコード生成ブロック１０６で解釈可能な形式仕様記述言語で記述されている。テンプレート適用データ１０４は、プログラムコード断片の振る舞いやメモリの性質を示すデータであり、モデル検証プログラム１１０に入力する検証対象のプログラムコードを生成するためのデータである。当該テンプレート適用データ１０４を用いて、モデル検証プログラム１１０で実行されるコードを生成すると、当該被検証プログラムをそのままモデル検証プログラムで実行可能な形式に変換するよりも、簡略化されたコードを生成することができる。
【００１６】
動作制御ブロック１０２は、被検証プログラムコード使用判断ブロック１０５に、被検証プログラムコード１０３とテンプレート適用データ１０４の両方を入力し、被検証プログラムコード１０３を解析した後に使用するコードを判断させる。具体的には、被検証プログラムコード１０３を使用するのか、又は、テンプレート適用データ１０４から生成したプログラムコードを使用するのかを判断する。被検証プログラムコード使用判断ブロック１０５が被検証プログラムコード１０３を使用すると判断した場合には、動作制御ブロック１０２は、被検証プログラムコード１０３をコード縮小ブロック１０７に入力する。コード縮小ブロック１０７は、コード縮小を行ったプログラムコード断片を出力する。その後、動作制御ブロック１０２は、当該プログラムコード断片を、言語変換ブロック１０８に入力して検証用プログラム１０９の断片を作成する。
【００１７】
一方、テンプレート適用データ１０４を使用する場合には、動作制御ブロック１０２は、テンプレート適用データ１０４をテンプレートコード生成ブロック１０６に入力して検証用プログラム１０９の断片を作成する。モデル検証プログラム１１０を実行するのに必要な全ての検証用プログラム１０９の断片を作成した後、動作制御ブロック１０２は、検証用プログラム１０９をモデル検証プログラム１１０に入力し、検証結果１１１を作成、取得し、当該検証結果をユーザーに報知する。
【００１８】
＜ハードウェア構成＞
次に、図２に、本提案のプログラム検証装置を構成するハードウェアブロック図を示す。情報処理装置２０１は、ユーザーの作成したプログラムの検証を行う装置である。情報処理装置２０１は、本体部２０２、表示装置２０３、キーボード２０４、及びマウス２０５を備える。また、本体部２０２は、中央処理装置２０６、主記憶装置２０７、及びハードディスク２０８を備える。図１に示したモデル検証プログラム１１０及びプログラム検証装置用プログラム１００は、ハードディスク２０８に格納されており、実行時には主記憶装置２０７にロードされ、中央処理装置（ＣＰＵ）２０６によって実行される。
【００１９】
＜プログラム例＞
次に、図４を参照して、本実施形態で説明する被検証プログラムコード１０３と、モデル検証プログラム１１０としてＳＰＩＮを用いる場合の検証用プログラム１０９との一例について説明する。本実施形態では、図４Ａに示すＣ言語の被検証プログラムコードを一般的なコンパイラで、図４Ｂに示すように、３番地コード化した上でプログラム検証作業を行う。また、本実施形態では、図４ＢのｔａｒｇｅｔＳｕｂ関数の４行目の配列アクセス（ｄａｔａ［ｉ］＝０；）についての配列外参照について説明する。図４ＢのＢＩＴ＿ＦＩＥＬＤ＿ＲＥＦ＜ｘｘ，ｙ，ｚ＞は、ｘｘ変数のｚｂｉｔ目からｙｂｉｔだけのデータを示す。
【００２０】
図４Ｃは、上記配列外参照についてプログラム検証プログラム１０１の作成した検証式データである。検証式には、図４Ｃに示すように、関数名と、当該関数内における行番号と、当該行番号における検証内容（検証式）とが含まれる。図４Ｃでは、１つの検証式のみが例示されているが、複数の検証式が予め定義されてもよい。また、図４Ｄは、比較例となる検証用プログラム１０９を全て被検証プログラムコード１０３から作成した場合の検証プログラムを示す。図４Ｆは、ｕｐｄａｔｅＰａｐｅｒＰａ関数について被検証プログラムコード１０３ではなく、テンプレート適用データ１０４から生成した検証用プログラム１０９を示す。
【００２１】
図４Ｅは、ｕｐｄａｔｅＰａｐｅｒＰａｐ関数についてのテンプレート適用データである。図４ＥはＸＭＬ形式でプログラム動作中に値が変化する変数を定義している。本実施形態ではｖｏｌａｔｉｌｅＭｅｍｏｒｙタグは、プログラム動作中に値が変化する変数の定義に用いられるタグである。ｎａｍｅＯｆＳｙｍｂｏｌは上記変数の名称の記述例である。ＳｅｔｔｌｅＦｕｎｃは上記変数を定義する関数名の記述例である。ｕｐｄａｔｅＩｎｔｅｒｖａｌは上記関数を指定回数呼び出した場合に変数が更新される間隔を定義する場合の記述例である。即ち、図４Ｅにおいては、ｓｅｎｓｏｒ．ｐａｐはｕｐｄａｔｅＳｅｎｓｏｒＰａｐが１０回呼び出される毎に、いずれかの値に変化する変数であることを示す。
【００２２】
＜処理フロー＞
次に、図３Ａ及び図３Ｂを参照して、本実施形態のプログラム検証における処理フローについて説明する。本実施形態では、ｔａｒｇｅｔＳｕｂ関数内の配列外参照（ｄａｔａ［ｉ］＝０；）を検証するケースについて説明する。以下で説明する処理は、中央処理装置（ＣＰＵ）２０６が、ハードディスク２０８に格納されたプログラム検証プログラム１０１を主記憶装置２０７に読み出して実行することにより実現される。図３Ａの３００は、プログラム検証の全体フローを示す。図３Ｂの３１０は、フローチャート３００内のＳ３０４のサブフローチャートを示す。図３Ｂの３２０は、フローチャート３００のＳ３０５内のサブフローチャートを示す。
【００２３】
Ｓ３０１、Ｓ３０２において、ＣＰＵ２０６は、図４Ａに示す被検証プログラムコード１０３と、図４Ｅに示すテンプレート適用データ１０４とを読み出し、被検証プログラムコード１０３を解析する。途中、ＣＰＵ２０６は、図４Ｂのように３番地コード化して副作用動作プログラムコードを単一動作プログラムコードに変換し、検証式と行番号の対応を簡便化することが可能である。
【００２４】
Ｓ３０３において、ＣＰＵ２０６は、図４Ｃのような検証式リストを作成する。つまり、ここでは、被検証プログラムコード１０３において検証する項目を作成している。これは、例えば、ユーザ指示に基づいて行われてもよい。当該ユーザ指示については、予め定義されたリスト等から選択する形式でもよい。ＣＰＵ２０６は、検証式リストの番号に対応する各々の検証プログラムを作成する。そのため、検証式によって、ｔａｒｇｅｔＳｕｂの４行目における変数ｉについてコード縮小ブロック１０７を用いて被検証プログラムコード１０３を縮小化し、必要な被検証プログラム断片を取得する。その結果、ｔａｒｇｅｔＳｕｂは、ｍａｉｎ関数から呼び出されており、グローバル変数ｓｅｎｓｏｒ．ｐａｐによって実行されるか否かの到達性が定義され、且つ、グローバル変数ｓｅｎｓｏｒ．ｐａｐは、ｍａｉｎ関数の呼び出すｕｐｄａｔｅＳｅｎｓｏｒＰａｐによって値が設定されることを理解する。
【００２５】
Ｓ３０４において、ＣＰＵ２０６は、被検証プログラムコード１０３を使用するか否かを判断する。即ち、被検証プログラムコードをモデル検証プログラムで実行できる形式にそのまま変換した詳細な被検証プログラムに変換するか、或いは、被検証プログラムの代わりにテンプレート適用データを使用した簡易的な被検証プログラムを生成するかを判断している。本実施形態によれば、プログラムの所定単位ごと、例えば関数ごとにこの判定を行い、検証を網羅的に行うか否かを決定している。なお、判断基準としては、Ｓ３０３で作成した検証リストに含まれる項目が当該関数を実行することにより実行されるか否かで判断することが望ましい。Ｓ３０４の詳細な処理についてはフローチャート３１０を用いて後述する。被検証プログラムコード１０３を使用する場合はＳ３０６に進み、使用しない場合はＳ３０５に進む。ｔａｒｇｅｔＳｕｂ関数及びｍａｉｎ関数は、図４Ｅのテンプレート適用データに含まれていない。ｕｐｄａｔｅＳｅｎｓｏｒＰａｐ関数はテンプレート適用データに含まれており、１０回呼び出された場合に、ｓｅｎｓｏｒ．ｐａｐをいずれかの値に設定する関数である。さらに、ｓｅｎｓｏｒ．ｐａｐは、１ｂｉｔ長さである。ＣＰＵ２０６は、このように、検証対象のプログラムを理解する。したがって、ｔａｒｇｅｔＳｕｂ関数及びｍａｉｎ関数については、Ｓ３０６に進み、ｕｐｄａｔｅＳｅｎｓｏｒＰａｐ関数についてはＳ３０５に進む。
【００２６】
被検証プログラムコード１０３を使用する場合、Ｓ３０６において、ＣＰＵ２０６は、ｍａｉｎ関数とｔａｒｇｅｔＳｕｂ関数については、被検証プログラムコード１０３を変換した上で、検証式をプログラム断片に変換して検証プログラム断片を埋め込む。一方、Ｓ３０５において、ＣＰＵ２０６は、ｕｐｄａｔｅＳｅｎｓｏｒＰａｐ関数について、テンプレート適用データ１０４をテンプレートコード生成ブロック１０６に入力してテンプレートコードを生成しＳ３０８に進む。Ｓ３０５の詳細については、フローチャート３０５を用いて後述する。
【００２７】
Ｓ３０８において、ＣＰＵ２０６は、モデル検証プログラムへ、Ｓ３０５又はＳ３０６からのプログラムを入力して実行する。仮にｕｐｄａｔｅＳｅｎｓｏｒＰａｐ関数をテンプレート適用データ１０４から生成せず、被検証プログラムコード１０３から生成した場合の検証用プログラム１０９を図４Ｄに示す。ｉｏ．ｐａｐは誰からも設定されることのない外部モデルに含まれる変数であるため、別スレッドとして、検証用プログラム断片を生成し不定性を定義する必要がある。また、ｕｐｄａｔｅＳｅｎｓｏｒＰａｐは、図４Ｂの被検証プログラムコードから変換したコードである。
【００２８】
図３Ａの説明に戻る。Ｓ３０９において、ＣＰＵ２０６は、検証結果１１１を取得し、ユーザーに提示する。これにより、検証式が不成立な場合があること等をユーザーに報知することができる。
【００２９】
次に、図３Ｂのフローチャート３１０について説明する。フローチャート３１０はフローチャート３００のＳ３０４の詳細を示す。
【００３０】
まず、Ｓ３０４１において、ＣＰＵ２０６は、図４Ｃに示す検証式に関連する被検証プログラムコードを抽出する。続いて、Ｓ３０４２において、ＣＰＵ２０６は、Ｓ３０４１で抽出した被検証プログラムコードに図４Ｃに示す検証式が含まれるか否かを判定する。該当する検証式が含まれる場合はＳ３０４３に進み、含まれない場合Ｓ３０４５に進む。
【００３１】
Ｓ３０４３において、ＣＰＵ２０６は、当該検証式が被検証プログラムの制御フローにのみ関連するものであるか否かを判定する。当該検証式が被検証プログラムの制御フローにのみ関連するものであれば、Ｓ３０４５に進み、そうでなければＳ３０４４に進む。
【００３２】
Ｓ３０４４において、ＣＰＵ２０６は、被検証プログラムコードを使用すると判断し、処理を終了する。一方、Ｓ３０４５において、ＣＰＵ２０６は、テンプレートコードを使用する（生成する）と判断し、処理を終了する。
【００３３】
次に、図３Ｂのフローチャート３２０について説明する。フローチャート３２０はフローチャート３００のＳ３０５の詳細を示す。つまり、フローチャート３２０は、テンプレートコード生成ブロック１０６の処理に相当する。
【００３４】
Ｓ３０５１において、ＣＰＵ２０６は、出力変数名と、ビット長さとを記憶する。続いて、Ｓ３０５２において、ＣＰＵ２０６は、入力変数のビット長さを記憶する。Ｓ３０５３において、ＣＰＵ２０６は、出力変数の更新頻度（１０）を記憶する。Ｓ３０５４において、ＣＰＵ２０６は、プログラムコード（テンプレートコード）を出力し、処理を終了する。出力されたテンプレートコードは、例えば、図４Ｆに示すｕｐｄａｔｅＳｅｎｓｏｒＰａｐ関数のコードとなる。なお、上述のフローチャートでは、説明を容易にするため、各関数ごと検証する例を示したが、本実施形態では、各関数ごとのプログラムコードを変換又は生成し、それらを合成した被検証プログラムをモデル検証プログラム１１０で検証することが望ましい。
【００３５】
図４Ｄと図４Ｆを比べると、図４Ｆはｉｏ．ｐａｐとｃｎｔ１が不要になっていること、ｓｅｎｓｏｒ．ｐａｐを合成する論理が無くなっていることから、モデル検証プログラム１１０の使用メモリは削減されている。実際にＳＰＩＮを用いて調べると、状態ベクタは２８バイトから２０バイトに削減されている。図４Ａに示す被検証プログラムコードの例では、図４Ｄでも図４Ｆでもモデル検証プログラムは実行可能であったものの、実際のプログラム検証ではより複雑なアルゴリズムも存在し、その場合にもより簡単な検証プログラムを合成することが可能である。
【００３６】
以上説明したように、本実施形態に係る情報処理装置は、所定単位の被検証プログラムごとに、検証対象のコードを有するか（検証式に関連するプログラムであるか）否かに応じて、被検証プログラムコードを使用するか否かを切り替える。つまり、本実施形態に係る情報処理装置は、検証対象のコード、例えば、配列外参照のコードを有する場合には詳細な検証を実行し、配列外参照のコードを含まなければテンプレートコードを用いた簡易的な検証を行う。なお、本実施形態では、所定単位のプログラムを関数ごとの例で説明したが、本発明をこれに限定する意図はなく他の単位のプログラムごとに上記判定を行ってもよい。このように、本実施形態によれば、所定の検証プログラムごとに、モデル検証プログラムの利用するメモリ使用量を削減し、状態爆発を低減することが可能である。
【００３７】
＜第２の実施形態＞
以下では、図５乃至図６Ｆを参照して、本発明の第２の実施形態について説明する。本実施形態は、配列の添え字が定数ではなく変数である場合について、モデル検証プログラム１１０としてＳＰＩＮを用いて、「配列外へのメモリアクセスは行ってはならない」などの性質についてのプログラム検証を行う場合について説明する。上記第１の実施形態では、テンプレートを適用する関数が検証式を調査するためのプログラム断片への到達性に関連するものであった。一方、本実施形態では、テンプレートを適用する関数の振る舞いが、検証式内の変数値に関連する場合で、関数の振る舞いが複数存在する場合について説明する。
【００３８】
＜プログラム例＞
図６を参照して、本実施形態で説明する被検証プログラムコード１０３と、モデル検証プログラム１１０としてＳＰＩＮを用いる場合の検証用プログラム１０９との一例について説明する。図６Ａは、Ｃ言語で記述された被検証プログラムコードと併記されたコメント文６０１中のテンプレート適用データを示す。
【００３９】
コメント文６０１中における、ＤａｔａＡｂｓｔｒｕｃｔｉｏｎタグはデータに対する振る舞いを抽象化した例を示す。ｎａｍｅＯｆＳｙｍｂｏｌタグは上記振る舞いを抽象化したデータの変数名称を示す。本実施形態では、ｎａｍｅＯｆＦｕｎｃタグの示す関数の振る舞いについて、テンプレートデータを用いて検証プログラムを生成する。
【００４０】
Ａｂｓｔｒｕｃｔｉｏｎタグは各々のテンプレートを示す。Ｃｏｎｄｉｔｉｏｎタグは条件文を意味し、ｖａｌｕｅタグはＣｏｎｄｉｔｉｏｎタグを満たす場合の値の定義式を記述する。１つ目のテンプレート適用データ（第１のテンプレート適用データ）は、条件式（（＿ｂ＆１）＝＝１）が真の場合にはｃａｌｃ＿ｂ関数の返し値がｂ集合要素のいずれかから２５６を引いた値である。一方、偽の場合にはｃａｌｃ＿ｂ関数の返し値がｂｂ集合要素のいずれかから２５６を引いた値であることを意味する。２つ目のテンプレート適用データ（第２のテンプレート適用データ）は、ｃａｌｃ＿ｂ関数の返し値がｂとｂｂの和集合の集合要素のいずれかから２５６を引いた値であることを意味する。
【００４１】
本実施形態ではＣ言語の図６Ａに示す被検証プログラムコードを一般的なコンパイラで、図６Ｂに示すように、３番地コード化した上でプログラム検証作業を行う。また、本実施形態では、図６Ｂのｍａｉｎ関数の５行目の配列アクセス（ｃ［Ｂ］＝（ｕｎｓｉｇｎｅｄ ｃｈａｒ）＿ｂ；）についての配列外参照について説明する。図６Ｃは、配列外参照についてプログラム検証プログラム１０１の作成した検証式データである。図６Ｄは、比較例となる検証プログラムを全て被検証プログラムコード１０３から作成した場合の検証プログラムを示す。図６Ｅは、図６Ａの被検証プログラムコードに併記されたコメント文６０１中に記述された第１のテンプレート適用データを元にして検証プログラムコードを生成したものである。図６Ｆは、第２のテンプレート適用データを元にして検証用プログラム１０９を生成したものである。
【００４２】
＜処理フロー＞
次に、図５Ａ及び図５Ｂを参照して、本実施形態のプログラム検証における処理フローについて説明する。以下で説明する処理は、中央処理装置（ＣＰＵ）２０６が、ハードディスク２０８に格納されたプログラム検証プログラム１０１を主記憶装置２０７に読み出して実行することにより実現される。図５Ａの５００は、プログラム検証の全体フローを示す。図５Ｂの５１０は、フローチャート５００内のＳ５０４のサブフローチャートを示す。図５Ｂの５２０は、フローチャート５００のＳ５０５内のサブフローチャートを示す。
【００４３】
Ｓ５０１、Ｓ５０２において、ＣＰＵ２０６は、図６Ａに示す被検証プログラムコード１０３と、テンプレート適用データ１０４とを読み出し、被検証プログラムコード１０３を解析する。途中、ＣＰＵ２０６は、図６Ｂのように３番地コード化して副作用動作プログラムコードを単一動作プログラムコードに変換し、検証式と行番号の対応を簡便化することが可能である。また、ＣＰＵ２０６は、図６Ａのコメント文６０１中に記述されるテンプレート適用データを解析し、テンプレートコード利用時の適用方法、即ち、２つのテンプレート適用データ（第１及び第２のテンプレート適用データ）を取得する。更に、ＣＰＵ２０６は、定数配列ｂとｂｂに対する記述を解析し、定数配列、即ちｂ集合の要素は２５８，２５７，２５５で要素数は３の集合であることを理解する。さらに、ｂｂ定数配列、即ちｂｂ集合の要素は、２５６，２５７，２５８で要素数が３の集合であることを理解することができる。
【００４４】
Ｓ５０３において、ＣＰＵ２０６は、図６Ｃに示す検証式リストを作成する。さらに、ＣＰＵ２０６は、検証式リストの番号に対応する各々の検証プログラムを作成する。そのため、検証式によって、ｍａｉｎ関数の５行目における変数Ｂについてコード縮小ブロック１０７を用いて被検証プログラムコード１０３の縮小化と必要最小限な被検証プログラムコード１０３の断片を取得する。ここで、検証式は、関数名と、行番号と、行番号における検証内容とを示すものである。その結果、変数Ｂはｃａｌｃ＿ｂ関数の返し値であり、ｃａｌｃ＿ｂ関数はｍａｉｎ関数から呼び出しされることを理解する。
【００４５】
Ｓ５０４において、ＣＰＵ２０６は、被検証プログラムコード使用判断ブロック１０５を用いて、被検証プログラムコード１０３を使用するか否かを判断する。被検証プログラムコード１０３を使用する場合はＳ５０６に進み、使用しない場合はＳ５０５に進む。ｍａｉｎ関数はテンプレート適用データに含まれておらず、且つ、ｃａｌｃ＿ｂ関数及びｃａｌｃ＿ｂ関数の返し値はテンプレート適用データに含まれている。なお、ｃａｌｃ＿ｂ関数の返し値は、Ｓ５０３で作成した図６Ｃに示す検証式内に含まれているため、Ｓ５０６に進む。
【００４６】
Ｓ５０６において、ＣＰＵ２０６は、コード縮小ブロック１０７を用いて、被検証プログラムコード１０３のみを用いて図６Ｃに示す検証を行うのに必要最小限な被検証プログラム断片を作成する。さらに、モデル検証プログラムの理解できる検証用プログラム１０９に変換する。その後、Ｓ５０８において、ＣＰＵ２０６は、動作制御ブロック１０２によって、検証用プログラム１０９をモデル検証プログラム１１０に入力して、Ｓ５０９で検証結果１１１を取得する。Ｓ５１０において、ＣＰＵ２０６は、モデル検証プログラム１１０を実行した検証結果１１１が、状態爆発を起こしたことを示すか否かを判定する。状態爆発を起こしていることを示す場合には、Ｓ５１１に進み、状態爆発を起こすことなく検証を終了することができたことを示す場合には、検証結果１１１をユーザーに表示してプログラム検証を終了する。Ｓ５１１において、ＣＰＵ２０６は、利用可能なテンプレート適用データがあるか否かを判定し、あればＳ５０５に進み、無ければ処理を終了する。
【００４７】
Ｓ５０５において、ＣＰＵ２０６は、動作制御ブロック１０２によって、テンプレート適用データ１０４の第１のテンプレートコードをテンプレートコード生成ブロック１０６に入力し、出力される検証用プログラム断片で検証用プログラム１０９を更新する。その後、Ｓ５０８に進み、上述したように、モデル検証プログラム１１０を実行し、Ｓ５０９で検証結果１１１を取得し、Ｓ５１０以降の処理を実行する。なお、モデル検証プログラム１１０を実行した際に状態爆発を発生し、結果を取得できない場合には、ＣＰＵ２０６は、Ｓ５１１においてＳ５０５から検証を再度行う。また、Ｓ５１１で既に適用可能なテンプレート適用データが存在しないと判定すると、ＣＰＵ２０６は、検証作業が終了しなかったことをユーザーに報知した上で、処理を終了する。
【００４８】
次に、図５Ｂのフローチャート５１０について説明する。フローチャート５１０はフローチャート５００のＳ５０４の詳細を示す。
【００４９】
まず、Ｓ５０４１において、ＣＰＵ２０６は、図６Ｃに示す検証式に関連する被検証プログラムコードを抽出する。続いて、Ｓ５０４２において、ＣＰＵ２０６は、Ｓ５０４１で抽出した被検証プログラムコードに図６Ｃに示す検証式が含まれるか否かを判定する。該当する検証式が含まれる場合はＳ５０４３に進み、含まれない場合はＳ５０４６に進む。
【００５０】
Ｓ５０４３において、ＣＰＵ２０６は、当該検証式が被検証プログラムの制御フローにのみ関連するものであるか否かを判定する。当該検証式が被検証プログラムの制御フローにのみ関連するものであれば、Ｓ５０４５に進み、そうでなければＳ５０４４に進む。Ｓ５０４４において、ＣＰＵ２０６は、プログラム検証が初回であるか否かを判定する。ここでの判定は、モデル検証プログラムを既に実行しているか否かを判定する。例えば、一度Ｓ５０８のモデル検証プログラムを実行して、Ｓ５１０で状態爆発が発生したと判断してテンプレートコードを生成してやり直した場合は、初回ではないと判定される。したがって、ＣＰＵ２０６は、Ｓ５０８でモデル検証プログラムを実行した場合に、実行回数等を保持しておくようにしてもよい。初回であればＳ５０４５に進み、初回でなければＳ５０４６に進む。
【００５１】
Ｓ５０４５において、ＣＰＵ２０６は、被検証プログラムコードを使用すると判断し、処理を終了する。一方、Ｓ５０４６において、ＣＰＵ２０６は、テンプレートコードを使用すると判断し、処理を終了する。
【００５２】
次に、図５Ｂのフローチャート５２０について説明する。フローチャート５２０はフローチャート５００のＳ５０５の詳細を示す。つまり、フローチャート５２０は、テンプレートコード生成ブロック１０６の処理に相当する。
【００５３】
Ｓ５０５１において、ＣＰＵ２０６は、利用するテンプレートを選択する。ここでは、例えば、第１のテンプレート適用データ又は第２のテンプレート適用データが選択される。なお、選択方法は、予め定めれた順で選択されてもよいし、ユーザーの指示に基づくようにしてもよい。続いて、Ｓ５０５２において、ＣＰＵ２０６は、出力変数名と、ビット長さとを記憶する。Ｓ５０５３において、ＣＰＵ２０６は、入力変数のビット長さを記憶する。Ｓ５０５４において、ＣＰＵ２０６は、出力変数の更新頻度（１０）を記憶する。Ｓ５０５５において、ＣＰＵ２０６は、プログラムコード（テンプレートコード）を出力する。出力されたテンプレートコードは、第１のテンプレート適用データを使用した場合、例えば、図６Ｅに示すコードとなる。一方、第２のテンプレート適用データを使用した場合は、図６Ｆに示すコードとなる。最後に、Ｓ５０５６において、ＣＰＵ２０６は、利用したテンプレートを記憶して処理を終了する。
【００５４】
本実施形態で示した図６Ａの被検証プログラムコード１０３は、実際には全て被検証プログラムコード１０３を用いても、検証プログラムは状態爆発を起こさずに配列外参照を指摘することができる。しかし、使用する状態ベクタ容量は、全ての検証プログラム断片を被検証プログラムコード１０３から作成した場合は４８バイトとなり、第１のテンプレート適用データ１０４を使用した場合が２０バイトとなった。また、第２のテンプレート適用データを使用した場合が１６バイトと大幅に削減できており、実際には様々に複雑化する、ユーザーの作成する被検証プログラムコード１０３を検証するために有効である。
【００５５】
以上説明したように、本実施形態に係る情報処理装置は、モデル検証プログラムの利用するメモリ使用量を削減し、状態爆発を低減することが可能である。
【００５６】
＜その他の実施形態＞
また、本発明は、以下の処理を実行することによっても実現される。即ち、上述した実施形態の機能を実現するソフトウェア（プログラム）を、ネットワーク又は各種記憶媒体を介してシステム或いは装置に供給し、そのシステム或いは装置のコンピュータ（又はＣＰＵやＭＰＵ等）がプログラムを読み出して実行する処理である。
【図１】
2015156053.tif 000003
【図２】
2015156053.tif 000004
【図３Ａ】
2015156053.tif 000005
【図３Ｂ】
2015156053.tif 000006
【図４Ａ】
2015156053.tif 000007
【図４Ｂ】
2015156053.tif 000008
【図４Ｃ】
2015156053.tif 000009
【図４Ｄ】
2015156053.tif 000010
【図４Ｅ】
2015156053.tif 000011
【図４Ｆ】
2015156053.tif 000012
【図５Ａ】
2015156053.tif 000013
【図５Ｂ】
2015156053.tif 000014
【図６Ａ】
2015156053.tif 000015
【図６Ｂ】
2015156053.tif 000016
【図６Ｃ】
2015156053.tif 000017
【図６Ｄ】
2015156053.tif 000018
【図６Ｅ】
2015156053.tif 000019
【図６Ｆ】
2015156053.tif 000020