(57)【要約】【課題】幅広いソフトウェアを検証することが可能なソフトウェア検証装置およびソフトウェア検証プログラムを提供する。【解決手段】検証対象の関数が含まれるソースコードを記憶するコード記憶部と、関数を検証するための検証コードを生成する検証コード生成部と、検証コードの挿入点を決定する挿入点決定部と、ソースコードの挿入点に検証コードを挿入する検証コード挿入部と、所定の繰り返し回数だけ関数を繰り返し実行する周期発生関数が含まれるソースコードを生成する周期発生関数生成部と、周期発生関数が含まれるソースコードと検証対象の関数が含まれるソースコードとを統合した統合ソースコードを生成するコード統合部と、統合ソースコードを当該統合ソースコードに含まれる検証コードに基づいて解析し、関数が取り得る状態を探索するモデル検査部と、を備えるソフトウェア検証装置。【選択図】図２
2013239008.tif 000002
【特許請求の範囲】
【請求項１】
検証対象の関数が含まれるソースコードを記憶するコード記憶部と、
前記関数を検証するための検証コードを生成する検証コード生成部と、
前記検証コードの挿入点を決定する挿入点決定部と、
前記ソースコードの前記挿入点に前記検証コードを挿入する検証コード挿入部と、
所定の繰り返し回数だけ前記関数を繰り返し実行する周期発生関数が含まれるソースコードを生成する周期発生関数生成部と、
前記周期発生関数が含まれるソースコードと前記検証対象の関数が含まれるソースコードとを統合した統合ソースコードを生成するコード統合部と、
前記統合ソースコードを当該統合ソースコードに含まれる前記検証コードに基づいて解析し、前記関数が取り得る状態を探索するモデル検査部と、
を備えることを特徴とするソフトウェア検証装置。
【請求項２】
請求項１に記載のソフトウェア検証装置において、
前記関数が取り得る状態には、大域変数の値と、所定のハードウェアからの出力値と、の少なくとも一方が含まれることを特徴とするソフトウェア検証装置。
【請求項３】
請求項２に記載のソフトウェア検証装置において、
前記検証コードは、前記関数が取り得る状態の範囲を限定するコードと、前記関数が取ることが期待される状態を示すコードと、の少なくとも一方を含むことを特徴とするソフトウェア検証装置。
【請求項４】
請求項３に記載のソフトウェア検証装置において、
前記関数の繰り返し回数と、前記関数への入力値の範囲と、の組を含む検証範囲情報が記憶される検証範囲情報記憶部を備え、
前記周期発生関数生成部は、前記検証範囲情報に含まれる繰り返し回数だけ前記関数を繰り返し実行する周期発生関数を生成し、
前記モデル検査部は、前記検証範囲情報に含まれる入力値の範囲に基づいて前記関数が取り得る状態を探索することを特徴とするソフトウェア検証装置。
【請求項５】
請求項４に記載のソフトウェア検証装置において、
前記検証範囲情報記憶部は、前記検証コードのパターンを表すパターン情報が含まれる前記検証範囲情報を記憶し、
前記検証コード生成部は、前記検証範囲情報に含まれる前記パターン情報に基づいて前記検証コードを生成することを特徴とするソフトウェア検証装置。
【請求項６】
請求項５に記載のソフトウェア検証装置において、
前記検証範囲情報記憶部は、前記検証コードの挿入位置を表す位置情報が含まれる前記検証範囲情報を記憶し、
前記検証コード挿入部は、前記位置情報により表される挿入位置に前記検証コードを挿入することを特徴とするソフトウェア検証装置。
【請求項７】
請求項１〜５のいずれか一項に記載のソフトウェア検証装置において、
前記コード記憶部は、前記検証コードの挿入位置を表す位置コードが含まれる前記ソースコードを記憶し、
前記検証コード挿入部は、前記位置コードにより表される挿入位置に前記検証コードを挿入することを特徴とするソフトウェア検証装置。
【請求項８】
検証対象の関数を含むソースコードをコンピュータに入力するコード入力工程と、
コンピュータが前記関数を検証するための検証コードを生成する検証コード生成工程と、
コンピュータが前記検証コードの挿入点を決定する挿入点決定工程と、
コンピュータが前記ソースコードの前記挿入点に前記検証コードを挿入する検証コード挿入工程と、
所定の繰り返し回数だけ前記関数を繰り返し実行する周期発生関数をコンピュータが生成する周期発生関数生成工程と、
前記周期発生関数と前記ソースコードとを統合した統合ソースコードをコンピュータが生成するコード統合工程と、
コンピュータが、前記統合ソースコードを当該統合ソースコードに含まれる前記検証コードに基づいて解析し、前記関数が取り得る状態を探索するモデル検査工程と、
をコンピュータに実行させることを特徴とするソフトウェア検証プログラム。
【請求項９】
請求項８に記載のソフトウェア検証プログラムにおいて、
前記関数が取り得る状態には、大域変数の値と、所定のハードウェアからの出力値と、の少なくとも一方が含まれることを特徴とするソフトウェア検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェア検証装置およびソフトウェア検証プログラムに関する。
【背景技術】
【０００２】
従来、ソフトウェアのソースコードのモデル検査技術が知られている。例えば特許文献１には、検証対象ソースコードをＫｒｉｐｋｅ構造モデルにモデル化し、そのＫｒｉｐｋｅ構造モデルに対してモデル検査を行うソースコード検証システムが記載されている。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２００９−２１１５０３号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
従来技術には、外部変数やハードウェア要因等による関数の内部状態の変化に対応していないため、繰り返し呼び出した場合に挙動が変化する関数を検証することができないという問題があった。
【課題を解決するための手段】
【０００５】
請求項１に記載のソフトウェア検証装置は、検証対象の関数が含まれるソースコードを記憶するコード記憶部と、前記関数を検証するための検証コードを生成する検証コード生成部と、前記検証コードの挿入点を決定する挿入点決定部と、前記ソースコードの前記挿入点に前記検証コードを挿入する検証コード挿入部と、所定の繰り返し回数だけ前記関数を繰り返し実行する周期発生関数が含まれるソースコードを生成する周期発生関数生成部と、前記周期発生関数が含まれるソースコードと前記検証対象の関数が含まれるソースコードとを統合した統合ソースコードを生成するコード統合部と、前記統合ソースコードを当該統合ソースコードに含まれる前記検証コードに基づいて解析し、前記関数が取り得る状態を探索するモデル検査部と、を備えることを特徴とする。
請求項８に記載のソフトウェア検証プログラムは、検証対象の関数を含むソースコードをコンピュータに入力するコード入力工程と、コンピュータが前記関数を検証するための検証コードを生成する検証コード生成工程と、コンピュータが前記検証コードの挿入点を決定する挿入点決定工程と、コンピュータが前記ソースコードの前記挿入点に前記検証コードを挿入する検証コード挿入工程と、所定の繰り返し回数だけ前記関数を繰り返し実行する周期発生関数をコンピュータが生成する周期発生関数生成工程と、前記周期発生関数と前記ソースコードとを統合した統合ソースコードをコンピュータが生成するコード統合工程と、コンピュータが、前記統合ソースコードを当該統合ソースコードに含まれる前記検証コードに基づいて解析し、前記関数が取り得る状態を探索するモデル検査工程と、をコンピュータに実行させることを特徴とする。
【発明の効果】
【０００６】
本発明によれば、幅広いソフトウェアを検証することができる。
【図面の簡単な説明】
【０００７】
【図１】本発明の第１の実施の形態に係るソフトウェア検証装置１の構成を示すブロック図である。
【図２】第１の実施の形態に係るソフトウェア検証プログラム５の構造とデータの流れを模式的に示す図である。
【図３】検証対象ソースコード５０１のプログラムの例である。
【図４】検証範囲情報５０２の例を示す図である。
【図５】検証コードの雛形群５０４の例を示す図である。
【図６】検証範囲情報５０２に基づいて生成される検証範囲限定コード５０５４および検証内容コード５０５５の例を示す図である。
【図７】検証コード生成部５０５が生成するヘッダファイル５０５１の例を示す図である。
【図８】検証コード生成部５０５により生成される、図７に例示したヘッダファイル５０５１を参照するためのプログラムコード５０５２の例を示す図である。
【図９】検証コード生成部５０５により生成される、図７に例示した変数v_adcを参照するためのプログラムコード５０５３の例を示す図である。
【図１０】検証コード挿入部５０３により生成された検証可能ソースコード５０８の例を示す図である。
【図１１】周期発生関数の雛形５０７の例を示す図である。
【図１２】周期発生関数生成部５１０により生成される、周期発生関数のヘッダファイル５１０１の例を示す図である。
【図１３】周期発生関数生成部５１０で作られるプログラムコード５１０２の例を示す図である。
【図１４】周期発生関数のソースコード５１０３の例を示す図である。
【図１５】演算装置３による検証結果５１３の表示装置９への表示例を示す図である。
【図１６】ソフトウェア検証プログラム５のフローチャートである。
【図１７】検証範囲情報の一例を示す図である。
【発明を実施するための形態】
【０００８】
（第１の実施の形態）
図１は、本発明の第１の実施の形態に係るソフトウェア検証装置１の構成を示すブロック図である。ソフトウェア検証装置１は、コンピュータ２と、例えばキーボードやマウス等の入力装置８と、例えば液晶ディスプレイ等の表示装置９から成る。本装置のユーザ（以下、単にユーザと称する）は、入力装置８を用いて、コンピュータ２に対し種々の指令を与える。コンピュータ２は、検証の結果等を表示装置９に表示する。
【０００９】
コンピュータ２は、演算装置（ＣＰＵ）３、固定ディスク装置等の外部記憶媒体４、メモリ（ＲＡＭ）６、および入出力回路７を備える。外部記憶媒体４には、予めソフトウェア検証プログラム５が格納されている。入出力回路７は、入力装置８から入力情報を取得し、表示装置９に出力情報を表示する。
【００１０】
図２は、第１の実施の形態に係るソフトウェア検証プログラム５の構造とデータの流れを模式的に示す図である。ソフトウェア検証プログラム５は、検証対象ソースコード５０１と検証範囲情報５０２が入力されると、検証結果５１３を出力するプログラムである。ソフトウェア検証プログラム５は、検証コード挿入部５０３、検証コードの雛形を複数備える検証コードの雛形群５０４、検証コード生成部５０５、ループ回数判別部５０６、周期発生関数の雛形５０７、検証可能ソースコード５０８、ソースコード統合部５０９、周期発生関数生成部５１０、ループあり検証可能ソースコード５１１、およびモデル検査部５１２から構成される。
【００１１】
コンピュータ２に入力された検証対象の関数を含むソースコードは、検証コード挿入部５０３およびループ回数判別部５０６に入力される。検証コード生成部５０５は、関数を検証するための検証コードを生成する。検証コード挿入部５０３は、検証コードの挿入点を決定し、ソースコードの挿入点に検証コードを挿入する。周期発生関数生成部５１０は、所定の繰り返し回数だけ検証対象の関数を繰り返し実行する周期発生関数が含まれるソースコードを生成する。ソースコード統合部５０９は、周期発生関数を含むソースコードと検証対象の関数を含むソースコードとを統合した統合ソースコードであるループあり検証可能ソースコード５１１を生成する。モデル検査部５１２は、統合ソースコードを当該統合ソースコードに含まれる検証コードに基づいて解析し、検証対象の関数が取り得る状態を探索する。
【００１２】
なお、図２では説明の都合上、ソフトウェア検証プログラム５を上述した各部から構成されるように図示しているが、本発明はこのような構成に限定されるものではない。例えば、図２で独立した機能部として図示した複数の機能部を、１つの機能部として構成してもよい。また、ある１つの機能部が有する機能を複数に分割し、他の機能部に割り当てることも可能である。
【００１３】
図３は、検証対象ソースコード５０１のプログラムの例である。図３の検証対象ソースコード５０１はＣ言語のソースコードであり、検証対象の関数である「getADC」という関数が含まれる。関数getADCは引数を取らない関数であり、一時変数として、「input」、「output」、「dif」、および「sign」と命名された４つの変数を用いる。なお、本実施形態で「関数」と称するものは、入力値や内部状態に基づく一群の処理をまとめたものを指し、これはサブルーチンやモジュール等と呼ばれることもある。
【００１４】
関数getADCは、引数および一時変数とは別に、「pre_input」と命名された外部変数と、「ADC」と命名されたレジスタを用いる。外部変数（大域変数）pre_inputは、１５行目、１６行目、１９行目、および２８行目において参照され、２９行目において更新される。また、レジスタADCは１２行目において参照される。ここでレジスタADCは、外部ハードウェアのレジスタ等の外部リソースを参照するものであり、例えばＣ言語のマクロ機能によって、「*(unsigned char *)0x100」のように、特定のメモリアドレス（上記の例では0x100番地）を直接参照するような定義がなされている。すなわち、検証対象ソースコード５０１が動作対象とするマイコンには、何らかのハードウェアデバイスが接続されており、そのハードウェアデバイスの有するレジスタが当該コンピュータのメモリアドレス空間内の所定番地に割り当てられている。ADCはこの番地に対応付けられており、ADCの読み書きはこの番地の読み書きすなわちレジスタの読み書きに等しい。この番地から読み出されるレジスタの値は、関数getADC自身がADCを書き換えていないにも関わらず、当該ハードウェアデバイスの動作に応じて変化しうる。
【００１５】
以上のように、検証対象ソースコード５０１に含まれる関数getADCは、実行される度に、外部変数や特定のメモリアドレスを参照および更新する。従って、引数を取らないにも関わらず、繰り返し呼び出した場合にその戻り値が変化する可能性がある。換言すれば、関数getADCは複数の状態（外部変数pre_inputが0の状態、外部変数pre_inputが1の状態、等）を取り得る。
【００１６】
検証対象ソースコード５０１には、Ｃ言語のコメントの形で、後述する検証コードの挿入点が記載されている。本実施形態では、１０行目、１１行目、１３行目、および２６行目のように、「// insert_point_」という記述で始まるコメントを、挿入点として扱う。詳細は後述するが、検証コードにはassumeとassertの２種類が存在するので、挿入点も検証コードに対応する２種類が存在する。１０行目および１１行目の挿入点はassumeに対応する挿入点であり、１３行目および２６行目の挿入点はassertに対応する挿入点である。
【００１７】
検証対象ソースコード５０１には更に、後述するヘッダファイルおよび変数定義用の挿入点が記載されている。本実施形態では、「// insert_point_header」という記述をヘッダファイルの挿入点として扱い、「// variable_definition」という記述を変数定義の挿入点として扱う。検証対象ソースコード５０１の１行目にはヘッダファイルの挿入点が、８行目には変数定義の挿入点が、それぞれ記載されている。
【００１８】
図４は、検証範囲情報５０２の例を示す図である。検証範囲情報５０２は行を識別するためのＮｏ５０２１、検証対象の関数を示す検証関数５０２２、検証対象ソースコード５０１への挿入箇所を識別可能な挿入点５０２３、検証する内容を識別可能な検証パターン５０２４、検証関数５０２２を実行する回数を識別可能なループ回数５０２５、検証する範囲を識別可能な検証範囲５０２６、検証範囲５０２６において期待する値を示す期待値５０２７からなる。
【００１９】
図５は、検証コードの雛形群５０４の例を示す図である。検証コードの雛形群５０４は、検証コードの雛形を複数有している。個々の雛形は、検証範囲を指定する検証範囲限定コードassumeと、検証したい内容を指定する検証内容コードassertとを含んでいる。検証コードの雛形群５０４では、１つ以上の雛形がグループ化されており、それら個々のグループには、検証パターンと称する、グループごとに一意な番号が割り当てられている。この番号は、図４に示した検証範囲情報５０２の検証パターン５０２４に対応している。
【００２０】
検証範囲限定コードassumeは、検証対象の関数getADCが利用する変数の値を特定の範囲に限定することにより、関数getADCの検証範囲を指定する。例えば、検証範囲限定コードassumeにより、変数ADCを100以上200以下の範囲に限定すれば、モデル検査部５１２は変数ADCが0や250など、この範囲から外れることがないと仮定して検証を行う。すなわち、モデル検査部５１２は、検証範囲限定コードassumeで指定された範囲の状態のみを探索する。換言すれば、検証範囲限定コードassumeは、検証対象の関数が取り得る状態の範囲を限定するコードである。
【００２１】
検証内容コードassertは、検証対象の関数getADCの特定地点において、特定の変数が取るべき値（条件）を指定するコードである。例えば、検証内容コードassertにより、変数difが5以下である、という条件を指定すれば、モデル検査部５１２は変数difが10や20など、この範囲から外れた値になることがあるか否かを検証する。換言すれば、検証内容コードassertは、検証対象の関数が取ることが期待される状態を示すコードである。
【００２２】
図５では、検証コードの雛形群５０４には、１番の検証パターンのグループのみが含まれている。このグループは、雛形５０４１と雛形５０４２をグループ化したものである。検証コードの雛形５０４１は、検証範囲限定コード５０４１１と検証内容コード５０４１２から成る。また、検証コードの雛形５０４２は、検証範囲限定コード５０４２１と検証内容コード５０４２２から成る。
【００２３】
検証コード生成部５０５は、検証範囲情報５０２が入力されると、検証コードの雛形群５０４から雛形のグループ（検証パターン）を選択する。例えば図４に示すように、検証パターン５０２４が１となっている検証範囲情報５０２が入力された場合には、図５に示した検証コードの雛形５０４１、５０４２を選択する。次に検証コード生成部５０５は、入力された検証範囲情報５０２から、検証コードが挿入される挿入点を特定する。例えば図４に示すように、挿入点５０２３が１となっている場合には、選択した雛形５０４１、５０４２から、１番の挿入点に対応する雛形５０４１を選択する（雛形５０４２は選択しない）。そして、ここで選択された雛形５０４１から、実際に挿入される検証コードを生成する。
【００２４】
図６は、検証範囲情報５０２に基づいて生成される検証範囲限定コード５０５４および検証内容コード５０５５の例を示す図である。図６に示すように、選択された検証コードの雛形５０４１に含まれる検証範囲限定コード５０４１１からは検証範囲限定コード５０５４が、検証内容コード５０４１２からは検証内容コード５０５５が、それぞれ作成される。検証範囲限定コード５０５４は、検証範囲限定コード５０４１１の括弧内の「lower」および「upper」を、検証範囲情報５０２の検証範囲５０２６に基づいて書き換えたコードである。同様に、検証内容コード５０５５は、検証内容コード５０４１２の括弧内の「expected」を、検証範囲情報５０２の期待値５０２７に基づいて書き換えたコードである。
【００２５】
検証コード生成部５０５は更に、上述したレジスタADCを検証するために必要な検証コードを生成する。以下、検証コード生成部５０５により生成される他の検証コードについて説明する。
【００２６】
図７は、検証コード生成部５０５が生成するヘッダファイル５０５１の例を示す図である。図７に示したヘッダファイルv_ADC.hは、検証対象ソースコード５０１が外部リソース（例えば外部ハードウェアのレジスタ）を参照している部分を、新しく定義した変数に切り替えるために用いられる。例えば、図３に示した検証対象ソースコード５０１は、１２行目において、外部ハードウェアのレジスタに対応するメモリADCを参照している。しかしながら、モデル検査部５１２は、上述のADCのように、特定のメモリアドレスを直接参照する記述を認識できない。そこで、検証コード生成部５０５は、Ｃ言語のマクロ命令#defineを用いて、ADCを別途用意した変数v_adcに置換している。これにより、マイコン上で動作するプログラムをモデル検査で検証可能となる。
【００２７】
図８は、検証コード生成部５０５により生成される、図７に例示したヘッダファイル５０５１を参照するためのプログラムコード５０５２の例を示す図である。検証コード挿入部５０３は、このプログラムコード５０５２を、検証対象ソースコード５０１に用意されたヘッダファイルの挿入点に挿入することにより、検証対象ソースコード５０１におけるメモリADCへの参照を、別途用意した変数v_adcへの参照に置き換える。
【００２８】
図９は、検証コード生成部５０５により生成される、図７に例示した変数v_adcを参照するためのプログラムコード５０５３の例を示す図である。検証コード挿入部５０３は、このプログラムコード５０５２を、検証対象ソースコード５０１に用意された変数定義の挿入点に挿入することにより、検証対象の関数getADC内に一時変数v_adcを用意する。これにより、検証対象ソースコード５０１におけるメモリADCへの参照は、この一時変数v_adcへの参照に置き換えられることになる。
【００２９】
検証コード生成部５０５が生成した以上のコードは、検証コード挿入部５０３に出力される。検証コード挿入部５０３は、検証対象ソースコード５０１に予め記載されている挿入点の位置に、検証コード生成部５０５により生成された各検証コードを挿入し、検証可能ソースコード５０８を生成する。
【００３０】
図１０は、検証コード挿入部５０３により生成された検証可能ソースコード５０８の例を示す図である。図１０に示した検証可能ソースコード５０８は、検証対象ソースコード５０１（図３）の１行目をプログラムコード５０５２（図８）に、８行目をプログラムコード５０５３（図９）に、１０行目を検証範囲限定コード５０５４（図６）に、２６行目を検証内容コード５０５５（図６）にそれぞれ変更したソースコードである。なお、入力された検証範囲情報５０２で指定されたなかった挿入点２（１１行目および１３行目）は、元の検証対象ソースコード５０１のままである。
【００３１】
次に、ループ回数判別部５０６および周期発生関数生成部５１０について説明する。ソフトウェア検証プログラム５に入力された検証範囲情報５０２は、上述した検証コード生成部５０５とは別に、ループ回数判別部５０６にも入力される。ループ回数判別部５０６は検証範囲情報５０２から、ループ回数５０２５と検証関数５０２２を抽出して周期発生関数生成部５１０に引き渡すことにより、ループ回数を判別する。周期発生関数生成部５１０は、ループ回数判別部５０６から引き渡されたこれらの情報と、予め用意されている周期発生関数の雛形５０７とに基づいて、周期発生関数のソースコードを生成する。
【００３２】
図１１は、周期発生関数の雛形５０７の例を示す図である。周期発生関数の雛形５０７は、所定のループをLOOP_MAX回だけ回す、すなわち、所定の命令をLOOP_MAX回だけ繰り返すプログラムとなっている。ループの中身に相当する位置（６行目）には、検証対象の関数の挿入点を示す「// target_function」というコメントが記述されている。また、１行目には、周期発生関数生成部５１０により生成されるヘッダファイルを取り込む旨が記述されている。
【００３３】
図１２は、周期発生関数生成部５１０により生成される、周期発生関数のヘッダファイル５１０１の例を示す図である。周期発生関数生成部５１０は、ループ回数判別部５０６から引き渡されたループ回数５０２５に基づいて、このヘッダファイル５１０１に、ループ回数を表すLOOP_MAXの定義を行う。図４に示した検証範囲情報５０２では、ループ回数５０２５は「２」となっているため、図１２ではLOOP_MAXが「２」と定義されている。
【００３４】
ヘッダファイル５１０１には更に、検証対象の関数の宣言（１行目）と、検証対象の関数の戻り値を受けとるための変数の定義（２行目）が為されている。図４に示した検証範囲情報５０２では、検証関数５０２２は「unsigned char getADC」であるので、図１２ではこれに準じた関数宣言が記載されている。また、戻り値を受けとるための変数の型「unsigned char」も、この検証関数５０２２から決定することができる。
【００３５】
図１３は、周期発生関数生成部５１０で作られるプログラムコード５１０２の例を示す図である。このプログラムコード５１０２は、上述した検証対象の関数を呼び出し、戻り値を上述の変数で受け取るコードである。周期発生関数生成部５１０は、このプログラムコード５１０２を、周期発生関数の雛形５０７に記載された挿入点に挿入することにより、検証対象の関数を繰り返し呼び出すプログラムコードを生成する。
【００３６】
図１４は、周期発生関数のソースコード５１０３の例を示す図である。周期発生関数のソースコード５１０３は、周期発生関数の雛形５０７（図１１）の６行目に、プログラムコード５１０２（図１３）を挿入したソースコードである。周期発生関数生成部５１０は、図１４に示したソースコード５１０３と、図１２に示したヘッダファイル５１０１を生成し、ソースコード統合部５０９に出力する。
【００３７】
ソースコード統合部５０９は、検証コード挿入部５０３により出力された検証可能ソースコード５０８（および図７に示したヘッダファイル５０５１）と、周期発生関数生成部５１０により出力されたソースコード５１０３（および図１２に示したヘッダファイル５１０１）とを統合した、ループあり検証可能ソースコード（統合ソースコード）５１１を生成してモデル検査部５１２に出力する。モデル検査部５１２は、周知の方法によりこのループあり検証可能ソースコード５１１を解析し、検証対象の関数getADCが取り得る状態を探索する。そして、その結果を検証結果５１３として出力する。モデル検査部５１２には、例えばＣＢＭＣ等の既存のソフトウェアを利用することが可能である。
【００３８】
図１５は、演算装置３による検証結果５１３の表示装置９への表示例を示す図である。解析の結果、検証内容コード５０５５（図６）で指定した条件が満たされないケースが明らかになると、モデル検査部５１２は検証内容コード５０５５で指定した文字列を検証結果５１３として出力する。図１５では、検証内容コード５０５５で指定した「invalid」という文字列が表示装置９に表示されている。すなわち、関数getADCを繰り返し呼び出した場合、検証内容コード５０５５で指定した条件が満たされなくなることがある、ということである。
【００３９】
図１６は、ソフトウェア検証プログラム５のフローチャートである。前述の通り、ソフトウェア検証プログラム５は外部記憶媒体４に予め格納されている。演算装置３は、外部記憶媒体４からソフトウェア検証プログラム５を読み出して実行することにより、図１６に示す処理が実行される。以下、図２に示すブロック図に基づいてソフトウェア検証プログラム５の流れを説明する。なお、図２に示すブロック図を構成する各機能部は、実際にはソフトウェア検証プログラム５を実行する演算装置３により実現される。つまり、図１６のフローチャートに示す各処理は、実際には演算装置３が実行する処理である。
【００４０】
まずステップＳ０１では、検証コード挿入部５０３が、検証対象ソースコード５０１の入力を受け付ける。ユーザは、例えば入力装置８から検証対象ソースコード５０１を直接入力したり、あるいは外部記憶媒体４などに予め記憶されているソースコードを指定し、そのソースコードを検証対象ソースコード５０１とする指令を演算装置３に入力したりする。検証コード挿入部５０３は、ユーザによるこれらの操作に応じて、検証対象ソースコード５０１の入力を受け付ける。入力された検証対象ソースコード５０１は、メモリ６に一時的に記憶される。
【００４１】
ステップＳ０２では、検証コード生成部５０５およびループ回数判別部５０６が、検証範囲情報５０２の入力を受け付ける。検証範囲情報５０２の入力の方法は、ステップＳ０１における検証対象ソースコード５０１の入力と同様である。ステップＳ０４では、検証コード生成部５０５が、入力された検証範囲情報５０２から使用する検証コードの雛形を識別し、検証コードを生成する。例えば、検証範囲情報５０２のＮｏ５０２１が１の行である場合、検証パターン５０２４に基づいて、検証コードの雛形５０４１を選択する。そして、検証範囲５０２６に基づいて検証範囲限定コードの雛形５０４１１を埋めることで検証範囲限定コード５０５４を生成する。更に、期待値５０２７に基づいて検証内容コードの雛形５０４１２を埋めることで、検証内容コード５０５５を生成する。最後に、検証関数５０２２の関数の戻り値のデータ型と検証範囲５０２６に記載の変数名に基づいてヘッダファイル５０５１とプログラムコード５０５３を生成し、検証範囲５０２６の変数名に基づいてプログラムコード５０５２を生成する。
【００４２】
ステップＳ０５では、検証コード挿入部５０３が、検証対象ソースコード５０１の１行目にプログラムコード５０５２を、８行目にプログラムコード５０５３をそれぞれ挿入する。更に、挿入点５０２３に基づいて検証コードを挿入する。例えば、挿入点５０２３の番号が１であるとき、その番号に対応する検証対象ソースコード５０１の１０行目に検証範囲限定コード５０５４を挿入し、２６行目に検証内容コード５０５５を挿入することで、検証可能ソースコード５０８を生成する。
【００４３】
ステップＳ０６では、ループ回数判別部５０６が、入力された検証範囲情報５０２からループ回数とループさせる検証対象の関数の関数名および戻り値のデータ型とを識別する。例えば、検証範囲情報５０２のループ回数５０２５からループ回数を識別する。ステップＳ０７では、周期発生関数生成部５１０が、識別されたループ回数と識別された検証対数の関数の関数名および戻り値のデータ型とに基づいて、ヘッダファイル５１０１を生成する。また、識別された検証対象の関数の関数名および戻り値のデータ型に基づいて、周期発生関数の雛形５０７の６行目にプログラムコード５１０２を挿入し、周期発生関数５１０３を生成する。なお、検証対象の関数の戻り値のデータ型と関数名を識別しないで、検証コード生成部５０５からこれらの情報を取得しても良い。
【００４４】
ステップＳ０８では、ソースコード統合部５０９が、検証可能ソースコード５０８、ヘッダファイル５０５１、周期発生関数５１０３、およびヘッダファイル５１０１を一つのグループとした、ループあり検証可能ソースコード（統合ソースコード）５１１を生成する。ステップＳ０９では、モデル検査部５１２が、ループあり検証可能ソースコード５１１を入力として周期発生関数を始点としたモデル検査を行う。ステップＳ１０では、モデル検査部５１２が、検証結果５１３を検証者に通知する。例えば、表示装置９に検証結果５１３を表示する。ここでユーザは、検証結果５１３を確認することができる。例えば、表示装置９に表示された検証結果５１３を確認する。
【００４５】
上述した第１の実施の形態によるソフトウェア検証装置によれば、次の作用効果が得られる。
（１）検証コード生成部５０５は、関数を検証するための検証コードを生成する。検証コード挿入部５０３は、検証対象ソースコード５０１の記述から検証コードの挿入点を決定し、挿入点に検証コードを挿入する。周期発生関数生成部５１０は、所定の繰り返し回数だけ関数を繰り返し実行する周期発生関数を生成する。ソースコード統合部５０９は、周期発生関数と検証可能ソースコード５０８とを統合した統合ソースコードを生成する。モデル検査部５１２は、統合されたループ有り検証可能ソースコード５１１を検証コードに基づいて解析し、関数が取り得る状態を探索する。このようにしたので、繰り返し呼び出したときに内部状態が変化する関数をも検証対象とすることができ、幅広いソフトウェアを検証することができる。
【００４６】
（２）検証コードは、関数が取り得る状態の範囲を限定するコードassumeと、関数が取ることが期待される状態を示すコードassertとを含む。このようにしたので、検証に必要な演算量を削減することができる。また、ソフトウェアの作成者がどのような入力を想定し、どのような結果を期待しているのかを明確にすることができる。
【００４７】
（３）メモリ６には、関数の繰り返し回数（ループ回数５０２５）と、関数への入力値の範囲（検証範囲５０２６）と、の組を含む検証範囲情報が一時的に記憶される。周期発生関数生成部５１０は、検証範囲情報に含まれる繰り返し回数だけ関数を繰り返し実行する周期発生関数を生成し、モデル検査部５１２は、検証範囲情報に含まれる入力値の範囲に基づいて関数が取り得る状態を探索する。このようにしたので、繰り返し回数および入力値の範囲の設定の切替が容易になる。また、それらの組を多数用意しておくことで、多数の組み合わせに対する検査を一括で行うことも可能になる
【００４８】
（４）関数が取り得る状態には、外部変数（大域変数）の値と、所定のハードウェアからの出力値（レジスタ等）と、が少なくとも含まれる。このようにしたので、従来のソフトウェア検査技術では検査することができなかった、例えば前回呼び出し時に外部変数に記憶しておいた値や、外部ハードウェアであるタイマ等により計測された経過時間に基づいて異常を検出する安全機能を備えたソフトウェアについても、ソースコードの不具合をモデル検査で検出することが可能になる。
【００４９】
（５）メモリ６に記憶される検証範囲情報には、検証コードのパターンを表すパターン情報である検証パターン５０２４が含まれる。検証コード生成部５０５は、この検証パターン５０２４に基づいて検証コードを生成する。このようにしたので、検証コードの種々のバリエーションに対応することができ、より精緻な検査が可能になる。
【００５０】
（６）メモリ６に記憶される検証範囲情報には、検証コードの挿入位置を表す位置情報である挿入点５０２３が含まれる。検証コード挿入部５０３は、挿入点５０２３により表される挿入位置に検証コードを挿入する。このようにしたので、検証の度に挿入点を指定する必要が無い。また、予め複数の挿入点を用意しておき、それらを必要に応じて切り替えることも可能になる。
【００５１】
（７）メモリ６に格納される検証対象ソースコード５０１には、検証コードの挿入位置を表す挿入点がＣ言語のコメントの形で含まれている。検証コード挿入部５０３は、検証対象ソースコード５０１に記載されている挿入位置に検証コードを挿入する。このようにしたので、検証の度に挿入点を指定する必要が無い。
【００５２】
次のような変形も本発明の範囲内であり、変形例の一つ、もしくは複数を上述の実施形態と組み合わせることも可能である。
【００５３】
（変形例１）
上述した実施形態では、検証コードの挿入位置は予め検証対象ソースコード５０１に記載されていた。本発明はこのような実施形態に限定されない。例えば、検証の都度、ユーザが入力装置８から挿入点を指定するようにしてもよい。周期発生関数の雛形５０７についても同様に、関数呼び出しを挿入する位置をユーザが指定するようにしてよい。
【００５４】
（変形例２）
上述した実施の形態において示した検証範囲情報５０２は一例であり、これ以外の形式の検証範囲情報５０２についても本発明を適用可能である。例えば、検証範囲情報５０２の数は２つ以上であってもよい。また、検証対象の関数に関する情報は、必ずしも検証範囲情報５０２に含める必要は無い。例えば、検証コード挿入部５０３が検証対象ソースコード５０１を分析し、検証対象の関数名を取得するようにしてもよい。また、期待値５０２７についても、必ずしも検証範囲情報５０２に含める必要は無い。例えば、期待値が既に検証対象ソースコード５０１に埋め込まれてコメントアウトされた状態で、挿入点５０２３で指定されたときにコメントアウトが外されるようにすることができる。また、第１の実施の形態では、検証範囲情報５０２の検証範囲５０２６に、検証対象ソースコード５０１に記載されている変数名を記述しているが、検証範囲のみを記述するようにしてもよい。
【００５５】
（変形例３）
図１７は、検証範囲情報の一例を示す図である。図１７に例示した検証範囲情報７０２には、図４に示した検証範囲情報５０２と比べ、ループ回数を含んでいない。このように、検証範囲情報は必ずしも図４に示した形でなくてもよい。ここでは、検証パターン７０２４およびループ回数７０３２を含む設定済み検証範囲情報７０３を予めソフトウェア検証装置１に設定しておき、ソフトウェアの検証を行う際に入力する検証範囲情報７０２のデータ量を減らした例を示している。演算装置３は、検証パターン７０２４を利用して、設定済み検証範囲情報７０３のループ回数７０３２を調べることが可能である。
【００５６】
また、上述した第１の実施の形態では、検証範囲情報５０２の検証範囲５０２６は、特定の変数の値が上限値と下限値の間であることを指定する内容となっていた。検証範囲５０２６の内容は、特定の変数の値を限定するような内容であればこれに限らず、どのようなものであってもよい。例えば、上限値と下限値のいずれか一方のみを指定するものであってもよいし、その変数の値が所定の値と等しいことを限定したり、逆に等しくないことを限定したりするものであってもよい。
【００５７】
（変形例４）
上述した第１の実施の形態で示した変数名、ファイル名等は全て一例であり、上述したものと異なっていてよい。また、ヘッダファイルの内容やプログラムコードについても、上述した第１の実施の形態で示したものと異なっていてよい。例えば、ヘッダファイル５１０１の２行目は、検証対象の関数が戻り値を必要としない場合にはなくてもかまわない。また、プログラムコード５１０２の１行目は、検証対象の関数が戻り値を必要としない場合には左辺に代入する形で記述しないでよい。
【００５８】
（変形例５）
上述した各実施形態では、本発明をＣ言語で書かれたソースコードの検査プログラムに適用した例を説明した。本発明はこのような実施の形態に限定されず、他の言語で書かれたソースコードを検査する装置やプログラムに本発明を適用することも可能である。
【００５９】
本発明の特徴を損なわない限り、本発明は上記実施の形態に限定されるものではなく、本発明の技術的思想の範囲内で考えられるその他の形態についても、本発明の範囲内に含まれる。
【符号の説明】
【００６０】
１…ソフトウェア検証装置、２…コンピュータ、３…演算装置、４…外部記憶媒体、５…ソフトウェア検証プログラム、６…メモリ、７…入出力回路、８…入力装置、９…表示装置、５０３…検証コード挿入部、５０５…検証コード生成部、５０６…ループ回数判定部、５０６…ループ回数判別部、５０９…ソースコード統合部、５１０…周期発生関数生成部、５１２…モデル検査部
【図１】
2013239008.tif 000003
【図２】
2013239008.tif 000004
【図３】
2013239008.tif 000005
【図４】
2013239008.tif 000006
【図５】
2013239008.tif 000007
【図６】
2013239008.tif 000008
【図７】
2013239008.tif 000009
【図８】
2013239008.tif 000010
【図９】
2013239008.tif 000011
【図１０】
2013239008.tif 000012
【図１１】
2013239008.tif 000013
【図１２】
2013239008.tif 000014
【図１３】
2013239008.tif 000015
【図１４】
2013239008.tif 000016
【図１５】
2013239008.tif 000017
【図１６】
2013239008.tif 000018
【図１７】
2013239008.tif 000019