JP6002507B2 - ソフトウェア検証用プログラムおよびソフトウェア検証システム - Google Patents

Description

本発明はソフトウェアの構造を解析するソフトウェアツールに係り、特にデータフローを利用した変数の属性解析と、検証用のモデルを構築するソフトウェアツールに関する。

近年、ソフトウェアの規模が巨大化し、構造や処理の複雑さが増しており、設計者や検証者がソフトウェアの全容を把握することが困難になっている。また、ソフトウェアが取りうる全ての状態をカバーするテストケースを用意して検証することが難しくなっている。特に車載機器等の制御を行う制御装置では、装置の電動化に伴う制御用ソフトウェアの規模増大により、ソフトウェアを含む電子制御装置に不具合が潜在し、システムの安全性を損なう恐れが増していることを背景として、種々の機能安全規格が制定されている。これらの制御システムでは、ハードウェアの不具合がソフトウェアの不具合を誘発することもあるため、ソフトウェアの検証だけでは不十分であり、ハードウェアとソフトウェアとを合わせて検証する必要がある。しかし特定のタイミングのみに発生する不具合は、テストで検出することが難しい。タイミング関連の不具合を引き起こす要因としては、複数のハードウェアの並行動作や、割り込み処理を挙げることができる。

システムの安全性を確保する上でも、設計者や検証者がソフトウェア、特に過去のソフトウェア資産や他の設計者が記述したソースコードの構造や処理を理解することが好ましい。また、ソフトウェアの取りうる状態に対するテストの網羅性を向上させ、不具合の原因を排除することが要求される。

設計者や検証者による理解を容易にすることを目的として、プログラムに対し静的解析や動的解析を行い、その結果を関数コールグラフなどの図形として視覚化する手法とソフトウェアツールがある。視覚化対象のうち、ソフトウェアの構成上で重要な情報の１つとして、命令間や変数間の依存関係がある。ここで依存関係は、実行順序により実行結果が変化する可能性のある関係である。

一方、システムの状態を網羅的に検証する技術として、モデル検査がある。モデル検査技術では、システムを状態遷移モデルに置き換え、システムに要求される性質をプロパティやアサーションとして定義し、状態遷移モデルと共にツールに入力することで、当該ツールがシステムの取りうる状態を調べ上げ、与えられたプロパティやアサーションが満たされるか否かを判定する。満たされない場合には、反例を出力する。

ハードウェアとソフトウェアの複合動作や相互作用により発生する不具合をモデル検査で検出するには、例えば特許文献１に開示されているように、システムの検証モデルとして、ハードウェアなどの外部環境モデル（ソフトウェアに対する外部環境を表現する検証用モデル）と、ソフトウェアモデル(ソフトウェアを表現する検証用モデル)とを作成し、合成する必要がある。ソフトウェアモデルの生成には、ソースコードを変換する方法がある。ただしソースコードを全て検証用モデルに変換すると、メモリ不足による状態探索未完了の問題（状態爆発と呼ばれる）が発生する虞があるため、コードの一部を抽出するスライシングと呼ばれる処理がなされることもある。

特開２００９-１２３１５９号公報

特許文献１記載のように、ソースコードの一部を抽出してソフトウェアモデルに変換する場合、ソフトウェアモデルの入出力に関係するハードウェアや、検証項目に関係するが抽出されなかったソフトウェアは、外部環境モデルとする必要がある。検証者はこの外部環境モデルを、検証目的に応じて詳細なものにしたり、抽象度の高いものにしたりできる。ただしソフトウェアモデル、外部環境モデル、およびシステムの検証モデルを用意するのは一般的に手間が掛かる。

また、特許文献１記載の技術では、外部環境モデルは、ソフトウェアのうち検査対象とする一部分の状態遷移情報から、検査対象外である他部分の挙動を模擬し、検査対象部分と他部分とのメッセージ通信を生成するものである。このため、検査対象とするソフトウェアの状態遷移情報がないと、外部環境モデルを生成できない。また、外部環境モデルにて故障などソフトウェアで想定していない挙動を取ることができない。

このような制約を受けない外部環境モデルを検査に適用するには、検査対象とするソフトウェアに応じて外部環境モデルを用意するか、用意された外部環境モデルに応じてソフトウェアから検査対象を抽出する必要がある。このとき、ソフトウェアモデルの入出力と、外部環境の入出力とは整合しなくてはならない。このため、ソースコードから一部を抽出する際に、外部環境モデルの入出力と整合するように、外部環境との境界となる変数を決めて抽出範囲を調整する必要がある。または逆に、ソフトウェアモデルの入出力に合わせて、外部環境モデルを用意する必要がある。入出力が整合するには、変数が表現するデータの種別が同じであり、単位や値域が同じである必要がある。

ソフトウェアモデルと外部環境モデルとの入出力を整合させるには、入出力となる変数の属性を一致させる必要があり、検証者は入出力変数の属性を調べる必要がある。一方で、コードの抽出範囲を過小に限定してしまうと、不具合の原因をモデル化できないため、不具合の原因をモデルに含めつつ状態爆発を回避して検証しようとするならば、ソフトウェアからコードを抽出する範囲を柔軟に調整する必要がある。しかし、抽出範囲を調整すると、調整の度に入出力変数が替わるため、変数の属性を調べなおさなければならず、規模が増大し複雑さが増しているソフトウェアについて、外部環境モデルと接続しうる変数を探索して、各変数の属性を調べることには多大な労力が必要となる。

本発明はこのような課題に鑑みてなされたものであり、本発明の目的は、システムの検証モデルとして、ハードウェアなどの外部環境モデルとソフトウェアモデルとを作成して合成する際に、ソフトウェアモデルと外部環境モデルとの入出力を整合させる手間を低減することにある。

