(57)【特許請求の範囲】
【請求項１】
ソフトウェアプログラムの動作を定義するソースコード群を入力するステップと、検査条件を入力するステップと、上記ソフトウェアプログラムが満たすべき性質を入力するステップを有し、上記ソフトウェアプログラムが上記検査条件の下で性質を満たすか否かを検査するソースコード検査方法であって、上記ソースコード群を動作仕様情報に変換するステップと、上記動作仕様情報の一部を検査対象範囲として選択するステップと、該検査対象範囲に対して検査を実行するステップと、該検査において該検査対象範囲を逸脱するケースがあることが示された場合に該検査対象範囲を拡大するステップを有し、逸脱がなくなるまでかかる検査と該検査対象範囲の拡大を繰り返すことを特徴とするソースコード検査方法。
【請求項２】
請求項１に記載のソースコード検査方法であって、上記ソフトウェアプログラムが満たすべき性質を入力する代わりに、あらかじめ定義された性質を検査することを特徴とするソースコード検査方法。
【請求項３】
請求項１または請求項２に記載のソースコード検査方法であって、上記検査対象範囲に対して検査を実行するステップとして、モデル検査プログラムを利用するソースコード検査方法。
【請求項４】
請求項１から３のいずれかに記載のソースコード検査方法であって、最初の検査対象範囲の選択に、モデル検査プログラムによる１度以上のシミュレーション実行の結果を用いることを特徴とするソースコード検査方法。
【請求項５】
請求項１から３のいずれかに記載のソースコード検査方法であって、最初の検査対象範囲の選択に、ソースコードによって定義されるソフトウェアプログラムの１度以上の実行の結果を用いることを特徴とするソースコード検査方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェアのソースコードの検査に関するものである。
【背景技術】
【０００２】
システムの振舞い（動作）、特に、システムを構成する複数の動作主体（例えば、複数の動作を実行する複数の機構からなる装置において、１つの動作を実行する機構の組み合わせが１つの動作主体であり、このように、複数の動作を実行する場合には、複数の動作主体がある）が事象のやり取りを介して連携しつつ、並行、並列に動作することによるシステムの振舞いは複雑である。このような分野の典型的なシステムとしては、ネットワークを介して通信プロトコルシステムや並行動作するハードウェア（装置など）をソフトウェアが制御する組込みシステムがある。このようなシステムでの各動作主体は、事象の同期的なやり取りのほかは独立して動作する。そのため、複数の動作主体間の事象のやり取りの内容によってシステムの振舞いが決定するだけでなく、やり取りの順序やタイミングにより、システムの振舞いが変化し得る。
【０００３】
このようなシステムを開発する場合には、各動作主体の動作を定義した動作仕様書を作成し、これを検査することが一般に行なわれる。各動作主体の動作の定義には、状態遷移モデルやシーケンス図，ＵＭＬなどが用いられる。システムの動作時における、事象のやり取りの内容、各動作主体間のやり取りの順序やタイミングの組み合わせが膨大となり、可能なシステムの振舞いが多数存在する。
【０００４】
システムの可能な振舞いを網羅的かつ自動的に分析する技術として、モデル検査技術が知られている。かかるモデル検査技術とは、予めシステムを構成する動作主体の動作仕様情報を専用言語で記述し、これとは別に、ソフトウェアプログラムが満たすべき性質情報を数学的な記法を用いて記述し、この動作仕様情報がこの性質情報を満たしているか否かを数学的に検査する技術である。モデル検査を実行するプログラムをモデル検査プログラムということにする。かかるモデル検査技術を実装した代表的なモデル検査プログラムとしては、ＳＰＩＮ（Ｓｉｍｐｌｅ  Ｐｒｏｍｅｌａ  Ｉｎｔｅｒｐｒｅｔｅｒ）（例えば、非特許文献１及び非特許文献２参照）やＳＭＶ（Ｓｙｍｂｏｌｉｃ  Ｍｏｄｅｌ  Ｃｈｅｃｋｅｒ）（例えば、非特許文献３参照），ＵＰＰＡＡＬ（例えば、非特許文献４参照）などが知られている。また、動作主体の動作仕様情報を記述する専用言語としては、例えば、ＳＰＩＮで用いられるＰｒｏｍｅｌａ（Ｐｒｏｔｏｃｏｌ  Ｍｅｔａ  Ｌａｎｇｕａｇｅ）がある。
【０００５】
モデル検査プログラムは、動作主体の動作仕様情報が性質情報を満たさない状態に至ることがある場合、その性質情報を満たさない状態に至るソフトウェアプログラムの動作過程を出力する。このように、モデル検査プログラムが出力する性質情報を満たさない状態に至るソフトウェアプログラムの動作過程を反例という。
【０００６】
モデル検査プログラムは、並行、並列に動作する複数の動作主体からなるシステムの可能な振舞いを網羅的に探索するものであることから、大規模なシステムの振舞いを検査する場合には、時間と計算機の記憶領域を大量に必要とするという課題がある。
【０００７】
モデル検査プログラムが要する時間と計算機の記憶領域の量は，検査の対象となる動作仕様情報で定義された動作主体の状態の量に依存することが，知られている。ここで，動作主体の状態とは、動作仕様情報に定義された変数の値と、動作仕様情報の動作中の位置（例えば、Ｐｒｏｍｅｌａで定義された動作仕様情報の文）の組合せで決定する、動作主体の動作状況を特定する情報である。さらに、複数の動作主体が並行、並列に動作するシステムの場合には、各動作主体の状態の組合せが、システム全体の状態となる。このように状態の量は組合せで決定するため、変数の取りうる値の量と、動作仕様情報の量が増えると、状態の量が急速に増大する。
【０００８】
かかる課題を解決するために、各モデル検査プログラムでは、探索を効率的に行なう技術が開発されている。その一例として、モデル検査プログラムの１つであるＳＰＩＮでは、計算機のＣＰＵのマルチコアに対応し、探索を分割して処理することで探索効率を向上させる技術が知られている（例えば、非特許文献２参照）。他の例としては、ＳＭＶでＢＤＤ（Ｂｉｎａｒｙ  Ｄｅｃｉｓｉｏｎ  Ｄｉａｇｒａｍ）とＳＡＴ（ＳＡＴｉｓｆｉａｂｉｌｉｔｙ  Ｐｒｏｂｒｅｍ）ソルバと呼ばれる技術を用いて探索効率の向上をはかるようにした技術も知られている（例えば、非特許文献３参照）。これらは、モデル検査のアルゴリズムの改良により、課題を解決するものである。
【０００９】
かかるモデル検査技術は、専用言語で記述したシステムを構成する動作主体の動作仕様情報を定義するが、ソフトウェアプログラムの動作仕様を定義するものとして、ソースコードがある。ソースコードは、プログラム言語を用いて記述する。代表的なプログラム言語としては、Ｃ言語やＪａｖａ言語がある。ここで、プログラム言語で記述されたソースコードを、モデル検査技術で用いる専用言語で記述した動作仕様情報に変換し、モデル検査プログラムを用いてソフトウェアプログラムを検査する技術がある（例えば、特許文献１参照）。本明細書においては、かかる技術を「ソースコード変換モデル検査」と総称する。
【００１０】
かかるソースコード変換モデル検査においても、前記の時間と計算機の記憶領域を大量に必要とするという問題がある。前記のモデル検査のアルゴリズムの改良による課題の解決のほかに、モデル検査プログラムの利用方法を改良して探索を効率的に行う技術が開発されている。
【００１１】
その一例として、検査対象たるソフトウェアプログラムを実行し、該ソフトウェアプログラムのソースコードのうち、かかる実行において処理された部分のみに検査範囲を限定する技術がある（例えば、特許文献２）。しかし，ソフトウェアプログラムのかかる実行で処理されなかった部分が，別の実行時には処理される可能性があり，検査範囲が過剰に限定される可能性がある。
【００１２】
他の例としては、ソースコードを静的解析し、かかる静的解析によって問題がある可能性が示された範囲を、検査対象としてモデル検査を行う技術がある（例えば、特許文献３）。特許文献３によれば、問題がある可能性がしめされた範囲は「警告」によって特定される。しかし，静的解析では多くの潜在的な警告を生成するため、検査する範囲が大きくなる。これらは、検査する範囲を限定することで、探索を効率的に行う技術である。
【００１３】
さらに他の例としては、タイムアウト時間を定義してモデル検査プログラムの実行時間を制限する技術がある（例えば、特許文献４）。さらに他の例としては、契約による設計（ＤｂＣ＝Ｄｅｓｉｇｎ  ｂｙ  Ｃｏｎｔｒａｃｔ）において定義する契約を用いる技術がある（例えば、特許文献５）。
【先行技術文献】
【特許文献】
【００１４】
【特許文献１】特許第３６３１６４７号公報
【特許文献２】ＷＯ２００６／０３８３９４号公報
【特許文献３】特開２００９−１２３２１６号公報
【特許文献４】特開２００９−０５３７５６号公報
【特許文献５】特開２００９−２１１５０３号公報
【非特許文献】
【００１５】
【非特許文献１】Ｇ．Ｊ．Ｈａｌｚｍａｎｎ著  「Ｔｈｅ  ＳＰＩＮ  ｍｏｄｅｌ  ｃｈｅｃｋｅｒ：Ｐｒｉｍｅｒ  ａｎｄ  ｒｅｆｅｒｅｎｃｅ  ｍａｎｕａｌ」Ａｄｄｉｓｏｎ  Ｗｅｓｌｅｙ，  ２０００年
【非特許文献２】中島  震著  「ＳＰＩＮモデル  検証モデリング技法」２００８年
【非特許文献３】Ａ．Ｃｉｍａｔｔｉ，  Ｅ．Ｇｉｕｎｃｈｉｇｌｉａ，  Ｍ．Ｒｏｖｅｒｉ，  Ｍ．Ｐｉｓｔｏｒｅ，Ｒ．Ｓｅｂａｓｔｉａｎｉ  ａｎｄ  Ａ．Ｔａｃｃｈｅｌｌａ．  「Ｉｎｔｅｇｒａｔｉｎｇ  ＢＤＤ−ｂａｓｅｄ  ａｎｄ  ＳＡＴ−Ｂａｓｅｄ  Ｓｙｍｂｏｌｉｃ  Ｍｏｄｅｌ  Ｃｈｅｃｋｉｎｇ」  Ｐｒｏｃｅｅｄｉｎｇｓ  ｏｆ  ４ｔｈ  Ｉｎｔｅｒｎａｔｉｏｎａｌ  Ｗｏｒｋｓｈｏｐ  ｏｎ  Ｆｒｏｎｔｉｅｒｓ  ｏｆ  Ｃｏｍｂｉｎｉｎｇ  Ｓｙｓｔｅｍｓ，  ２００２年
【非特許文献４】Ｇ．Ｂｅｈｒｍａｎｎ  ｅｔ．ａｌ  「Ａ  Ｔｕｔｏｒｉａｌ  ｏｎ  ＵＰＰＡＡＬ」  Ｉｎ  ｐｒｏｃｅｅｄｉｎｇ  ｏｆ  ｔｈｅ  ４ｔｈ  Ｉｎｔｅｒｎａｔｉｏｎａｌ  Ｓｃｈｏｏｌ  ｏｎ  Ｆｏｒｍａｌ  Ｍｅｔｈｏｄｓ  ｆｏｒ  ｔｈｅ  Ｄｅｓｉｇｎ  ｏｆ  Ｃｏｍｐｕｔｅｒ，Ｃｏｍｍｕｎｉｃａｔｉｏｎ，ａｎｄ  Ｓｏｆｔｗａｒｅ  Ｓｙｓｔｅｍｓ（ＳＦＭ−ＲＴ’０４）．  ＬＮＣＳ  ３１８５  ２００４年
【非特許文献５】Ｇ．Ｊ．Ｈａｌｚｍａｎｎ，Ｄ．Ｂｏｓｎａｃｋｉ著  「Ｔｈｅ  Ｄｅｓｉｇｎ  ｏｆ  Ｍｕｌｔｉｃｏｒｅ  Ｅｘｔｅｎｓｔｉｏｎ  ｏｆ  ｔｈｅ  ＳＰＩＮ  ＭＯＤＥＬ  ＣＨＥＣＫＥＲ」  ＩＥＥＥ  ＴＲＡＮＳＡＣＴＩＯＮＳ  ＯＦ  ＳＯＦＴＷＡＲＥ  ＥＮＧＩＮＮＥＲＩＮＧ  ＶＯＬ．３３  Ｎｏ．１０  ｐｐ．６５９−６７４，２００７年。
【発明の概要】
【発明が解決しようとする課題】
【００１６】
上記に示したように、ソースコード変換モデル検査において、モデル検査プログラムが要する時間と計算機の記憶容量の大きさが問題となる。
【００１７】
ソースコードにはソフトウェアプログラムの行うべき処理がすべて記述されており、ソフトウェアプログラムの様々な機能を実現している。ソフトウェアプログラムを検査する場合において、検査条件を設定することが一般的に行われている。具体的には、ソフトウェアプログラムの検査の際には、検査条件を設定することで、検査の範囲を限定することが行われている。例えば、特定の機能に関してのみ検査したい場合がある。そのために、機能を選択するためのソフトウェアプログラムへの入力値を、検査条件として設定する。他の例としては、ソフトウェアプログラムが受理しうる入力値の全集合のうち、代表的な値の集合に限定する。これは、同値分析や境界値分析としてよく知られている。
【００１８】
検査条件を設定した場合、ソフトウェアプログラムのソースコードのうち、かかる検査条件の下では処理されない部分が生じる。上記に示したように、モデル検査プログラムが要する時間と計算機の記憶領域の量は、動作主体の状態の量に依存することが知られている。検査条件の下で処理されない部分が検査対象に含まれていることは、検査条件の下では検査には無関係であるにも関わらず、状態の量を増大させることになる。その結果、モデル検査プログラムが要する時間と計算機の記憶領域の量が増大する。
【００１９】
本発明はかかる点を鑑みてなされたものであって、モデル検査の対象となるソフトウェアプログラムのソースコードもしくはソースコードを変換して動作仕様情報のうち、モデル検査の対象とする範囲を、検査条件の下で適切に限定することで、モデル検査プログラムが要する時間と計算機の記憶容量を削減するためのものである。
【課題を解決するための手段】
【００２０】
本発明は、複数の動作主体から構成されるシステムのソフトウェアプログラムのソースコードを、モデル検査プログラムを用いて効率的に検査することを可能にする。
【００２１】
本発明によれば、ソフトウェアプログラムのソースコードを、モデル検査プログラムが受理する専用言語を用いた動作仕様情報に変換し、かかる動作仕様情報の一部分を検査対象として選定する。かかる検査対象をモデル検査プログラムで検査し、検査対象から逸脱する実行があることがモデル検査プログラムにより示されれば、逸脱後に処理される範囲を検査対象に加える。さらに、逸脱がなく検査を完了するまで、モデル検査プログラムによる検査と、逸脱後に処理される範囲の検査対象への追加を加えることを繰り返す。
【００２２】
具体的には、本発明が提供するソースコード検査装置は、検査対象となるソースコードを受理するソースコード入力部と、検査条件を受理する検査条件入力部と、かかるソースコードを変換し、かつ、検査条件の下で限定された動作仕様情報（初期モデル）を構築する初期モデル構築部と、モデルの一部を検査対象として選定して縮小モデルを構築するモデル縮小部と、モデル検査を行うモデル検査部を有し、モデル検査部で縮小モデルからの逸脱が発見された場合には、モデル縮小部でモデルの範囲を再定義した新たな縮小モデルを作成して再度モデル検査部でモデル検査を行うことを繰り返すことを特徴とする。
【００２３】
加えて、例えば特許文献４や特許文献５で示されている、検査範囲の限定とは異なる方法でモデル検査プログラムが要する時間と計算機の記憶領域の量を削減する技術を、同時に適用してもよい。
【発明の効果】
【００２４】
本発明によれば、検査対象範囲を限定したモデル検査を逸脱がなくなるまで繰り返すことにより、動作可能範囲の網羅性を維持しつつ、かつ、最小限の検査対象範囲を選定してモデル検査を実施できる。これにより、モデル検査プログラムが要する時間と計算機の記憶領域の量を削減できる。
【００２５】
ここで注意すべきは、検査の対象となる状態の量は検査対象範囲に依存するため、本発明において限定された検査対象範囲に対する毎回のモデル検査での状態の量は、入力されるソースコードに対する状態の量よりも常に小さいことである。したがって、毎回のモデル検査に要する記憶領域の量は、入力されるソースコード全体を対象としたモデル検査に要する記憶領域の量に比べて、常に小さい。また、状態の量は検査対象範囲に対して組合せ的に増加するため、限定された範囲に対するモデル検査を繰り返すことに要する計算時間の和は、入力されるソースコード全体を対象とした１度のモデル検査に要する計算時間に比べて小さい。
【図面の簡単な説明】
【００２６】
【図１】本発明における第１の実施形態の全体構成の一例を示すブロック構成図である。
【図２】図１における、初期モデル構築部と、モデル縮小部と、モデル検査部の構成およびデータフローの一例を示すブロック構成図である。
【図３】図１における、ソースコード１０１の一例である。
【図４】図１における、全体モデル１３３の一例である。
【図５】図１における、初期モデル１０５の一例である。
【図６】図１における、パス１４３の一例である。
【図７】図１における、縮小モデル１０６の一例である。
【図８】図１における、縮小モデル１０６の他の一例である。
【図９】本発明における第１の実施形態のソースコード検査の手順の一例を示すフローチャートである。
【図１０】本発明における第２の実施形態の全体構成の一例を示すブロック構成図である。
【図１１】本発明における第３の実施形態の全体構成の一例を示すブロック構成図である。
【発明を実施するための形態】
【００２７】
以下、図面を参照して本発明の実施形態について詳しく説明する。
【００２８】
［実施例１］
本発明の実施例１に適用されるソースコード検査装置１００は、入力されたソースコード００１により定義される、ソフトウェアプログラムの振舞いが、別途入力された性質００３を満たしているかどうかを検査し、検査結果を出力する。ソースコード検査装置１００により出力される検査結果は、ソースコード００１が、性質００３を満たしている旨の応答、もしくは、性質００３を満たさない動作列（反例）である。ここで、ソースコード検査装置１００の機能構成の一例を、図１のブロック図に示す。ソースコード検査装置１００は、図示するように、ソースコード入力部１１０と、検査条件入力部１２０と、初期モデル構築部１３０と、モデル縮小部１４０と、性質入力部１５０と、モデル検査部１６０と、結果出力部１７０と、を備える。
【００２９】
不正な停止状態の検出などのように、モデル検査部１６０が性質００３の入力なしに可能な検査を実施可能な場合には、性質００３を入力する性質入力部１５０を利用しない実施形態をとってもよい。
【００３０】
以降、初期モデル構築部１３０と、モデル縮小部１４０と、モデル検査部１６０と、を、図２を参照しながら説明する。
【００３１】
初期モデル構築部１３０は、モデル変換部１３１と、検査条件設定部１３２と、を有する。
【００３２】
モデル変換部１３１は、図１におけるソースコード入力部１１０を通じて入力されたソースコード１０１を、全体モデル１３３へと変換する。全体モデル１３３は、ソースコード１０１の動作を示す動作仕様情報である。モデル変換部に入力されるソースコード１０１は、本発明により実現される装置にて検査されるプログラムのソースコードであり、例えば図３にその一部が示されるＣ言語ソースコード。ここで，ソースコード１０１は１つのソースコードである必要はなく、対象となる１つ以上のソフトウェアプログラムを記述した１つ以上のソースコードの群であってよい。全体モデルは、ある実施形態においては、図２におけるモデル検査実行部１６１により解釈可能な形式で出力される。例えば、モデル検査実行部１６１が、非特許文献１に示されるＳＰＩＮを用いてモデル検査を実行する実施形態においては、全体モデル１３３は、Ｐｒｏｍｅｌａとなる。例えば、図３にその一部が示されるＣ言語ソースコードは、図４にその一部が示されるＰｒｏｍｅｌａモデルに変換される。モデル変換部１３１は、例えば、特許文献１により示される方法により、Ｃ言語で記述されたソースコードを、Ｐｒｏｍｅｌａで記述された全体モデル１３３へと変換する。全体モデル１３３は、ある実施形態においては、モデル検査実行部１６１が解釈できる形式へと変換可能な、任意の形式でも良い。
【００３３】
検査条件設定部１３２は、図１における検査条件入力部１２０から入力された検査条件１０２と、モデル変換部１３１により出力された全体モデル１３３とを入力とし、検査条件１０２の下において全体モデルと等価である初期モデル１０５を出力する。初期モデル１０５は、ある実施形態においては、全体モデル１３３と同じ、モデル検査実行部１６１により解釈可能な形式で出力される。例えば、初期モデル１０５は、Ｐｒｏｍｅｌａ形式を用いることができる。また、全体モデル１３３は、ある実施形態においては、モデル検査実行部１６１が解釈できる形式へと変換可能な、任意の形式でも良い。検査条件設定部１３２は、例えば、図４にその一部が示されるＰｒｏｍｅｌａモデルを、図５にその一部が示されるＰｒｏｍｅｌａモデルに変換する。図４にその一部が示されるＰｒｏｍｅｌａモデルでは、行１０１から行１０８により、変数ｍｅｔｈｏｄには１、  ２、  ３、のいずれかの値が非決定的に代入されるが、図５にその一部が示されるＰｒｏｍｅｌａモデルでは、行１０１により、変数ｍｅｔｈｏｄには１が決定的に代入される。
【００３４】
モデル縮小部１４０は、パス選択部１４１と、パス適用部１４２とを有する。
【００３５】
パス選択部１４１は、検査条件１０２の下で実行可能なパス１４３を選択する。パス１４３は、例えば、初期モデル１０５を、ランダムにシミュレーション実行することか、初期モデル１０５を、分岐を手作業で選択するマニュアルシミュレーション実行することか、ソースコード１０１に対応するプログラムの実行トレースを、初期モデル１０５に対応付けることか、ソースコード１０１に対応するプログラムをデバッガ上でステップ実行して得られた実行トレースを、初期モデル１０５に対応付けることか、モデル逸脱判定部１６２から出力された逸脱分岐情報１０７を、初期モデル１０５に対応付けることか、の方法で選択される。ここで例示した、初期モデル１０５のランダムなシミュレーション実行、または、初期モデル１０５の分岐を手作業で選択するマニュアルシミュレーション実行、または、ソースコード１０１に対応するプログラムの実行、または、ソースコード１０１に対応するプログラムのデバッガ上でのステップ実行は、１度の実行でなくてよく、２回以上の実行により得られた実行トレースを利用してよい。
【００３６】
パス選択部１４１は、複数のパスを選択しても良く、また、複数の異なる方法により、パスを選択しても良い。パス選択部により選択されるパスは、例えば、図６に示す、検査モデル上の文の行番号の羅列により表現される。パス選択部により選択されるパスは、これに限らず、例えば、モデルに含まれるプロセスそれぞれについて、プロセスが起動されうるか否かと、モデルに含まれる条件分岐それぞれについて、条件が満たされうるかどうかと、の情報を含む、任意の表現でも良い。あるいは、パス選択部により選択されるパスは、モデルに含まれる文を示す任意の識別子の羅列による、任意の表現でも良い。
【００３７】
パス適用部１４２は、初期モデル１０５を、パス選択部１４１により選択されたパス１４３に対応する文のみに対して、モデル検査を行い、かつ、パス選択部１４１により選択されたパス１４３に対応する文のみにてモデル検査を完了できるか否かを判定できる情報を含む、縮小モデル１０６へと変換する。また、パス適用部１４２は、初期モデル１０５を、縮小モデル１０６に含まれる文と、パス選択部１４１により選択されたパス１４３に対応する文と、のいずれかに含まれる文のみに対して、モデル検査を行い、かつ、パス選択部１４１により選択されたパス１４３に対応する文のみにてモデル検査を完了できるか否かを判定できる情報を含む、縮小モデル１０６へと変換する。例えば、パス適用部１４２は、図７に示される縮小モデルを、図６に示されるパスに行番号が含まれる、図５に示される初期モデルの行と、図６に示されるパスに行番号が示されず、かつ、分岐の条件文であり、かつ、対応する  ｉｆ  もしくは  ｄｏ  の行が、図６に示されるパスに行番号が含まれる、図５に示される初期モデルの行と、モデル検査実行時に逸脱を判定する為のａｓｓｅｒｔ文と、を含むように生成する。図７に示される縮小モデルに含まれる、モデル検査実行時に逸脱を判定する為のａｓｓｅｒｔ文は、図６に示されるパスに行番号が示されず、かつ、分岐の条件文であり、かつ、対応する  ｉｆ  もしくは  ｄｏ  の行が、図６に示されるパスに行番号が含まれる、図５に示される初期モデルの行と、その次の行との間に含まれる。モデル検査実行時に逸脱を判定する為のａｓｓｅｒｔ文は、モデル検査実行時に逸脱を判定する為ではないａｓｓｅｒｔ文と区別するため、例えば、図７の行２１２に示されるよう、逸脱を示すコメントを付記する。
【００３８】
モデル検査部１６０は、モデル検査実行部１６１と、モデル逸脱判定部１６２と、を有する。
【００３９】
モデル検査実行部１６１は、モデル縮小部１４０により生成された縮小モデル１０６が、図１の性質入力部１５０により入力された、性質１０３を満たすかどうか、モデル検査を行う。モデル検査実行部１６１は、例えば、非特許文献１にて開示される、モデル検査プログラムＳＰＩＮに対して、Ｐｒｏｍｅｌａで記述された縮小モデル１０６の例と、ＬＴＬ式で記述された性質１０３の例とを与え、モデル検査プログラムＳＰＩＮを実行してえられた、モデル検査の結果と、縮小モデル検査結果１６３として出力する。
【００４０】
モデル逸脱判定部１６２は、縮小モデル検査結果１６３が、モデル逸脱を示す結果であるか否かを判定し、モデル逸脱が発生していなければ、縮小モデル検査結果１６３を用いて検査結果１０４を図１の結果出力部１７０を通じて出力し、モデル逸脱が発生していれば、縮小モデル検査結果１６３を用いて逸脱分岐情報１０７を生成する。例えば、縮小モデル１０６として、図７にその一部を示すＰｒｏｍｅｌａモデルを用い、モデル検査実行部１６１を実行した場合、縮小モデル検査結果として、図７の行２１２を含む反例パスが得られることから、モデル逸脱判定部１６２は、モデル逸脱が生じたと判定する。
【００４１】
本実施例におけるソースコード検査手順の一例を、図９に示されるフローチャートを用いて説明する。本実施例におけるソースコード検査手順の一例は、モデル変換ステップＳ１０１と、検査条件設定ステップＳ１０２と、パス選択ステップＳ１０３と、パス適用ステップＳ１０４と、モデル検査実行ステップＳ１０５と、モデル逸脱判定ステップＳ１０６と、からなる。
【００４２】
本実施例におけるソースコード検査手順の一例では、まず、モデル変換ステップＳ１０１において、検査対象の計算機プログラムのソースコード００１を、図１のソースコード入力部１１０を用いて、ソースコード検査装置１００に入力し、図２のモデル変換部１３１を用いて、全体モデル１３３へと変換する。例えば、図３に示されるＣ言語ソースコードを、図４に示されるＰｒｏｍｅｌａモデルへと変換する。
【００４３】
モデル変換ステップＳ１０１に続いて、検査条件設定ステップＳ１０２において、全体モデル１３３と、図１の検査条件入力部１２０を用いて、ソースコード検査装置１００に入力された検査条件００３と、を、図２に示される検査条件設定部１３２に入力し、初期モデル１０５を出力する。例えば、図４に示される全体モデルを、図５に示される初期モデルへと変換する。図４に示される初期モデルでは、行１０１から行１０８により、変数ｍｅｔｈｏｄには１、  ２、  ３、のいずれかの値が非決定的に代入されるが、図５に示される初期モデルでは、行１０１により、変数ｍｅｔｈｏｄには１が決定的に代入される。
検査条件設定ステップＳ１０２に続いて、パス選択ステップＳ１０３において、初期モデルＳ１０５を、パス選択部１４１に入力し、パス１４３を出力する。例えば、図５に示される初期モデルを、モデル検査装置にてランダムシミュレーションを実行し、パスとして、図６に示される行番号の列を出力する。
【００４４】
パス選択ステップＳ１０３に続いて、パス適用ステップＳ１０４において、図２に示される初期モデル１０５と、パス１４３を、パス適用部１４２に入力し、縮小モデル１０６を出力する。例えば、図５に示される縮小モデルと、図６に示されるパス１４３と、を、パス適用部１４２に入力し、図７に示される縮小モデルを出力する。
【００４５】
パス適用ステップＳ１０４に続いて、モデル検査実行ステップＳ１０５において、図２に示される縮小モデル１０６と、図１の性質入力部１５０を用いてソースコード検査装置１００に入力された、性質１０３を、モデル検査実行部１６１に入力し、モデル検査を実行することで、縮小モデル検査結果１６３を出力する。例えば、図７に示される縮小モデルが、「デッドロック状態に陥らない」という性質を満たすかどうかの検証結果を、モデル検査実行部１６１が、図７に示される縮小モデルを、モデル検査プログラムＳＰＩＮに入力し、デッドロック状態と、ａｓｓｅｒｔ不成立の検出を行えるオプションにて、検査を実行する。縮小モデル検査結果１６３は、例えば、検査の反例として、図７に示される縮小モデルの、行２１２のａｓｓｅｒｔ文が成立しない実行パスと、図７に示される縮小モデルの全文と、を含む。
【００４６】
モデル検査実行ステップＳ１０５に続いて、モデル逸脱判定ステップＳ１０６において、図２に示される縮小モデル検査結果１６３から、モデル逸脱の有無を判定する。縮小モデル検査結果１６３から、モデル逸脱が有ったと判定された場合、縮小モデル検査結果１６３から逸脱分岐情報１０７を生成し、パス選択ステップＳ１０３に戻り、パス選択部１４１に対して逸脱分岐情報１０７を入力する。例えば、モデル逸脱判定部１６２は、図７に示される縮小モデルの、行２１１の分岐が成立したことからモデル逸脱が生じたと判定し、図７に示される縮小モデルの行２１１を指し示す情報を、逸脱分岐情報１０７として生成し、パス選択部に入力する。これに続いて、パス選択部は、図７に示される縮小モデルの行２１１を指し示す情報から、図５に示される行２１１を含むパスを生成し、パス適用部１４２に入力する。これに続いて、パス適用部１４２は、図５に示される初期モデルと、図７に示される縮小モデルと、図５に示される行２１１を含むパスと、から、図８に示される縮小モデルを生成する。
【００４７】
図９に戻り、モデル逸脱判定ステップＳ１０６において、モデル逸脱が無しであると判定された場合、縮小モデル検査結果１６３から、検査結果１０４が生成される。例えば、検査結果１０４は、縮小モデル検査結果１６３そのものである。検査結果１０４は、図１の結果出力部を通じて、出力される。例えば、図８に示される縮小モデルが、「デッドロック状態に陥らない」という性質を満たすかどうかの検証結果を、モデル検査実行部１６１が、図７に示される縮小モデルを、モデル検査プログラムＳＰＩＮに入力し、デッドロック状態と、ａｓｓｅｒｔ不成立の検出を行えるオプションにて、検査を実行し、縮小モデル検査結果１６３として、「デッドロック状態に陥る」ことを示す情報と、「デッドロック状態に陥る」実行パスが出力された場合、モデル逸脱判定部は、縮小モデル検査結果１６３から、モデルの逸脱が無しであると判定し、縮小モデル検査結果１６３に含まれる、「デッドロック状態に陥る」ことを示す情報と、「デッドロック状態に陥る」実行パスとを、検査結果１０４として出力する。
【００４８】
［実施例２］
ある実施形態においては、図１０にしめすように、パス適用部１４４は、パス選択部１４１により選択されたパス１４３に対応する文のみに対して、モデル検査を実行可能である縮小モデル１０８と、パス選択部１４１により選択された、パス１４３に対応する文のみにて、モデル検査を完了できるか否かを判定できる情報を含む、縮小モデルメタ情報１０９と、を出力し、モデル逸脱判定部１６４は、縮小モデル検査結果１６５と、縮小モデルメタ情報１０９と、を入力としても良い。パス選択部１４１により選択された、パス１４３に対応する文のみにて、モデル検査を完了できるか否かを判定できる情報は、例えば、モデル逸脱時にのみ実行される行番号を含む。
【００４９】
［実施例３］
ある実施形態においては、図１１に示すように、パス適用部１４５が実行された時、該当実行以前にパス適用部１４５がパス１４３として出力したパスと、新たに生成したパスと、の両方を含むパスを、パス１４３として出力することで、パス適用部１４６は、縮小モデル１０６を入力にとらなくても良い。
【００５０】
なお、本実施形態の説明において、モデル検査プログラムＳＰＩＮと、モデル記述言語Ｐｒｏｍｅｌａを用いたが、本発明は特定のモデル検査プログラムおよびモデル記述言語のみを用いることができるものではなく、任意のモデル検査プログラム、および、任意のモデル記述言語を用いてよい。例えば、非特許文献３に示されるＳＭＶ、非特許文献４に示されるＵＰＰＡＡＬを用いることができ、これらに限定するものではない。
【００５１】
［実施例４］
実施例１と同時に、モデル検査における状態数を削減する他の技術を利用することができる。たとえば、特許文献４に示されるタイムアウト時間を用いて検査の実行時間を制限する技術を同時に用いることができる。さらに他の例としては、特許文献５に示される契約による設計において定義する契約情報を用いる技術を同時に用いることができる。
【産業上の利用可能性】
【００５２】
システムの可能な振舞いを網羅的かつ自動的に分析する技術として利用可能である。
【符号の説明】
【００５３】
００１，１０１  ソースコード
００２，１０２  検査条件
００３，１０３  性質
００４，１０４  検査結果
１００  ソースコード検査装置
１０５  初期モデル
１０６  縮小モデル
１０７  逸脱分岐情報
１０８  縮小モデル
１０９  縮小モデルメタ情報
１１０  ソースコード入力部
１２０  検査条件入力部
１３０  初期モデル構築部
１３１  モデル変換部
１３２  検査条件設定部
１３３  全体モデル
１４０  モデル縮小部
１４１  パス選択部
１４２，１４４，１４６  パス適用部
１４３  パス
１５０  性質入力部
１６０  モデル検査部
１６１  モデル検査実行部
１６２，１６４  モデル逸脱判定部
１６３，１６５  縮小モデル検査結果
１７０  結果出力部
【図１】
0005463226.tif 000002
【図２】
0005463226.tif 000003
【図３】
0005463226.tif 000004
【図４】
0005463226.tif 000005
【図５】
0005463226.tif 000006
【図６】
0005463226.tif 000007
【図７】
0005463226.tif 000008
【図８】
0005463226.tif 000009
【図９】
0005463226.tif 000010
【図１０】
0005463226.tif 000011
【図１１】
0005463226.tif 000012