(57)【特許請求の範囲】
【請求項１】
プログラムに含まれる変数の依存関係に関する変数依存関係データに基づいて、異なる実行単位にまたがる変数依存関係を有する箇所を不具合要因の可能性のある箇所として検出する不具合要因検出手段と、
前記変数依存関係に基づいて、前記箇所に関する不具合可能性の評価点を算出する評価点算出手段と、
前記評価点を表示する評価点表示手段とを備え、
前記評価点算出手段に入力される前記変数依存関係データはツリー形式であり、前記評価点算出手段は前記不具合要因検出手段による検出結果を前記変数依存関係データの上位ノードで集計することにより前記評価点を算出することを特徴とするソースコード検証システム。
【請求項２】
プログラムに含まれる変数の依存関係に関する変数依存関係データに基づいて、異なる実行単位にまたがる変数依存関係を有する箇所を不具合要因の可能性のある箇所として検出する不具合要因検出手段と、
前記変数依存関係に基づいて、前記箇所に関する不具合可能性の評価点を算出する評価点算出手段と、
前記評価点を表示する評価点表示手段とを備え、
前記評価点表示手段は、前記評価点が付けられたプログラムの箇所と前記評価点とを対応付けて表示し、かつ前記評価点の高低順に表示することを特徴とするソースコード検証システム。
【請求項３】
プログラムに含まれる変数の依存関係に関する変数依存関係データに基づいて、異なる実行単位にまたがる変数依存関係を有する箇所を不具合要因の可能性のある箇所として検出する不具合要因検出手段と、
前記変数依存関係に基づいて、前記箇所に関する不具合可能性の評価点を算出する評価点算出手段と、
前記評価点を表示する評価点表示手段とを備え、
前記評価点表示手段は、前記変数依存関係データのグラフにおいて、前記評価点が付けられた変数と前記評価点とを対応付けて表示することを特徴とするソースコード検証システム。
【請求項４】
前記評価点算出手段は、データ競合の可能性を示す評価点と、それ以外の可能性を示す評価点とを区別して算出することを特徴とする、請求項１乃至３のいずれかに記載のソースコード検証システム。
【請求項５】
プログラムのソースコードから変数依存関係データを解析するコード解析部と、
前記変数依存関係データからユーザ指定の変数に関係する部分を抽出する変数依存関係抽出部と、
前記ソースコードから前記抽出された依存関係データに対応するコードを抽出するコード抽出部と、
前記変数依存関係データに基づいて、異なる実行単位にまたがる変数依存関係から不具合要因の可能性のある箇所を検出する不具合要因検出手段と、
前記変数依存関係に基づいて、前記箇所に関する不具合可能性の評価点を算出する評価点算出手段とを備え、
前記コード抽出部は、前記評価点に基づき、コードの抽出範囲を選定することを特徴とする、ソースコード検証システム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明はソフトウェアのソースコードを検査する装置、ツールに関する。
【背景技術】
【０００２】
情報制御システムでは、プログラムの処理の実行タイミングにより発生する不具合が存在することがある。不具合の例として、プログラムの１変数に対して、プログラムに並列または並行に実行される複数の実行単位（プロセス、スレッド、タスクなど）があり、それらの読み書きが重なるデータ競合がある。このような不具合は発見が難しく、発生しても再現性がないことで原因究明が難しい場合が多い。
【０００３】
このような処理のタイミングに依存した不具合を発見する方法の１つに、ソースコードの静的解析がある。解析によりプログラムに存在する不具合可能性を検出する。例えば異なる実行単位の実行パス上にある同一変数への書き込みを探し出すことでデータ競合の可能性を検出する。
【０００４】
しかしタイミング依存の不具合はデータ競合以外の原因でも発生するため、静的解析により検出できるタイミング依存の不具合は種類が限定されている。また静的解析により検出された不具合可能性は、必ずしも不具合を発生させず、逆に不具合でないもの（偽陽性）を多々検出することがある。これらの問題を解決するために、形式手法の１つであるモデル検査が適用されうる。モデル検査では、設計のモデル記述言語による表現にて抽象化が適切であれば偽陽性は発生しない。またプログラムの振る舞いを網羅的に検査するため、タイミングに依存した不具合も検出することができる。特許文献１では、モデル検査を用いて割込みに起因する不具合を検出している。
【０００５】
一方でモデル検査には、網羅的な検査を行うがための課題も存在する。それは計算量が大きくなることで、計算機のメモリ等のリソースが不足したり、計算時間が長大になり、検証が未完了となる問題である。この対策として、上記の抽象化や、検査範囲の絞込みなどの方法が取られる。特許文献２では、検査対象であるプログラムのソースコードにおける変数間の依存関係（変数依存関係）を解析することで、着目された変数に関連のあるコードを絞り込む。また変数依存関係を表示して、ユーザが検証モデルに変換するコードをさらに絞り込むための範囲指定を可能としている。
【０００６】
ただし検証範囲を絞り込む場合、プログラムを広く検証するにはプログラムを分割して複数の検証を実行する必要が生じる。この分割と複数の検証実行は、検証に要する労力と時間を増大させる。このため、限られた人手と時間の下では、不具合の可能性の高い箇所から優先的に検証を実施することが必要な場合が出てくる。特に再現性のない不具合が発見されその原因を探索している状況下では、プログラム全体を検証して不具合のないことを示す場合と異なり、まずは１つの不具合を早期に検出しその原因を解析できるようにすることが求められるため、検証対象に優先順位を付ける考え方は重要となる。よって、検証対象の箇所ごとの不具合の可能性が評価され、その評価に基いた検証対象の優先順位を示す情報、または検証者による優先順位の付与に利用できる情報が検証者に提供されると、その情報は有用である。
【０００７】
検証対象の箇所ごとの不具合の可能性を評価する技術として、特許文献３では、変数依存関係上である実行単位Ａに属する変数ａが、異なる実行単位Ｂに属する変数ｂと、異なる実行単位Ｃに属する変数ｃとの間に依存関係を持つときに、実行単位Ａ，Ｂ，Ｃの実行優先順位を比較し、整合性を評価している。例えば、実行単位Ｂ，Ｃの優先度が異なる場合には整合性が無いと評価し、優先度が一致する場合には整合性があると評価する。
【先行技術文献】
【特許文献】
【０００８】
【特許文献１】特開２０１１−１９１８４３号公報
【特許文献２】特開２０１３−１５６７８６号公報
【特許文献３】特開２０１３−２５４３７１号公報
【発明の概要】
【発明が解決しようとする課題】
【０００９】
しかし、タイミングに依存する不具合は、実行単位の実行優先順位に整合性がある場合でも発生しうる。このため、上記の従来技術では、実行単位の実行優先順位が同じ場合には不具合の可能性を検出することができず、検証者に対して有用な情報を適切に提供することができないという問題がある。
【００１０】
そこで、本発明は、検証者に対して有用な情報を適切に提供することができるソースコード検証システムを提供することを目的とする。
【課題を解決するための手段】
【００１１】
本発明は、プログラムに含まれる変数の依存関係に関する変数依存関係データに基づいて、異なる実行単位にまたがる変数依存関係を有する箇所を不具合要因の可能性のある箇所として検出する不具合要因検出手段と、前記変数依存関係に基づいて、前記箇所に関する不具合可能性の評価点を算出する評価点算出手段と、前記評価点を表示する評価点表示手段とを備えることを特徴とする。
【発明の効果】
【００１２】
本発明によれば、検証者に対して有用な情報を適切に提供することができる。
【図面の簡単な説明】
【００１３】
【図１】本発明の実施形態に係るシステム構成。
【図２】ソースコード検証システムの機能と関連するプログラムの構成。
【図３】ソースコード検証システムと関連するプログラムの処理フロー。
【図４】変数依存関係探索部の処理フロー。
【図５】サンプルコード。
【図６】サンプルコードの変数依存関係のグラフ。
【図７】サンプルコードの評価データ。
【図８】サンプルコードの評価結果の表示。
【図９】修正したサンプルコードの評価結果の表示。
【発明を実施するための形態】
【００１４】
以下、図面を用いて本発明の実施形態について説明を行う。
【実施例１】
【００１５】
図１は、本実施形態に係るソースコード検証システムの構成図である。このソースコード検証システムは、ソフトウェアツールとして実現されている。各機能はソフトウェアとして実装されており、表示画面、主演算装置、主記憶装置（メインメモリ）、ハードディスク等の記憶媒体、キーボードやポインティングデバイス等の入力装置を備えるコンピュータ上で実行される。
【００１６】
ソースコード検証システムを実現するソフトウェアは、ソースコード評価プログラム１２０として、コンピュータ１１０のＲＯＭ１１３に格納されており、ＣＰＵ１１１により読み出されて実行される。コンピュータ１１０はソースコード評価プログラム１２０によって規定された処理を実行する。検査対象であるオブジェクトコードの元になるソースコードのファイルや、そのソースコードを元に作成された検証モデルのファイルは、コンピュータ１１０上のハードディスク１１４に格納されている。ソースコード評価プログラム１２０に対するユーザ操作は、キーボードなどの入力装置１３０から行うことができる。ソースコード評価プログラム１２０による出力は、ディスプレイなどの表示装置１４０への表示や、ハードディスク１１４へデータファイル生成として成されるが、図示しない外部コンピュータへのネットワークを介した出力、ＣＤ−ＲＯＭなどの外部記憶媒体へのデータファイル形式での書き込みによる出力であってもよい。また他のプログラムもソースコード評価プログラム１２０と同様に入力と出力し、操作される。
【００１７】
図２は、ＲＯＭ１１３に格納されたプログラムの構成を示している。プログラムには、検証モデル生成プログラム２１０と、ソースコード評価プログラム１２０がある。
【００１８】
検証モデル生成プログラム２１０は、ソースコード２００を入力とし、検証モデル２４０を出力する。検証モデル生成プログラム２１０は、コード解析部２２０、変数依存関係抽出部２２５、コード抽出部２３０、変換部２３５からなる。コード解析部２２０は、ソースコード２２０の変数依存関係を解析する。変数依存関係抽出部２２５は、コード解析部２２０から変数依存関係データを受け取り、ユーザが指定した変数について、変数依存関係を抽出する。コード抽出部２３０は、ソースコード２００から、変数依存関係抽出部２２５により抽出された変数依存関係データに関係するコードを抽出する。変換部２３５は、コード抽出部２３０が抽出したコードを、所定の変換ルールに沿ってモデル記述言語に変換することで、検証モデル２４０を生成し、出力する。
【００１９】
ソースコード評価プログラム１２０は、入力部２５０、検出部２６０、評価点算出部２７０、評価データベース２８０、表示部２９０とからなる。入力部２５０は、変数依存関係抽出部２２５により抽出された変数依存関係データを入力として読み込む。検出部２６０は、入力部２５０により読み込まれた変数依存関係データに対して解析を行い、異なる実行単位にまたがる依存関係を不具合要因の可能性のある箇所として検出し、評価データベース２８０に記録する。評価点算出部２７０は、入力部２５０により読み込まれた変数依存関係データと、検出部２６０による不具合要因の可能性の検出結果とから、変数依存関係上の各変数について、すなわちプログラムの各箇所について不具合可能性の評価点を算出し、評価データベース２８０に記録する。表示部２９０は、評価点算出部２７０により算出された評価点を評価データベース２８０から取得し、表示装置２９０にて表示する。表示部２９０は、評価点を変数依存関係データと共に表示することもある。
【００２０】
図３は、検証モデル生成プログラム２１０とソースコード評価プログラム１２０とが実行する処理フローである。ステップ３００で処理が開始される。このとき、評価データベース２８０は初期化される。ステップ３１０にてコード解析部２２０は、ソースコード２００を解析して変数依存関係データを生成する。ステップ３２０にて変数依存関係抽出部２２５は、コード解析部２２０の解析した変数依存関係データから、ユーザが指定した変数に関連する変数依存関係データを抽出する。ステップ３３０にて入力部２５０は、変数依存関係抽出部２２５により抽出された変数依存関係データを入力として読み込む。ステップ３４０にて検出部２６０は、変数依存関係データに対して解析を行い、異なる実行単位にまたがる依存関係を検出し、評価データとして評価データベース２８０に記録する。ステップ３５０にて評価点算出部２７０は、変数依存関係上の各変数について不具合可能性の評価点を算出し、評価データとして評価データベース２８０に記録する。ステップ３６０にて表示部２９０は、評価点算出部２７０により算出された評価点を評価データベース２８０から取得し、表示装置２９０にて表示する。ステップ３９０で処理を終了する。
【００２１】
図４は、評価点算出部２７０によるステップ３５０の処理を詳細化したフローである。この処理は、ツリー形式に抽出された変数依存関係データの各ノードにおいて実行されるものであり、かつルートノードから下位ノードに向かって再帰的に実行される。ステップ４００で処理が開始される。ステップ４１０からステップ４５０は、各下位ノードについて実行される。ステップ４１０では、各下位ノードに対して本フローの処理が実行される。ステップ４２０からステップ４５０は、１つの下位ノードが評価対象としている各変数について実行される。ステップ４２０では、１変数についての当該下位ノードにおける評価データが評価データベース２８０から取得される。この評価データはカテゴリ１とカテゴリ２に区別されている。カテゴリ２はデータ競合の可能性を示し、カテゴリ１はそれ以外の可能性を示す。カテゴリ２がデータ競合の可能性を示す理由は、変数ツリーの下位に同一の変数へのアクセスが出現していることを意味しているためである。
【００２２】
ステップ４３０では、ステップ４２０で対象とした変数が、現ノードにおいて評価対象とされているかを評価データベース２８０から判定する。当該変数に関する評価データが評価データベース２８０にない、すなわち評価対象とされておらず、かつ下位ノードでの当該変数の評価データがカテゴリ１であれば、ステップ４４０へ進む。それ以外、すなわち評価データがあり評価対象とされているか、または下位ノードでの評価データがカテゴリ２であれば、ステップ４５０へ進む。ステップ４４０では、当該変数に関する下位ノードでの評価データを、当該ノードのカテゴリ１の評価データとして評価データベース２８０に記録する。ステップ４５０では、当該変数に関する下位ノードでの評価データを、現ノードのカテゴリ２の評価データに追加する。さらに現ノードでの当該変数に関するカテゴリ１の評価データをクリアしてカテゴリ２に追加し、評価データベース２８０に記録する。全ての評価対象変数と下位ノードについて処理を実施した後、ステップ４９０にて本フローを終了する。
【００２３】
図４の処理フローのように、下位ノードにおける不具合要因の検出結果を、上位ノードで集計することにより、上位ノードにおける不具合リスク、コード抽出部２３０が抽出するコードに含まれる不具合リスクを評価することができる。
【００２４】
図５は検証対象となるサンプルプログラムのソースコードの一部を示している。本実施例では、ソースコードはＣ言語で記述されているものとする。ソースファイル５１０，５２０，５３０からなるプログラムの構成を以下に説明する。主処理は関数ｆｕｎｃである。関数ｉｎｐｕｔは割込みにより実行される設定となっており、レジスタ変数ＤＩ０に入力される値を変数ａに代入する。レジスタ変数ＤＩ０の値はいつでも変化しうる。関数ｆｕｎｃでは、変数ａを２倍する処理を関数ｃａｌｃ１，ｃａｌｃ２で冗長に行い、２つの計算結果ｘ１，ｘ２を比較して、一致していれば計算結果を確定させて変数ｘに代入し、一致していなければエラー対処を関数ｅｒｒ＿ｈａｎｄｌｅで行なう。
【００２５】
図６は、図５のサンプルソースコードをコード解析部２２０が解析し、変数依存関係抽出部２２５が変数ｘ（０１６行目）をルートノードとしてツリー形式に抽出した変数依存関係データをグラフ化した変数ツリー６００である。変数依存関係データや変数ツリー６００にて、ノードは変数を示しており、変数は記述位置や属する実行単位で区別されている。例えばｘ＠０１６は、０１６行目の変数ｘを意味している。各変数が属する実行単位や関数は図には示されていないが、データには含まれる。変数ツリー６００では、ｉｆ文のような制御構文もノードとして扱っている。斜め線のついている変数ノードは、当該ノードが変数ツリーの他の箇所に既出であり（以下「既出ノード」を呼ぶ）、下位ノードを省略していることを意味している。矢印が依存関係を示しており、矢印の元が依存元つまり変数値に影響を与える方、矢印の先が依存先つまり影響を受ける方である。また実線の矢印は依存先と依存元の変数が同一の実行単位に含まれることを意味し、破線の矢印は異なる依存先と依存元の変数が異なる実行単位に属することを意味する。
【００２６】
検出部２６０はステップ３４０にて、変数ツリー６００を探索し、破線の矢印で表現される依存関係を発見、抽出する。変数ツリー６００では、ａ＠２０５からａ＠１０４への依存関係と、ａ＠２０５からａ＠１０９への依存関係が該当する。これらは異なる実行単位にまたがる依存関係であり、処理タイミングに依存する不具合要因の可能性のある箇所として認識される。
【００２７】
図７は、図５のサンプルソースコードに関する評価データベース２８０の内容を示している。評価データ７００では、変数ツリー６００のノードごと、すなわち記述位置（ここでは行で表現）で区別された変数ごとに、カテゴリ１とカテゴリ２それぞれの評価データが記録されている。「ａ（２）」は、変数ａが評価対象として、不具合要因の可能性のある箇所が当該ノードから下位に２箇所存在していることを示している。この数値が評価点となる。なお図７では評価データが空のノードなど、一部データの図示を省略している。
【００２８】
なお、評価点は、上述のように不具合要因の可能性のある箇所の個数の値に限定されるものではなく、種々のものが考えられる。例えば、評価点は、不具合要因の可能性のある箇所の個数に対応させてＡ、Ｂ、Ｃ、…といったように不具合要因の可能性の程度を表すものであってもよい。この場合には、不具合要因の可能性のある箇所が１箇所であれば評価点をＡとし、２箇所であれば評価点をＢとするといった方法を採ることもでき、不具合要因の可能性のある箇所が１〜２箇所であれば評価点をＡとし、３〜４箇所であれば評価点をＢとするといったように、一つの評価点が所定の幅を有するものであってもよい。
【００２９】
検出部２６０が抽出した２箇所の依存関係は、ａ（１０４行目）とａ（１０９行目）のカテゴリ１の欄に、「ａ（１）」として記録されている。つまり検出部２６０が抽出した依存関係は、依存先の変数に関するデータとして評価データベース２８０に記録される。ステップ３４０が終了した時点では、評価データ７００に記録されたデータはこの２つのみである。その次に、評価点算出部２７０がステップ３５０にて、図４の処理フローを変数ツリー６００と評価データ７００を入力として実行する。ｘ１＠１０４は下位にａ＠１０４があり、ａ＠１０４はカテゴリ１に「ａ（１）」の評価データがある。ｘ１＠１０４には変数ａについての評価がないため、ステップ４３０からはステップ４４０に進み、評価データ７００のカテゴリ１に「ａ（１）」が入る。同様にｘ１＠０１６のカテゴリ１にも「ａ（１）」が入る。変数ツリー６００にて、斜め線のついた変数ノードであるｘ１＠１０４では、図４の処理は実施せず、評価データは空とする。これにより、ｘ１＠０１２も評価データが空になる。
【００３０】
ｘ２＠１０９の下位にはａ＠１０９があり、ｘ２＠１０９には変数ａについての評価がないため、評価データ７００のカテゴリ１に「ａ（１）」が入る。同様にｘ２＠０１２、ｉｆ＠０１２のカテゴリ１にも「ａ（１）」が入る。ｘ＠０１６の下位にはｘ１＠０１６とｉｆ＠０１２がある。まずｘ１＠０１６の評価データを取得すると、カテゴリ１に「ａ（１）」の評価データがあり、ｘ＠０１６には変数ａについての評価がないため、カテゴリ１に「ａ（１）」が入る。次にｉｆ＠０１２の評価データを取得すると、やはりカテゴリ１に「ａ（１）」の評価データがあるが、ここでｘ＠０１６のカテゴリ１には既に変数ａについての評価データが存在するため、ステップ４３０からはステップ４５０に進み、既に記録されたカテゴリ１の「ａ（１）」をクリアしつつ、ｉｆ＠０１２の「ａ（１）」と合算し、カテゴリ２に「ａ（２）」を記録する。以上でステップ３５０の処理は終了する。
【００３１】
図７で評価データ７１０は、評価データ７００とは異なる形式での評価データの記録方法を示している。評価データ７１０では、検出部２６０が抽出した依存関係の依存先が記録される。ステップ４４０やステップ４５０でも、検出部２６０が抽出した情報を保持して記録がされる。このためｘ＠０１６には、カテゴリ２の要因としてａ＠１０４，ａ＠１０９が記録される。評価点は各カテゴリに記録された変数の数をカウントして付けられる。ａ＠１０４，ａ＠１０９はそれぞれカテゴリ１に自身を含んでいるため、不具合要因の存在箇所であることがわかる。評価データ７１０の形式では、不具合要因の重複は排除することができるため、既出ノードであるｘ１＠１０４でも図４の処理を実施してよい。実施した場合、ｘ１＠０１２はカテゴリ１に「ａ＠１０４」が入る。ｉｆ＠０１２ではカテゴリ１に「ａ＠１０４」と「ａ＠１０９」が入る。ｘ＠０１６にて、ｘ１＠０１６の「ａ＠１０４」と、ｉｆ＠０１２の「ａ＠１０４」が重複していることがステップ４５０にて判定され、片方だけがカテゴリ２に記録される。
【００３２】
図８は、表示部２９０によるステップ３６０での表示内容を示している。評価点テーブル８００は、評価データ７００または７１０の内容を集計したものである。ｘ＠０１６はカテゴリ２の評価点が２、ａ＠１０４とａ＠１０９はカテゴリ１の評価点が１であることが示されている。なお評価点テーブル８００は、変数ツリー６００の各ノードのうち、下位ノードと評価点が異なるノードのみを表示している。プログラムの他の箇所や、ｘ＠０１６の依存先を変数依存関係のルートとして同様に評価点を算出し、評価点の高い順に評価点テーブル８００と同様の表示を行なうことで、ユーザは検証対象に優先順位を付けることができる。またカテゴリ１，２と区別して評価点が表示されているため、ユーザは不具合要因がデータ競合なのかそれ以外なのかを認識することができ、検証対象を選定する際の参考情報とすることができる。例えばデータ競合について優先的に検証するという方針があるときは、カテゴリ２の数値が高い箇所を選べばよい。但し、評価点がカテゴリ１，２の数値を合算した値で表示されるものであってもよい。また、特定のカテゴリの優先度が高い場合には、そのカテゴリに関する評価点のみを表示するものであってもよい。
【００３３】
評価点テーブル８００では変数ごとに評価点を表示したが、表示部２９０がソースコード２００を入力として、変数の記述位置情報を利用して、変数が記述された箇所のコードを評価点と共に表示してもよい。
【００３４】
変数ツリー８１０は、変数ツリー６００の各ノードに、評価データ７００のカテゴリ１，２の数値を付与して表示したグラフである。各ノードに付記された数値のうち、左側がカテゴリ１、右側がカテゴリ２の数値を示している。このような表示により、ユーザは視覚的に変数ツリーと不具合要因の分布との関係を認識することができる。
【００３５】
検証モデル生成プログラム２１０のコード抽出部２３０に対し、ユーザは変数ツリー上で抽出範囲を指定するとしたとき、変数ツリー８１０のような表示は、検証対象の優先順位を含め、ユーザによる抽出範囲の検討をしやすくする。変数ツリーにて下位ノードを全て抽出すると、コード抽出量が膨大になる場合がある。このため途中で下位ノードの抽出を打ち切ることができれば、コード抽出量は抑えられ、検証モデルのサイズも小さくなる。変数ツリーの下位ノードを抽出する深さは、上位ノードの評価点に影響する。ユーザは段階的に下位ノードを抽出しながら、評価点を観察することで、下位ノードの抽出範囲を適切に選定することができる。
【００３６】
コード抽出部２３０は、評価データベース２８０から評価点を取得し、検証範囲を自動的に選定することもできる。例えば変数ツリー６００のルートノードの各下位ノードについて、評価点の最も高いノードをルートとするサブツリーを用いてコードを抽出することで、検証対象を分割しつつ、不具合可能性の高い箇所を含む検証モデルを生成することができる。または、プログラムに記述されている変数について１つずつ変数ツリーを抽出させ、評価点を観察し、評価点が指定された閾値以上となる変数について、コード抽出と検証モデルへの変換を実行してもよい。
【００３７】
関数ツリー８２０は、変数ツリー８１０の各ノードを属する関数を単位として集約し、その関数をノードとして表現したものである。変数ツリー８１０と同様に評価データ７００の評価点が関数ノードに付与されているが、１つの関数内でもっとも評価点の高い変数ノードの数値が付与されている。関数ツリー８２０は、変数ツリー８１０より表示が簡素化されるので、ユーザの認識がしやすい。ユーザは評価結果を詳細に把握したいときには変数ツリー８１０を、概要を把握したいときには関数ツリー８２０を表示させるといったように使い分ければよい。
【００３８】
なお図８に示されるような評価点の情報は、モデル検査だけでなく、ソフトウェアの検証手法全般での対象の優先順位付けや、不具合の可能性がある箇所の抽出に利用できる情報である。
【００３９】
ところで、図８では、プログラム中の変数依存関係を有する全ての箇所に対して評価点を表示するものであるが、これに限定されるものではない。例えば、評価点が０である点には評価点を表示しないものであってもよく、また、評価点が一定以上（例えば、２点以上）の箇所のみを表示するものであってもよい。さらには、複数の変数の中でも特に不具合を生じさせやすい特定の変数に関係する箇所のみを表示するものであってもよく、例えば図８の例では、カテゴリー１に関する評価点のみを表示することが考えられる。  図９は、ユーザが図８の評価結果や、さらにその評価結果から検証モデル２４０を生成させて検証実行した結果から、不具合要因を把握してソースコード５１０を修正したソースコード９１０、およびソースコード９１０，５２０，５３０について図３の処理を実行し、変数ツリー８１０と同様に評価結果を表示させた変数ツリー９２０を示している。ソースコード９１０では、関数ｉｎｐｕｔを割込みで実行する設定をやめ、関数ｆｕｎｃの冒頭で呼び出すように修正している。これにより、変数ａの値が関数ｆｕｎｃの以降の実行中に変化することがなくなる。この修正により変数ツリー９２０では、全ての評価点が０となり、ユーザは不具合要因が除去されたことを認識することができる。
【００４０】
以上のように、本実施形態に係るソースコード検証システムによれば、タイミングに依存する不具合を良好に検出することができ、検証者に対して有用な情報を適切に提供することができる。具体的には、検証対象の箇所ごとの不具合の可能性を評価し、その評価に基いた評価点を検証対象の箇所ごとに付与し、その評価点が表示されるため、検証者は、検証対象の優先順位を容易に把握することができる。従って、検証者は前記評価点から、プログラムの各箇所について検証実施の優先順位を決めることができ、限られた人手と時間の中で費用対効果の高い検証を実施することができる。
【符号の説明】
【００４１】
１２０…ソースコード評価プログラム、１４０…表示装置、２００…ソースコード、２１０…検証モデル生成プログラム、２２０…コード解析部、２２５…変数依存関係抽出部、２３０…コード抽出部、２３５…変換部、２４０…検証モデル、２５０…入力部、２６０…検出部、２７０…評価点算出部、２８０…評価データベース、２９０…表示部
【図１】
0006416588.tif 000002
【図２】
0006416588.tif 000003
【図３】
0006416588.tif 000004
【図４】
0006416588.tif 000005
【図５】
0006416588.tif 000006
【図６】
0006416588.tif 000007
【図７】
0006416588.tif 000008
【図８】
0006416588.tif 000009
【図９】
0006416588.tif 000010