上記課題を解決するため本発明は、検証対象となるソフトウェアのソースコードを入力とし、前記ソースコードを解析して、モデル検査用のモデルを生成する検査用モデル生成プログラムにおいて、前記プログラムは、前記コンピュータに前記ソースコードの変数等の依存関係を導出する依存関係解析部と、前記ソースコードの一部の変数について属性情報を記録する変数属性記録部と、前記依存関係と前記変数属性記録部の属性情報から、前記ソースコードの各変数について属性を推論する変数属性解釈部と、前記属性情報を表示する変数属性情報表示部と、を有するように構成する。

次に、外部環境モデルデータベースと、前記変数属性情報に応じて前記外部環境モデルデータベースから利用可能なモデルを引き出す外部環境モデル候補抽出部とを有するように構成する。

次に、前記依存関係に対して範囲限定の指定を受け付ける依存関係限定部と、前記の限定された依存関係からソースコードのスライシングを行うソースコード抽出部と、前記の抽出されたソースコードから検査用のソフトウェアモデルを生成するモデル変換部と、前記外部環境モデル候補抽出部が引き出したモデルから利用するモデルを選ぶ外部環境モデル選択部と、前記ソフトウェアモデルと、前記外部環境モデル選択部が選んだ外部環境モデルとから、検査用のシステムモデルを合成するシステムモデル合成部と、を有するように構成する。

検査用モデル生成プログラムが、変数の一部(マイコン入出力を行うレジスタ変数や、関数の引数など)に関する属性情報から、変数の依存関係を辿りつつ、他の変数の属性を推論することにより、前記プログラムのユーザは全ての変数について属性情報を自ら調査する必要が無くなり、ソフトウェアモデルと外部環境モデルとの入出力を整合させる手間が軽減される。

また検査用モデル生成プログラムが、推論されたものを含む変数属性情報から、外部環境モデルとして利用可能なものをデータベースから抽出することにより、前記プログラムのユーザは外部環境モデルの選択に掛かる工数を低減することができる。

またユーザが変数を１つ以上選択すると、検査用モデル生成プログラムが、選択された変数と依存関係のある変数の属性情報から、スライシング後のソフトウェアモデルに接続可能な外部環境モデルをデータベースから探索し、候補として提示する。逆に、外部環境モデルを選択すると、その外部環境モデルの入出力変数の属性から、接続可能なソフトウェアの変数を探索し、スライシングの条件（スライス基準）として設定することで、選択された外部環境モデルと接続可能なソフトウェアモデルの変換元となるソースコードを抽出する。以上により、ユーザが検証のためにハードウェアとソフトウェアの双方をモデル化する作業に掛かる工数を低減することができる。

本発明の構成を表す図である。 本発明の機能構成を表す図である。 変数の属性情報を推論する処理フローを表す図である。 属性推論処理の詳細な処理フローを表す図である。 解析対象例のソースコードを表す図である。 変数依存関係グラフの例を表す図である。 変数属性データベースに格納されているテーブルを表す図である。 推論ルールデータベースに格納されているテーブルを表す図である。 変数属性情報を表す図である。 変数属性情報を表す図である。 本発明の機能構成を表す図である。 システムの検証モデルを生成する処理フローを表す図である。 外部環境モデルの候補リストを表す図である。 システム検査用モデルを表す図である。

以下、図面を用いて本発明の実施形態について説明を行う。

図１は、本発明をシステムとして実現した場合のシステム構成である。本発明は、例えばソフトウェアツールとして実現される。システム１０において、処理を実行するためのソフトウェアは検証モデル生成プログラム１１３１として、例えばコンピュータ１１上のＲＯＭ１１３に格納されており、ＣＰＵ１１１によって読み出され、ＲＡＭ１１２を作業用記憶領域として用い、実行される。これにより、コンピュータ１１は検証モデル生成プログラム１１３１によって規定された処理を実行する。その処理内容は図２以降で説明する。解析対象となるソースコードファイルは、コンピュータ１１上のハードディスク１１４などの記憶装置に格納されている。解析実行指示などのユーザ操作は、キーボードなどの入力装置１２から行うことができる。

なお、検証モデル生成プログラム１１３１による出力は、例えばディスプレイなどの表示装置１３になされるが、それ以外に、図示しない外部コンピュータへのネットワークを介した出力、ＣＤ−ＲＯＭなどの外部記憶媒体へのデータファイル形式での書き込みによる出力であってもよい。

図２は、検証モデル生成プログラム１１３１の基本的な機能構成を示している。ファイル入力部２１は、解析対象となるソースコードファイルをユーザが１ないし複数選択できる機能を有しており、ユーザによるファイル指定に従い、ソースコードファイルをコンピュータの記憶媒体（ハードディスク１１４など）から読み込む。依存関係解析部２２は、ユーザが解析実行を指示すると、ファイル入力部２１が読み込んだソースコードファイルを解析し、ソースコードから生成されるプログラムの依存関係を導出する。ここで依存関係とは、プログラムの実行順序により演算結果に影響のありうる関係のことであり、具体的には、ステートメント間の依存関係であるプログラム依存関係や、変数間の依存関係である変数依存関係である。プログラム依存関係を変数単位に分解すると変数依存関係になるので、プログラム依存関係と変数依存関係は情報としては等価とみなせる。プログラム依存関係や変数依存関係の導出方法については、文献に譲り、本明細書では割愛する。

変数属性入力部２３は、ソースコードに記述されたある変数に関する属性について、ユーザからの入力を受け付ける。以降では特に明記しない限り、変数の属性といえば、ソフトウェアモデルの入出力の整合に関係するものを指すとする。変数属性データベース２４は、ファイル入力部２１が読み込んでいるソースコードの一部の変数について、属性情報を記録している。変数属性解釈部２５は、依存関係解析部２２が導出した依存関係情報と、変数属性入力部２３と変数属性データベース２４のいずれか、または両方が持つ変数属性情報とから、ソースコードに記述された各変数の属性について、可能な限り推論を行う。推論には、推論ルールデータベース２６に記録されたルールを用いる。変数属性表示部２７は、変数属性解釈部２５が推論した変数属性情報を、変数属性入力部２３と変数属性データベース２４の持つ変数属性情報と併せて、表示装置１３に表示する。

図３は、検証モデル生成プログラム１１３１が図２に示された機能を用いて行う処理であり、入力となるソースコードに記述された変数の属性情報を推論する処理のフローを示している。

処理を開始すると、ステップ３１にて、依存関係解析部２２は、入力となるソースコードの依存関係を解析し、データとして出力する。例として、変数ａと変数ｂについて、ａ＝ｂという式がソースコードに記述されているとすると、変数依存関係としては「ａ←ｂ」と表現できる。これは変数ｂが変数ａに影響を与えるという意味である。逆に「ａ→ｂ」と記述してもよく、表現のルールを決めればよい。本実施例では前者を採用する。また、ａは依存元、ｂは依存先と呼ぶことにする。

次にステップ３２にて、変数属性解釈部２５は、変数属性入力部２３や変数属性データベース２４から、入力となるソースコードに記述された変数の属性情報を取得し、依存関係解析部２２の出力した依存関係データにおける各変数と対応付ける。なおステップ３２は、該当する変数の属性情報が空のときだけ実行し、それ以外ではスキップする。

次にステップ３３にて、変数属性解釈部２５は、依存関係データにおいて属性推論処理の始端となる変数を抽出する。本実施例では、入力となるソースコードがプログラムとして実行される際に入力となる変数の属性情報をもとに、前向きに（依存先の変数から、依存元の変数へ）属性情報の推論を進めるものとする。また、本実施例の処理は再帰的になっている。このため始端変数として、影響する変数がない、すなわちどの変数からも依存されていない（依存元になる変数が存在しない）変数を抽出する。ただし依存関係がループしており該当する変数が存在しない場合には、任意の変数を１つ選択する。

次にステップ３４にて、変数属性解釈部２５は、対象とする始端変数のそれぞれについて、属性を推論する処理（詳細は図４に記載）を行う。ステップ３４は、ステップ３３にて抽出された全ての推論始端となる変数について、それぞれ実行する。以上をもって処理を終了する。

なお、図３の処理を実行するタイミングは、ユーザによる実行指示時か、ユーザが変数属性入力部２３に対し属性情報を入力したときとする。処理を終了したら、変数属性表示部２７が、出力された依存関係情報を表示装置１３に表示する。

図４は、ある変数の属性情報を推論する処理であり、図３のステップ３４（「属性推論」処理）の詳細フローを示している。

処理を開始すると、ステップ４１は、属性情報を推論する対象変数の全ての依存元変数について、それぞれ実行する。ステップ４１にて、変数属性解釈部２５は、対象とする依存元変数について、属性情報を推論する処理（図４の処理）を行う。次にステップ４２にて、変数属性解釈部２５は、対象変数と依存元変数とがデータ依存関係にあるかを判定する。データ依存関係であれば、対象変数の属性情報を更新する必要が無いので処理を終了し、そうでなければ、ステップ４３に進む。次にステップ４３にて、変数属性解釈部２５は、いずれかの依存元変数の属性情報がステップ４１にて更新されたか否かを判定する。１変数でも更新されていればステップ４４に進み、１つも更新されていなければ、対象変数の属性情報を保持して、処理を終了する。次にステップ４４にて、変数属性解釈部２５は、対象変数が推論ルールデータベース２６に記録されている推論ルールに該当するか否かを判定する。１ルールでも該当すればステップ４５に進み、該当するルールがなければ、対象変数の属性情報を保持して、処理を終了する。次にステップ４５にて、変数属性解釈部２５は、ステップ４４にて該当した推論ルールに基づき推論処理を実行し、その結果を対象変数の属性情報に反映する。以上をもって処理を終了する。なお上記は依存関係がループしていない場合の処理であり、ループが存在する場合には、１度「属性推論」処理の対象になった変数は対象外にすることが必要となる。

以下では、図３と図４の処理例を示す。図５のソースコード５０は、解析対象として検証モデル生成プログラム１１３１に入力する、Ｃ言語で記述されたソースコードの例である。左端の数字は行番号である。

図６の変数依存関係グラフ６１は、図５のソースコード５０を依存関係解析部２２が解析し出力する変数依存関係データをグラフ化したものである。この変数依存関係グラフ６１は、例えば表示装置１３に表示される。変数依存関係グラフ６１のノードは、変数の名称や実体（記憶領域）だけでなく、記述位置（および実行パス）でも区別した変数である。例えば「ｓｔｒｏｋｅ（Ｌ２０＠ｃｏｎｔｒｏｌ）」と表記された変数は、ソースファイルの２０行目、関数ｃｏｎｔｒｏｌ内に記述された変数ｓｔｒｏｋｅであること意味している。変数の区別には、記述された行番号だけでなく列番号や、ソースファイル名を用いてもよい。また、図６のグラフには記載されていないが、各ノードには、変数の型のようにソースコードのみから判明する属性や、変数属性入力部２３や変数属性データベース２４から与えられた属性、変数属性解釈部２５が推論した属性が対応付けられ、データとしてＲＡＭ１１２やハードディスク１１４に記憶されている。

また図６において、依存関係を示すエッジ（矢印）、および演算式における関係を示すエッジ（破線）には、関係の種類を示すデータが対応付けられて記憶されている。依存関係のエッジにおいて、ｄｅｆは依存元の変数を依存先の変数が定義（代入などにより値を決めていること）を示している。ｕｓｅはデータ依存関係（依存元の変数が、依存先の変数の値を利用していること）を示している。ｃｏｎｄは制御依存関係（依存先の変数の値により実行パスが変わるため、依存元の変数の値に影響があること）を示している。

図７の変数属性テーブル７１は、変数属性データベース２４に記録されている変数属性の例を示している。変数属性テーブル７１の項目は、変数名、ｉｎ／ｏｕｔ（変数がプログラムの入力か出力か）、単位、データ種別からなる。これらの値は予め設定されている。変数ｒｅｇ＿ａｄ＿１は、入力用の変数であり、データ種別は（例えば自動車のブレーキペダルの）ストローク量であることがわかる。またその単位は「（Ａ／Ｄ変換値）」とあるが、これはＡ／Ｄ（Ａｎａｌｏｇ／Ｄｉｇｉｔａｌ）変換により得られる値であり、単位は特に決められていないことを示している。

図８の推論ルールテーブル８１は、推論ルールデータベース２６に記録されている推論ルールの例を示している。推論ルールテーブル８１の項目は、前件と後件からなる。前件の条件が成立するときに、後件の条件も成立することを意味している。前件と後件は、述語論理で表現されている。これらの値は予め設定されている。

推論ルールテーブル８１の推論ルールＮｏ．１にて、ＸとＹはある変数を示しており、Ｄｅｆ（Ｘ，Ｙ）「ＸがＹを定義している」ならば、ＳａｍｅＡｔｔｒ（Ｘ，Ｙ）「ＹはＸと同じ属性情報を有する」ことを意味している。

推論ルールテーブル８１の推論ルールＮｏ．２にて、Ｘ，Ｙ，Ａはある変数を示しており、Ｃｏｎｄ（Ｘ，Ａ）「ＡがＸと制御依存関係にある（Ａが依存元）」かつ、Ｃｏｎｄ（Ｙ，Ａ）「ＡがＹと制御依存関係にある」かつ、Ｃｏｍｐ（Ｘ，Ｙ）「ＸとＹとは演算式内にて大小比較の関係にある（大小比較記号で結ばれている）」ならば、Ｆｌａｇ（Ａ）「Ａは（異常などの）判定フラグであり、単位はなし」、かつＳａｍｅＡｔｔｒ（Ｘ，Ｙ）であることを意味している。なお、フラグＡの判定対象とするデータ種別は、例えば変数Ｘのデータ種別とする。

推論ルールテーブル８１の推論ルールＮｏ．３にて、Ｘ，Ｙ，Ｚはある変数を示しており、Ｄｅｆ（Ｘ，Ｙ，Ｚ）「ＸとＹがＺを定義している」かつ、Ｍｕｌ（Ｘ，Ｙ）「ＸとＹとは演算式内にて乗算の関係にある（乗算記号で結ばれている）」ならば、ＭｕｌＡｔｔｒ（Ｘ，Ｙ，Ｚ）「Ｚのデータ種別はＸ（またはＹ）と同じであり、かつ、Ｚの単位はＸとＹの単位を乗じたもの」であることを意味している。同様に、和差算、除算についても推論ルールを記述することができる。

推論ルールテーブル８１の推論ルールＮｏ．４にて、Ｘ，Ｙはある変数を示しており、Ｃｏｍｐ（Ｘ，Ｙ）かつ、Ｖａｃａｎｔ（Ｙ）「Ｙの属性が空」ならば、Ｔｈｒｓｈ（Ｙ）「Ｙのデータ種目は『閾値』である」であることを意味している。ただし、Ｔｈｒｓｈ（Ｙ）に「？」が付いているのは、確定でないことを意味している。なお、閾値Ｙのデータ種別は、変数Ｘのデータ種別とする。

推論ルールテーブル８１の推論ルールＮｏ．５にて、Ｘ，Ｙ，Ｚはある変数を示しており、Ｄｅｆ（Ｘ，Ｙ，Ｚ）かつ、Ｖａｃａｎｔ（Ｙ）ならば、ＳａｍｅＡｔｔｒ（Ｘ，Ｚ）であることを意味している。ただし、ＳａｍｅＡｔｔｒ（Ｘ，Ｚ）に「？」が付いており、確定でないことを意味している。

推論ルールテーブル８１の推論ルールＮｏ．６にて、Ｙ，Ａはある変数を示しており、推論ルールＮｏ．２の前件が成立し、かつＥｒｒＴｈｒｓｈ（Ｙ）「Ｙが異常閾値」ならば、ＥｒｒＦｌａｇ（Ａ）「Ａは異常判定フラグ（異常を示すフラグ）」であることを意味している。前件に推論ルールＮｏ．２を用いているので、Ｎｏ．６が優先されるとする。つまり、Ｆｌａｇ（Ａ）よりＥｒｒＦｌａｇ（Ａ）の適用が優先される。

図９は、変数依存関係グラフ６１のノードと対応付けられた変数属性テーブル９１を示しており、図３の処理を１回実行した後の値が入っている。変数属性テーブル９１の項目は、変数名、単位、データ種別からなる。

変数属性テーブルにおいて、変数は実体で区別されており、記述位置では区別されていない。このため、変数依存関係グラフ６１のノードと、変数属性テーブル９１の行とは、ｎ：１対応となっている。例えば変数ｓｔｒｏｋｅについて、変数依存関係グラフ６１には対応するノードが２つあるが、変数属性テーブル９１には対応する行は１つのみである。

以下では、変数属性解釈部２５が推論処理により変数属性テーブル９１を生成する過程を説明する。変数属性解釈部２５は、依存関係解析部２２から変数依存関係グラフ６１のデータを受け取り、変数依存関係グラフ６１に含まれる変数から、変数属性テーブル９１のデータ構造を生成する。この時点で、変数属性テーブル９１には変数名のみが入っており、残りのデータは空である。各変数の属性情報の更新を示すフラグ（変数属性テーブル９１に記載なし）はクリアする。

次に変数属性解釈部２５は、変数依存関係グラフ６１に含まれる変数の属性情報を、変数属性データベース２４の変数属性テーブル７１から取得する。ただし本実施例では、入力用変数の属性情報のみを取得する。すると、変数ｒｅｇ＿ａｄ＿１に関する属性情報が取得されるので、変数属性テーブル９１に値を入れる。この際、変数ｒｅｇ＿ａｄ＿１の属性情報の更新を示すフラグをセットする。

次に変数属性解釈部２５は、変数依存関係グラフ６１の推論始端となる変数を抽出する。全ノードについて、依存元となる変数の有無を判定し、無いと判定されたノードだけ残すと、変数ｓｔｒｏｋｅ（Ｌ２０＠ｃｏｎｔｒｏｌ）が抽出される。この変数に対して、変数属性解釈部２５は図４の「属性推論」処理を行う。

変数ｓｔｒｏｋｅ（Ｌ２０＠ｃｏｎｔｒｏｌ）に対して「属性推論」処理が実行されると、「属性推論」は再帰的な処理となっているため、変数依存関係グラフ６１の全ノードに対して「属性推論」処理が実行される。変数ｒｅｇ＿ａｄ＿１（Ｌ７＠ｉｎｐｕｔ）は、依存先変数を持たないので、属性情報が保持される。この属性情報は、変数属性テーブル７１から取得した値と同じである。

次に、変数ｓｔｒｏｋｅ＿ｒａｗ（Ｌ７＠ｉｎｐｕｔ）に対して、ステップ４２〜４５の処理が実行される。依存先変数のｒｅｇ＿ａｄ＿１（Ｌ７＠ｉｎｐｕｔ）は、変数属性テーブル７１から値を取得したことで、属性情報が更新されているので、推論ルールテーブル８１から合致する推論ルールが検索される。合致する推論ルールとしてＮｏ．１が抽出され（推論ルールのＸがｒｅｇ＿ａｄ＿１，Ｙがｓｔｒｏｋｅ＿ｒａｗ）、ｓｔｒｏｋｅ＿ｒａｗの属性は、ｒｅｇ＿ａｄ＿１と同じ内容に更新される。

同様に他の変数の属性情報も更新していく。変数ｓｔｒｏｋｅ＿ｒａｗ（Ｌ１６＠ｃｏｎｖｅｒｔ）と変数ｓｔｒｏｋｅ＿ｒａｗ（Ｌ１０＠ｃｈｅｃｋ）は、変数ｓｔｒｏｋｅ＿ｒａｗ（Ｌ７＠ｉｎｐｕｔ）とデータ依存関係なので、属性情報は更新しない（更新済みである）。

変数ｓｔｒｏｋｅ＿ｍａｘ（Ｌ１０＠ｃｈｅｃｋ）は、推論ルールテーブル８１の推論ルールＮｏ．４に合致するので、データ種別は「ストローク量に対する閾値」、単位は「（Ａ／Ｄ変換値）」と判定される。ただし確定ではないので、属性値に「？」が付いている。

変数ｅｒｒ＿ｓｔｒｏｋｅ（Ｌ１１＠ｃｈｅｃｋ）は、推論ルールテーブル８１の推論ルールＮｏ．２に合致する（推論ルールのＸがｓｔｒｏｋｅ＿ｒａｗ，Ｙがｓｔｒｏｋｅ＿ｍａｘ，Ａがｅｒｒ＿ｓｔｒｏｋｅ）ので、後件のＦｌａｇ（Ａ）から、ｅｒｒ＿ｓｔｒｏｋｅの属性情報について、データ種別はストローク量に対する判定フラグであり、判定フラグなので単位はなしに更新される。またＳａｍｅＡｔｔｒ（Ｘ，Ｙ）から、ｓｔｒｏｋｅ＿ｍａｘの属性は、ｓｔｒｏｋｅ＿ｒａｗと同じ内容に更新される。

変数ｅｒｒ＿ｓｔｒｏｋｅ（Ｌ１５＠ｃｏｎｖｅｒｔ）はｅｒｒ＿ｓｔｒｏｋｅ（Ｌ１１＠ｃｈｅｃｋ）とデータ依存関係なので、属性情報は更新しない。

変数ｓｔｒｏｋｅ（Ｌ１６＠ｃｏｎｖｅｒｔ）は、推論ルールテーブル８１の推論ルールＮｏ．３に合致する（推論ルールのＸがｓｔｒｏｋｅ＿ｒａｗ，Ｙがｃ＿ｉｎ＿ｓｔｒｏｋｅ，Ｚがｓｔｒｏｋｅ）。しかし、ｃ＿ｉｎ＿ｓｔｒｏｋｅの属性情報が空であり不明なので、推論を進めることはできない。その一方で、推論ルールＮｏ．５にも合致するので、ｓｔｒｏｋｅデータ種別は「ストローク量」と判定される。ただし確定ではないので、属性値に「？」が付いている。

以上で、図３の処理を終了する。同様にして、出力用変数の属性情報をもとに、後ろ向きに推論を進めてもよい。

以上のようにして、一部の変数の属性情報から、他の変数の属性情報を自動的に推論することができ、ユーザが手作業で変数の依存関係を追跡し、属性情報を解釈していくより、短い時間で変数の属性情報を得ることができる。

図１０は、ユーザからの変数属性情報の入力を受けて図３の推論処理を再度実行し、変数属性テーブル９１を更新した変数属性テーブル１０１を示している。

変数属性テーブル９１の値が推論処理により導出された後で、ユーザが変数属性入力部２３に対し、変数ｓｔｒｏｋｅ＿ｍａｘのデータ種別が「異常閾値」、単位が「（Ａ／Ｄ変換値）」であると入力する。これらの属性値は、データ種別と単位と、それぞれに取りうる値が用意されており、候補としてリスト表示される。ユーザは表示装置１３上でリストを目視し、入力装置１２から選択の上、確定させる。検証モデル生成プログラム１１３１内では、データ種別の候補として、「閾値」や「異常閾値」などが予め定義されている。また、「異常閾値」は「閾値」の下位概念であると定義されている。このため、変数ｓｔｒｏｋｅ＿ｍａｘのデータ種別が「閾値」のときは、リスト上で現在の値として「閾値」が選択状態にあり、その次の候補として下位概念である「異常閾値」がリスト上で順に表示される。

ユーザが属性情報の入力を確定させると、検証モデル生成プログラム１１３１は図３の推論処理を実行する。すると変数ｅｒｒ＿ｓｔｒｏｋｅの属性情報が、推論ルールＮｏ．６により更新され、データ種別は「ストローク量の異常判定フラグ」となる。

さらにユーザが変数ｃ＿ｉｎ＿ｓｔｒｏｋｅの属性情報として、データ種別を「係数」、単位を「ｃｍ／（Ａ／Ｄ変換値）」と入力して確定させると、検証モデル生成プログラム１１３１は図３の推論処理を実行し、変数ｓｔｒｏｋｅの属性情報が推論ルールＮｏ．３により更新され、データ種別は「ストローク量」、単位は「ｃｍ」となる。単位を示すデータは、分子と分母とそれぞれに要素を用意して、分子と分母で重複するものを除去すればよい。なお、単位系の演算規則は、推論ルールテーブル８１と同様に、検証モデル生成プログラム１１３１内に定義しておくものとする。

以上のようにして、ユーザが変数の属性情報を追加入力することで、属性情報を推論できる変数の個数を増やし、全変数に対する割合を向上させることができるので、ユーザが手作業で変数の属性情報を解釈するより、さらに短い時間で変数の属性情報を得ることができる。
図１１は、検証モデル生成プログラム１１３１の機能構成を示しており、これらの機能は図２の基本機能構成と併せて動作する。

依存関係限定部１１１は、依存関係解析部２２から解析対象のソースコードに関する依存関係情報を受け取り、依存関係情報に含まれる各変数について個別に、ソースコード抽出時に残すか否かのデータ（残存設定データ）と対応付けて管理する。残存設定データは２値（Ｔｒｕｅ；残す、Ｆａｌｓｅ；残さない）で示され、依存関係情報のうちソースコード抽出に利用する範囲を限定する意味がある。残存設定データの初期値は、例えば全変数についてＴｒｕｅとする。また依存関係解析部２２は、ユーザ入力や外部環境モデル選択部１１６からの指定を受けて、残存設定データを変更する。

依存関係情報において、ソースコード抽出時に残る設定となっている変数と、残らない設定となっている変数とに依存関係があるとき、残る変数がソフトウェアモデルと外部環境モデルとの境界になる。以下、このような変数を境界変数と呼ぶ。例えば変数依存関係グラフ６１において、ｓｔｒｏｋｅ＿ｒａｗ（Ｌ７＠ｉｎｐｕｔ）を残すと設定し、ｒｅｇ＿ａｄ＿１（Ｌ７＠ｉｎｐｕｔ）を残さないと設定したとき、ｓｔｒｏｋｅ＿ｒａｗ（Ｌ７＠ｉｎｐｕｔ）は境界変数である。

依存関係解析部２２の残存設定データに対する、ユーザ入力や外部環境モデル選択部１１６からの指定内容は、各変数の残存設定でもよいし、境界に指定する変数でも良い。例えばｓｔｒｏｋｅ＿ｒａｗ（Ｌ７＠ｉｎｐｕｔ）を入力側の境界変数に指定するとき、ｓｔｒｏｋｅ＿ｒａｗ（Ｌ７＠ｉｎｐｕｔ）の残存設定はＴｒｕｅとなり、ｒｅｇ＿ａｄ＿１（Ｌ７＠ｉｎｐｕｔ）の残存設定はＦａｌｓｅとなる。

ソースコード抽出部１１２は、ファイル入力部２１から解析対象のソースコードを受け取り、依存関係限定部１１１による依存関係情報とその残存設定データとに基づいて、ソースコードの抽出（スライシング）を行う。抽出したソースコードはファイルに出力する。スライシングの方法として例えば、ソースコードを構文解析した後、依存関係情報に含まれる変数のうち、残存設定がＴｒｕｅの変数が記述されているステートメント、およびそのステートメントを包含する構文（関数など）、関連する構文（変数宣言など）を残し、それ以外のコードを除去する。

モデル変換部１１３は、ソースコード抽出部１１２が出力するスライシング後のソースコードを、モデル検査器が扱えるモデル記述言語に変換する。例えばＳＰＩＮ（Ｓｉｍｐｌｅ Ｐｒｏｍｅｌａ ＩＮｔｅｒｐｒｉｔｅｒ）というモデル検査器では、モデル記述言語はＰｒｏｍｅｌａである。モデル変換の方法として、ソースコードを構文解析した後、ソースコードの構文から、モデル記述言語の構文へ変換する規則に基づいて各構文を変換する。この変換規則は予め用意しておく。変換により得られるモデルは、検査対象となるソフトウェアに関する検証用モデルであり、検査対象となるシステムに関する検証用モデルの部品である。

外部環境モデルデータベース１１４は、検証対象となるソフトウェアの外部環境について予めコーディングまたは自動コード生成用にテンプレート化されたモデル部品について、属性と紐付けられて記憶されている。外部環境モデル候補抽出部１１５は、依存関係限定部１１１から残存設定データと対応付けられた依存関係情報を、変数属性解釈部２５から検証対象となるソフトウェアの各変数の属性情報を受け取り、残存設定がＴｒｕｅとなっている変数の属性情報の一部（データ項目や単位など）を検索キーとして、インタフェースが合致する外部環境モデルを、外部環境モデルデータベース１１４より抽出する。抽出された外部環境モデルは、検証対象となるソフトウェアの外部環境となりうるモデルである。

外部環境モデル選択部１１６は、外部環境モデル候補抽出部１１５により抽出された外部環境モデルの属性（名称等）を、ユーザに対して表示装置１３を用いてリスト表示し、ユーザからの各外部環境モデルの利用有無について、入力装置１２から指定を受け付ける。利用有無は、デフォルトでは「なし」である。ユーザが外部環境モデルの１つについて、利用有無を「あり」に指定すると、選択された外部環境モデルのインタフェースとなっている変数の属性情報が、依存関係限定部１１１に渡され、依存関係限定部１１１は検証対象となるソフトウェアの変数のうち、外部環境モデルのインタフェース変数と属性が合致する変数を依存関係情報から検索し、境界変数として残存設定を変更する。具体的には、境界変数は残す設定とする。インタフェース変数が入力のとき、境界変数から依存元方向（より出力に近い方）の変数は、残らない設定の変数を残る設定に変更する（例えば残存設定がＴｒｕｅの変数が出現するまで）。また、境界変数から依存先方向（より入力に近い方）の変数は、残らない設定とする。インタフェース変数が出力のときには、入力のときと残存設定の変更が逆になる。なお外部環境モデル選択部１１６は、利用有無が「あり」に指定された外部環境モデルをファイルに出力してもよい。

モデル合成部１１７は、モデル変換部１１３が出力するソフトウェアモデルと、外部環境モデル選択部１１６にて利用ありに指定された外部環境モデルとから、検証対象となるシステムの検証モデルを合成する。この際、外部環境モデルのインタフェース変数と、対応するソフトウェアの境界変数とで、一致しない属性情報がある場合、外部環境モデルのインタフェース変数の属性情報を変更する。例えば、インタフェース変数の名称を、境界変数の名称と同一に変更する。合成された検証モデルは、ハードディスク１４にファイルとして出力される。

図１２は、検証モデル生成プログラム１１３１が図２や図１１に示された機能を用いて行う処理であり、システムの検証モデルを生成する処理のフローを示している。

処理を開始すると、ステップ１２１にて、検証モデル生成プログラム１１３１は、図３の処理を行い、検証対象となるソフトウェアの依存関係情報を生成する。依存関係解析部２２から、依存関係限定部１１１に、依存関係情報が渡されて管理される。

ステップ１２２にて、外部環境モデル候補抽出部１１５は、ステップ１２１にて出力された依存関係情報をもとに、外部環境モデルデータベース１１４から外部環境モデルの候補を抽出する。

ステップ１２３にて、検証モデル生成プログラム１１３１は、入力装置１２からのユーザ入力を確認する。ユーザ入力がある変数の残存設定を変更するものであれば、ステップ１２４に進む。ユーザ入力が外部環境モデル候補抽出部１１５の抽出したある外部環境モデルの利用有無設定を変更するものであれば、ステップ１２５に進む。ユーザ入力がシステムの検証モデル合成を指示するものであれば、ステップ１２７に進む。

ステップ１２４にて、依存関係限定部１１１は、ユーザ入力に従って依存関係情報における各変数の残存設定を変更し、ステップ１２２に戻る。ステップ１２２では、各変数の残存設定の変更に対応して、外部環境モデル候補の抽出を再度実行する。

ステップ１２５にて、外部環境モデル選択部１１６は、ユーザ入力に従って各外部環境モデルの利用有無設定を変更し、ステップ１２６に進む。ステップ１２６にて、依存関係限定部１１１は、ステップ１２５にて利用ありと設定された外部環境モデルの、インタフェース変数の属性から、検証対象となるソフトウェアにて対応する境界変数を検索し、依存関係情報における各変数の残存設定を変更する。変更が完了したら、ステップ１２３に戻る。

ステップ１２７にて、ソースコード抽出部１１２は、変数の残存設定を付与された依存関係情報を利用してソースコードの抽出を行う。ステップ１２８にて、モデル変換部１１３は、ステップ１２７にて抽出されたソースコードを、ソフトウェアの検証用モデルに変換する。ステップ１２９にて、モデル合成部１１７は、ステップ１２８にて出力されたソフトウェアの検証モデルと、ステップ１２５にて利用ありと設定された外部環境モデルとから、システムの検証モデルを合成して出力する。以上により処理を終了する。

図１３の外部環境モデル属性テーブル１３１は、外部環境モデルデータベース１１４に記録されている外部環境モデルに関する属性情報の例であり、このテーブルも外部環境モデルデータベース１１４に記録されている。変数属性テーブル１３１の１行は１つの外部環境モデルに紐付いており、項目は外部環境モデル名、インタフェース変数名、ｉｎ／ｏｕｔ（インタフェース変数が入力か出力か）、（インタフェース変数の）単位、（インタフェース変数の）データ種別、（外部環境モデルの）抽象度からなる。これらの値は予め設定されている。

外部環境モデル属性テーブル１３１には、Ｓｔｒｏｋｅ１、Ｓｔｒｏｋｅ２、Ｓｔｒｏｋｅ３の３つの外部環境モデルが登録されており、どれもインタフェース変数のデータ種別は「ストローク量」、入出力は「入力」である。一方で、インタフェース変数の単位は、Ｓｔｒｏｋｅ１とＳｔｒｏｋｅ２が「（Ａ／Ｄ変換値）」、Ｓｔｒｏｋｅ３は「ｃｍ」となっている。

外部環境モデル候補抽出部１１５は、図１０の変数属性テーブル１０１を変数属性解釈部２５から受け取り、外部環境モデル属性テーブル１３１とデータ種別および単位が合致する外部環境モデルを抽出する。すると、変数ｒｅｇ＿ａｄ＿１とｓｔｒｏｋｅ＿ｒａｗに対してはＳｔｒｏｋｅ１とＳｔｒｏｋｅ２が、変数ｓｔｒｏｋｅに対してはＳｔｒｏｋｅ３が抽出され、外部環境モデル選択部１１６にその属性情報と共に渡される。

また依存関係限定部１１１は、外部環境モデル選択部１１６から、Ｓｔｒｏｋｅ１〜Ｓｔｒｏｋｅ３のうち、ユーザに利用ありと設定された外部環境モデルのインタフェース変数に関する属性情報を受け取り、依存関係情報における各変数の残存設定を変更する。例えばユーザがＳｔｒｏｋｅ３を利用ありに設定したとき、そのインタフェース変数のデータ種別「ストローク量」と単位「ｃｍ」が依存関係限定部１１１に渡され、依存関係限定部１１１は対応する変数ｓｔｒｏｋｅを境界変数として扱う。

図１４の検証用モデル１４０は、検証対象システムについてモデル合成部１１７が出力する検証用モデルの例である。なお検証用モデル１４０を出力する前提として、外部環境モデル選択部１１６では外部環境モデルとしてＳｔｒｏｋｅ３がユーザ入力により利用ありに設定されており、依存関係限定部１１１ではユーザ入力により変数ｅｒｒ＿ｓｔｒｏｋｅの残存設定がＦａｌｓｅにされているとする。またモデル合成部１１７が利用する変換ルールは、Ｃ言語の関数をＰｒｏｍｅｌａのインラインマクロに置換し、関数コールグラフにてどの関数からも呼び出しされていない関数に対応するインラインマクロを実行するプロセスを追加するとしている。

検証用モデル１４０は、４つの部分から成っている。検証用モデル部品１４１は、ソフトウェアモデルと外部環境用モデルにて使用されている変数や固定値の宣言を、モデル合成部１１７がまとめたものである。検証用モデル部品１４２は、外部環境モデルデータベース１１４に記録されている外部環境モデルＳｔｒｏｋｅ３のコードについて、インタフェース変数名を境界変数ｓｔｒｏｋｅの名称に変更したものである。検証用モデル部品１４３は、モデル変換部１１３が変換して出力したソフトウェアの検証用モデルについて、さらにモデル合成部１１７が、境界変数ｓｔｒｏｋｅ（１４行目）に値を代入する構文を、外部環境モデルＳｔｒｏｋｅ３のインラインマクロ呼び出しに置換したものである。このようなインラインマクロへの置換は、予め変換ルールとして決めておく。検証用モデル部品１４４は、モデル合成部１１７にて追加されたプロセスである。

以上のようにしてシステムの検証用モデルをプログラムが合成することにより、ユーザは外部環境モデルの選択に掛かる工数や、ソフトウェアモデルと外部環境モデルとの入出力を整合させる手間を低減させることができる。またさらに、ユーザがソフトウェアとその外部環境の双方をモデル化する作業に掛かる工数を低減することができる。

１１ コンピュータ
１１１ ＣＰＵ
１１２ ＲＡＭ
１１３ ＲＯＭ
１１３１ 検証モデル生成プログラム
１２ 入力装置
１３ 表示装置
１１４ ハードディスク
２１ ファイル入力部
２２ 依存関係解析部
２３ 変数属性入力部
２４ 変数属性データベース
２５ 変数属性解釈部
２６ 推論ルールデータベース
２７ 変数属性表示部

Claims (7)

1. コンピュータにソフトウェアのソースコードを入力させ、前記ソフトウェアの検証を行うためのソフトウェア検証用プログラムにおいて、
   前記ソースコードに対して命令または変数の依存関係を導出する依存関係解析部と、
   前記ソースコードの一部の変数について属性情報を記録する変数属性記録部と、
   前記依存関係と前記属性情報から、前記ソースコード中の各変数について、予め設定された推論ルールに従って属性情報を推論する変数属性解釈部と、
   前記属性情報を表示する属性情報表示部と、
   外部環境モデルをその属性情報と共に記録する外部環境モデルデータベースと、
   前記外部環境モデルデータベースから、前記ソースコードを変換したソフトウェアモデルの外部環境となりうるモデルを抽出する外部環境モデル抽出部と、を備え、
   前記外部環境モデル抽出部は、前記依存関係に含まれる属性情報から、インタフェースの属性が合致する外部環境モデルを検索して、前記ソフトウェアモデルに接続可能な外部環境モデルの候補として出力することを特徴とするソフトウェア検証用システム。
2. ユーザによる属性情報の入力を受け付ける変数属性入力部を備え、
   前記変数属性解釈部は、前記ソースコードの各変数に関する属性情報の推論に、前記変数属性入力部に入力された属性情報を利用することを特徴とする請求項１記載のソフトウェア検証用システム。
3. 前記依存関係についてソースコード抽出のための命令または変数の残存設定の変更をユーザから受け付ける依存関係限定部を備え、
   前記外部環境モデル抽出部は、前記依存関係限定部により残存設定が変更された前記依存関係にもとづき、前記インタフェースと属性が合致する変数としては前記残存設定が残る様に設定されている変数のみを用い、前記外部環境モデルデータベースから抽出する外部環境モデルの候補を絞り込むことを特徴とする請求項１記載のソフトウェア検証用システム。
4. 前記依存関係についてソースコード抽出のための命令または変数の残存設定を変更する依存関係限定部を備え、
   前記外部環境モデル抽出部は前記外部環境モデルデータベースから抽出された外部環境モデルに対するユーザによる選択を受け付け、ユーザが前記外部環境モデルを選択すると、前記依存関係限定部は、選択された前記外部環境モデルの属性情報からインタフェースが合致する変数を前記依存関係から検索し、前記ソースコードを変換したソフトウェアモデルと、前記外部環境モデルとの境界となる変数として、前記依存関係の残存設定を変更することを特徴とする、請求項３記載のソフトウェア検証用システム。
5. 前記依存関係から前記ソースコードの一部を抽出するソースコード抽出部と、前記ソースコード抽出部によるソースコードを変換してソフトウェアモデルとするモデル変換部と、
   前記モデル変換部によるソフトウェアモデルと前記外部環境モデル抽出部による外部環境モデルとを合成して、前記ソフトウェアを含むシステムの検証用モデルを出力するモデル合成部と、を備え、
   前記モデル合成部は、前記ソフトウェアモデルと、前記外部環境モデルとのインタフェースについて両者が整合するように修正を行うことを特徴とする請求項３から５いずれか一項に記載のソフトウェア検証用システム。
6. 前記変数属性解釈部は、前記依存関係中で、どの変数からも依存されていない変数を始端変数として選択し、依存先の変数から依存元の変数へと属性情報の推論を行うことを特徴とする請求項１記載のソフトウェア検証用システム。
7. 前記変数属性解釈部は、前記依存関係中にループがあるときに、一度属性情報の推論を行った前記ループに属する変数については、推論の対象外とすることを特徴とする請求項１記載のソフトウェア検証用システム。