(57)【特許請求の範囲】
【請求項１】
ソフトウェアのソースコードを、異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換するソースコード変換装置で実行されるソースコード変換方法であって、
前記異なる複数の変換ルールは、前記ソースコードを前記検査コードへ変換し抽象化する一連の処理を、細粒度に分割したものであり、
前記変換ルールは、
前記ソースコードを特定のプログラミング言語に依存しない形式である中間形式へ変換する第１変換ルールと、
前記変換された中間形式を抽象化する第２変換ルールと、
前記抽象化された中間形式を前記検査コードに変換する第３変換ルールと、を含み、
前記方法は、
前記ソースコードを入力するステップと、
少なくとも一つの前記第１変換ルールの入力を受け付けるステップと、
少なくとも一つの前記第２変換ルールの入力を受け付けるステップと、
少なくとも一つの前記第３変換ルールの入力を受け付けるステップと、
前記入力された第１変換ルールを用いて、前記ソースコードを前記中間形式へ変換するステップと、
前記入力された第２変換ルールを用いて、前記変換された中間形式を抽象化するステップと、
前記入力された第３変換ルールを用いて、前記抽象化された中間形式を前記検査コードへ変換するステップと、を含み、
前記中間形式は、前記ソースコード又は前記検査コードの要素と等価な要素である物理要素の他に、前記変換された中間形式を抽象化するステップで生成される要素である論理要素を表現可能であることを特徴とするソースコード変換方法。
【請求項２】
請求項１に記載のソースコード変換方法において、
前記論理要素は、関連する物理要素への参照及び任意の情報を含み、
前記変換された中間形式を抽象化するステップは、前記第２変換ルールで定められた所定の条件と合致する要素を前記論理要素に変換することによって、追加の属性情報を付与するステップを含み、
前記検査コードに変換するステップは、前記論理要素を前記検査コードの要素と等価な要素に変換するステップを含むことを特徴とするソースコード変換方法。
【請求項３】
請求項１又は請求項２に記載のソースコード変換方法において、
前記変換された中間形式を抽象化するステップは複数回実行可能であって、
ある回の前記ソフトウェアを抽象化するステップで生成された論理要素は、当該回よりも後の回の前記ソフトウェアを抽象化するステップで新たな論理要素に変換されることを特徴とするソースコード変換方法。
【請求項４】
請求項１から請求項３のいずれか一つに記載のソースコード変換方法において、
前記第１変換ルール、前記第２変換ルール、及び前記第３変換ルールの少なくとも一つは、前記ソースコード変換装置の内部に蓄積された複数の変換ルールの中から選択されることによって、入力が受け付けられることを特徴とするソースコード変換方法。
【請求項５】
請求項１から請求項４のいずれか一つに記載のソースコード変換方法において、
前記第１変換ルール、前記第２変換ルール、及び前記第３変換ルールの少なくとも一つは、利用者の記述によって入力が受け付けられることを特徴とするソースコード変換方法。
【請求項６】
ソースコード変換装置によるソースコード変換方法であって、
ソフトウェアのソースコードを入力するステップと、
異なる複数の変換ルールを入力するステップと、
前記ソースコードを、前記異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換するステップと、を含み、
前記複数の変換ルールの少なくとも一部は、前記ソースコード変換装置の内部に蓄積された複数の変換ルールの中から選択して入力され、
前記異なる複数の変換ルールは、前記ソースコードを、該ソースコードの記述言語に依存しない汎化されたプログラム情報をもつ汎化モデルへ変換する実装−汎化変換ルールと、前記汎化モデルを抽象化する抽象化変換ルールと、前記抽象化された汎化モデルを前記検査コードへ変換する汎化−検査変換ルールとを含み、
前記ソースコードを前記検査コードに変換するステップは、
前記実装−汎化変換ルールを用いて、前記ソースコードを前記汎化モデルへ変換するステップと、
前記抽象化変換ルールを用いて、前記汎化モデルを抽象化するステップと、
前記汎化−検査変換ルールを用いて、前記抽象化された汎化モデルを前記検査コードに変換するステップと、を含み、
前記ソースコードを前記検査コードへ変換する一連のステップにおいて、内部的に保持される情報であるモデルの形式はメタモデルによって定義され、
前記モデルは、前記ソースコードに対応する情報をもつ実装モデルと、前記汎化モデルと、前記検査コードに対応する情報をもつ検査モデルとを含み、
前記実装モデルは、そのメタモデルであるメタ・実装モデルによって定義され、
前記汎化モデルは、そのメタモデルであるメタ・汎化モデルによって定義され、
前記検査モデルは、そのメタモデルであるメタ・検査モデルによって定義され、
前記各メタモデルは、データ構造の定義と、データに含まれる要素間の制約に関する情報とを保持し、
前記メタ・汎化モデルは、前記メタ・実装モデルの要素に等価な要素である第１物理要素の定義と、前記メタ・検査モデルの要素に等価な要素である第２物理要素の定義と、前記抽象化変換ルールを用いて前記汎化モデルを抽象化するステップで生成される要素である論理要素の定義と、を含むことを特徴とするソースコード変換方法。
【請求項７】
請求項６に記載のソースコード変換方法において、
前記メタ・汎化モデルでは、前記メタ・汎化モデルで定義される前記論理要素が、前記メタ・汎化モデルで定義される前記第１物理要素又は前記第２物理要素を継承するように定義されることを特徴とするソースコード変換方法。
【請求項８】
請求項６又は請求項７に記載のソースコード変換方法において、
前記論理要素は、関連する物理要素への参照及び任意の情報を含み、
前記汎化モデルを抽象化するステップは、前記抽象化変換ルールで定められた所定の条件と合致する要素を前記論理要素に変換することによって、追加の属性情報を付与するステップを含み、
前記汎化モデルを前記検査コードに変換するステップは、前記論理要素を前記検査コードの要素と等価な要素に変換するステップを含むことを特徴とするソースコード変換方法。
【請求項９】
請求項６から請求項８のいずれか一つに記載のソースコード変換方法において、
前記汎化モデルを前記検査コードに変換するステップは複数回実行可能であって、
ある回の汎化モデルを抽象化するステップで生成された論理要素は、当該回よりも後の回の前記汎化モデルを抽象化するステップで新たな論理要素に変換されることを特徴とするソースコード変換方法。
【請求項１０】
請求項６から請求項９のいずれか一つに記載のソースコード変換方法において、
前記変換ルールに関する情報は、ソースコード変換装置の記憶部に格納された変換ルールを指し示す識別情報のみが含まれており、
前記変換ルールの実体を、前記識別情報を用いて前記記憶部から取り出し、前記取り出された変換ルールの実態を変換に用いることを特徴とするソースコード変換方法。
【請求項１１】
請求項６から請求項１０のいずれか一つに記載のソースコード変換方法において、
前記入力されたソースコードから、前記変換ルールの検索条件を抽出又は生成し、
前記検索条件と合致する変換ルールを、ソースコード変換装置の記憶部から取得し、前記取得された変換ルールを前記変換ルールとして受け付けることを特徴とするソースコード変換方法。
【請求項１２】
請求項６から請求項１１のいずれか一つに記載のソースコード変換方法において、
前記実装モデル、前記汎化モデル、及び前記検査モデルの各中間のモデルは、それぞれ構文を定義するメタモデルによってデータ構造と意味論が定義されることを特徴とするソースコード変換方法。
【請求項１３】
プロセッサ及び記憶領域を備えるソースコード変換装置に、ソフトウェアのソースコードを、異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換する処理を実行させるソースコード変換プログラムであって、
前記異なる複数の変換ルールは、前記ソースコードを前記検査コードへ変換し抽象化する一連の処理を、細粒度に分割したものであり、
前記変換ルールは、
前記ソースコードを特定のプログラミング言語に依存しない形式である中間形式へ変換する第１変換ルールと、
前記変換された中間形式を抽象化する第２変換ルールと、
前記抽象化された中間形式を前記検査コードへ変換する第３変換ルールと、を含み、
前記処理は、
前記ソースコードを入力するステップと、
少なくとも一つの前記第１変換ルールの入力を受け付けるステップと、
少なくとも一つの前記第２変換ルールの入力を受け付けるステップと、
少なくとも一つの前記第３変換ルールの入力を受け付けるステップと、
前記入力された第１変換ルールを用いて、前記ソースコードを前記中間形式へ変換するステップと、
前記入力された第２変換ルールを用いて、前記変換された中間形式を抽象化するステップと、
前記入力された第３変換ルールを用いて、前記抽象化された中間形式を前記検査コードへ変換するステップと、を含み、
前記中間形式は、前記ソースコード又は前記検査コードの要素と等価な要素である物理要素の他に、前記変換された中間形式を抽象化するステップで生成される要素である論理要素を表現可能であることを特徴とするソースコード変換プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソースコード変換方法及びソースコード変換プログラムに係り、特に、ソフトウェアのモデル検査において、モデルチェッカの入力言語で検査コードを記述するコストを低減させるために、計算機を活用してソフトウェアのソースコードを検査コードに変換する方法に関する。
【背景技術】
【０００２】
近年、ソフトウェアシステムが一般社会に浸透し、ソフトウェアに求められる信頼性が非常に高くなってきている一方で、ソフトウェアは複雑化及び大規模化の一途をたどっており、手作業でのレビュー、及びテストによる品質確保が非常に困難になってきている。
【０００３】
モデル検査技術は、ソフトウェアの振舞いを、特定モデルチェッカの入力言語で記述し、特定モデルチェッカを実行することで、前記ソフトウェアの取り得る状態を網羅的に検査することによって前記ソフトウェアが持つべき性質を満たしているかどうかを判定する技術である（例えば非特許文献１参照）。非特許文献１に開示される方法によると、ソフトウェアの振る舞いを、Ｐｒｏｍｅｌａと呼ばれる入力言語で記述し、SPINと呼ばれるモデルチェッカに入力することで、検査を実施する。
【０００４】
モデル検査技術は複雑化及び大規模化の一途をたどるソフトウェアの品質確保に有望な技術であるが、ソフトウェアの取り得る状態を網羅的に検査するため、規模の大きなソフトウェアでは、検査すべき状態数が膨大な分量となる状態爆発と呼ばれる現象が起きる。この状態爆発によって、処理に必要な時間計算量が現実的に許容不可能な大きさとなる現象、及び、処理に必要な空間計算量が処理に用いる計算機に搭載された記憶領域を超える現象の、少なくとも一方が引き起こされ、上述した検査を完了できない場合があり得る。
【０００５】
状態爆発に対応するために、抽象化と呼ばれる処理を、ソースコード又は検査コードに対して行い、状態数を検査可能な範囲まで削減することがある。抽象化は、例えば、選択的実行文の分岐条件の簡略化がある。抽象化によって、本来存在しない実行パスが生じる事態、又は存在する実行パスが消滅する事態が引き起こされる場合があるため、検査コードに対する検査結果によって示されるソフトウェアの性質と本来のソフトウェアの性質とに差異が生まれることがあり得る。そのため、ソフトウェアに対して検査すべき性質に鑑み、抽象化の水準を検討した上で、抽象化を適用することが望ましい。
【０００６】
さらに、モデル検査技術は、検査対象のソフトウェアを、特定モデルチェッカの入力言語で記述する労力が大きいことが実用上の問題となることがあり得る。図３５に、特許文献１に開示されたソースコード変換装置の一例を示す。特許文献１に開示される方法によると、ソースコードは、特定モデルチェッカの入力言語で書かれた検査コードへ、翻訳マップを用いて変換される（ステップ９１０〜９４０）。特許文献１に開示される方法によると、検査コードは、利用者によって定義された環境モデルを用いて、前記変換とは別に前記特定モデルチェッカによって検査される（ステップ９７５、ステップ９５０〜９７０）。
【０００７】
また、ソフトウェアの開発技術の一つとして、モデル駆動型開発がある。モデル駆動型開発は、ソフトウェアの設計情報をモデルとして記述し、そのモデルを変換操作により詳細化することで、ソフトウェア開発を進める技術である。例えば、モデル駆動型開発において、モデルのフォーマット及びモデルの意味はMOFにより記述されたメタモデルにより規定され（例えば、非特許文献２参照）、QVTによりモデルを詳細化する変換ルールが記述され（例えば、非特許文献３参照）、OCLによりモデルの整合性及び健全性に関する制約の記述並びに検証が行われ（例えば、非特許文献４参照）、MOFM2Tによりモデルからソースコードが生成される（例えば非特許文献５参照）。
【０００８】
なお、モデル検査技術における「モデル」と、モデル駆動型開発における「モデル」は、互いに独立した概念であり、一般にデータ構造及び意味などに関する共通性はない。
【先行技術文献】
【特許文献】
【０００９】
【特許文献１】特開２０００−１８１７５０号公報
【非特許文献】
【００１０】
【非特許文献１】G. J. Holzmann, "The Model Checker Spin," IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 279--295, May 1997http://doi.ieeecomputersociety.org/10.1109/32.588521
【非特許文献２】The Object Management Group, "Meta Object Facility (MOF) Core Specification", formal/06-01-01, January 2006, http://www.omg.org/spec/MOF/2.0/PDF
【非特許文献３】The Object Management Group , "Meta Object Facility (MOF) 2.0 Query/View/Transformation Specification", formal/2008-04-03, April 2008, http://www.omg.org/spec/QVT/1.0/PDF
【非特許文献４】The Object Management Group、"Object Constraint Language", formal/2006-05-01, May 2006, http://www.omg.org/spec/OCL/2.0/PDF
【非特許文献５】The Object Management Group, "MOF Model to Text Transformation Language, v1.0", formal/2008-01-16, January 2008, http://www.omg.org/spec/MOFM2T/1.0/PDF
【発明の概要】
【発明が解決しようとする課題】
【００１１】
モデル検査によるソフトウェアの信頼性確保を有効に実施するためには、ソースコードからモデルチェッカの入力言語で記述された検査コードを自動生成するなどの方法により、検査コードを得るための労力を低減させること、並びに、ソフトウェアの仕様及び設計を、モデルチェッカによる網羅的検査が現実的な時間計算量及び空間計算量で終了するように抽象化することが必要となる。
【００１２】
特許文献１に開示される方法によると、抽象化記述の再利用性が低いという課題が存在する。特許文献１に開示される方法によると、モデル検査に必要な抽象化の手段である、翻訳マップ及び環境モデルは、ソースプログラムの改訂など、新しいタイプの命令がソースコード内に導入された場合に限定されているが、現実の検査においては、（１）新しいタイプの命令の導入に限らない、ソフトウェアの設計変更（２）対象ソフトウェアの抽象化方法の変更（３）異なるモデルチェッカによる検査への対応の３種類の変更があり得る。
【００１３】
（１）の例としては、ソフトウェアの構造変更による、環境モデルとの対応付けの変更、及び、複数の命令をまたがる、手続きの変更があり得る。ソフトウェアは改訂ごとに構造変更が伴うことが多く、この種類の変更が頻繁に加わる。
【００１４】
また、（２）の例としては、乱数等を関数の定数又は非決定的な値への置き換え、及び処理の簡略がある。現実的なソフトウェアのモデル検査では状態爆発が容易に生じるため、検査項目に応じた抽象化、及び、検査水準自体の調整が必要となる。
【００１５】
（３）の例としては、異なる検査が可能なモデルチェッカへの変更、及び、もっと単純に、モデルチェッカのバージョン変更への対応があり得る。モデルチェッカはそれぞれに特長が存在するため、効果的な検査の為にはモデルチェッカの複数対応が望ましい。
【００１６】
特許文献１に開示される方法によると、上述した３種類の変更のいずれに対応する場合にも、ソースコードの言語からモデルチェッカの言語へのマップである翻訳マップと、モデルチェッカの言語で記述された環境モデルとの、少なくとも一方を修正しなければならない。そのため、ある目的１（例えば、抽象化方法の変更）の為の変更を行った上で、異なる目的２（例えば、設計変更）の為の変更を行った時、これらの変更前の翻訳マップ及び環境モデルに対し、目的２及び新たな目的３（例えば、モデルチェッカの変更）の変更を行おうとした場合、最初に行った目的２の為の変更を再利用できず、新たに目的２と目的３とを同時に満たす変更を行わなければならない。
【００１７】
本発明は、従来の技術の課題を踏まえ、抽象化記述の変更を柔軟に行うことができ、さらに、抽象化記述を効率的に再利用可能な、ソースコード変換方法及びソースコード変換プログラムを提供することを目的とする。
【課題を解決するための手段】
【００１８】
本発明の代表的な一例を示せば、ソフトウェアのソースコードを、異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換するソースコード変換装置で実行されるソースコード変換方法であって、前記異なる複数の変換ルールは、前記ソースコードを前記検査コードへ変換し抽象化する一連の処理を、細粒度に分割したものであり、前記変換ルールは、前記ソースコードを特定のプログラミング言語に依存しない形式である中間形式へ変換する第１変換ルールと、前記変換された中間形式を抽象化する第２変換ルールと、前記変換された中間形式を前記検査コードに変換する第３変換ルールと、を含み、前記方法は、前記ソースコードを入力するステップと、少なくとも一つの前記第１変換ルールの入力を受け付けるステップと、少なくとも一つの前記第２変換ルールの入力を受け付けるステップと、少なくとも一つの前記第３変換ルールの入力を受け付けるステップと、前記入力された第１変換ルールを用いて、前記ソースコードを前記中間形式へ変換するステップと、前記入力された第２変換ルールを用いて、前記変換された中間形式を抽象化するステップと、前記入力された第３変換ルールを用いて、前記変換された中間形式を前記検査コードへ変換するステップと、を含み、前記中間形式は、前記ソースコード又は前記検査コードの要素と等価な要素である物理要素の他に、前記変換された中間形式を抽象化するステップで生成される要素である論理要素を表現可能であることを特徴とする。
【発明の効果】
【００１９】
本願において開示される発明のうち代表的なものによって得られる効果を簡潔に説明すれば、下記の通りである。すなわち、抽象化記述の変更を柔軟に行うことができ、さらに、抽象化記述を効率的に再利用可能な、ソースコード変換方法及びソースコード変換プログラムを提供できる。
【図面の簡単な説明】
【００２０】
【図１】本発明の基本概念を説明するための図である。
【図２】本発明のソースコード変換処理における、変換ルールの入力インタフェースについて説明する図である。
【図３Ａ】本発明の第１の実施例になるソースコード変換システムの構成例を示す図である。
【図３Ｂ】図３Ａの変換システムにおけるソースコード変換装置の構成例を示す図である。
【図４】本発明の第１の実施例の処理フローの例を示す図である。
【図５Ａ】ソースコード変換装置に対する入力操作の一例を示す図である。
【図５Ｂ】ソースコード変換装置に対する入力操作の他の例を示す図である。
【図６】ソースコード変換装置の動作を説明する図である。
【図７】ソースコード変換の手順をより詳細に説明する図である。
【図８Ａ】モデルの抽象化の一例を示す図である。
【図８Ｂ】モデルの抽象化の一例を示す図である。
【図９】本発明の第一の実施例におけるメタ・実装モデルの一例を示す図である。
【図１０】本発明の第１の実施例におけるメタ・汎化モデルの一例を示す図である。
【図１１】本発明の第１の実施例におけるメタ・検証モデルの一例を示す図である。
【図１２】本発明の第１の実施例における第１の変換例におけるソースコードを示す図である。
【図１３】本発明の第１の実施例における第１の変換例における検査コードを示す図である。
【図１４】本発明の第１の実施例における第１の変換例における実装モデルを示す図である。
【図１５】本発明の第１の実施例における第１の変換例における最初の汎化モデルを示す図である。
【図１６】本発明の第１の実施例における第１の変換例における二番目の汎化モデルを示す図である。
【図１７】本発明の第１の実施例における第１の変換例における検査モデルを示す図である。
【図１８】本発明の第１の実施例における第２の変換例におけるソースコードを示す図である。
【図１９】本発明の第１の実施例における第３の変換例におけるソースコードを示す図である。
【図２０】本発明の第１の実施例における第２の変換例における実装モデルを示す図である。
【図２１】本発明の第１の実施例における第３の変換例における実装モデルを示す図である。
【図２２】本発明の第１の実施例における第２の変換例における最初の汎化モデルを示す図である。
【図２３】本発明の第１の実施例における第３の変換例における最初の汎化モデルを示す図である。
【図２４】本発明の第１の実施例における第４の変換例における検査コードを示す図である。
【図２５】本発明の第１の実施例における第４の変換例における検査モデルを示す図である。
【図２６】本発明の第１の実施例における第５の変換例におけるソースコードを示す図である。
【図２７】本発明の第１の実施例における第５の変換例における検査コードを示す図である。
【図２８】本発明の第１の実施例における第５の変換例における実装モデルを示す図である。
【図２９】本発明の第１の実施例における第５の変換例における最初の汎化モデルを示す図である。
【図３０】本発明の第１の実施例における第５の変換例における二番目の汎化モデルを示す図である。
【図３１】本発明の第１の実施例における第５の変換例における三番目の汎化モデルを示す図である。
【図３２】本発明の第１の実施例における第５の変換例における検査モデルを示す図である。
【図３３】本発明の第２の実施例になるソースコード変換装置の処理フローの例を示す図である。
【図３４】本発明の第３の実施例における、変換の妥当性の検証の手順を詳細に説明する図である。
【図３５】従来例のソースコード変換装置の一例を示す図である。
【発明を実施するための形態】
【００２１】
本発明では、異なる複数の変換ルールを用いて検査対象のソースコードをモデルチェッカの入力言語で記述された検査コードへ変換する。前記異なる複数の変換ルールは、検査対象のソースコードをモデルチェッカの入力言語で記述された検査コードへ変換し、抽象化する一連の処理を細粒度に分割したものであり、複数の変換ルールを組み合わせて用いることにより、前記ソースコードから前記検査コードへの変換が実現される。
【００２２】
本発明において、検査対象のソースコードを検査コードへ変換する一連の処理を、抽象化の処理も含めて、細粒度に分割し、分割されたそれぞれを、「変換ルール」と呼ぶ。本発明により実現されるソースコード変換装置は、ソースコードを検査コードへ変換する場合、異なる複数の変換ルールが、利用者によって、選択され、又は入力されるためのインタフェースを所有する。前記変換ルールは、事前にソースコード変換装置内部に蓄積された複数の変換ルールの中からの選択と、利用者の記述と、のいずれかの手段により入力される。
【００２３】
また、本発明において、変換ルールは、ソースコードを、前記ソースコードの記述言語に依存しない、汎化されたプログラム情報をもつ形式（汎化モデル）へ変換する実装−汎化変換ルールと、汎化モデルを抽象化する抽象化変換ルールと、汎化モデルをモデルチェッカの記述言語へ変換する汎化−検査変換ルールに分類される。換言すると、異なる複数の変換ルールは、ソースコードを特定のプログラミング言語に依存しない形式である中間形式へ変換する第１変換ルールと、前記中間形式に対して抽象化処理を行う第２変換ルールと、前記中間形式から前記検査コードに変換する第３変換ルールとに分類される。ソースコードから検査コードへの変換は、ソースコードを、実装−汎化変換ルールにより、汎化モデルへ変換するステップと、前記汎化モデルを、抽象化変換ルールにより抽象化するステップと、前記汎化モデルを、汎化−検査変換ルールにより、検査コードへ変換するステップと、の３つのステップを続けて行うことで実現される。換言すると、ソースコードから検査コードへの変換は、前記第１、第２、第３の変換ルールを各々１つ以上入力するステップと、前記第１変換ルールを用いて、ソフトウェアのソースコードを、前記中間形式へ変換するステップと、前記第２変換ルールを用いて、前記中間形式で表現されたソフトウェアを抽象化するステップと、前記第３変換ルールを用いて、前記中間形式を検証ツールの入力言語で記述された検証用コードに変換するステップの３つのステップを続けて行うことで実現される。
【００２４】
また、本発明において、検査対象のソースコードを、検査コードへ変換する一連の処理にて、内部的に保持される情報（モデル）は、その形式をメタモデルにより定義される。前記モデルは、検査対象のソースコードに対応する情報をもつ実装モデルと、前述の汎化モデルと、モデルチェッカの記述言語に対応する情報をもつ検査モデルと、に分類される。実装モデルは、そのメタモデルであるメタ・実装モデルにより定義され、汎化モデルは、そのメタモデルであるメタ・汎化モデルにより定義され、検査モデルは、そのメタモデルであるメタ・検査モデルにより定義される。前述のそれぞれのメタモデルは、データ構造の定義と、データに含まれる要素間の制約に関する情報とを保有する。
【００２５】
また、本発明において、汎化モデルには、実装モデルもしくは検査モデルの要素に対応付く等価な要素が存在する物理要素と、抽象化の変換の過程で用いる論理要素との、２種類の要素が含まれる。論理要素は、属性情報と、関連する物理要素への参照を持つことができる、物理要素の特性を継承した要素である。物理要素それぞれには、対応した論理要素が存在する。例えば、物理要素を、対応した論理要素に置き換えることで追加の属性情報を与えること、新たな論理要素へ置き換えること、及び、論理要素を異なる物理要素へ置き換えることを、変換ルールとして記述することにより、抽象化記述を段階ごとに再利用可能とすることができる。
【００２６】
以下、図面を参照して本発明の実施形態について詳しく説明する。
【００２７】
まず、図１、図２を参照しながら本発明の基本概念を説明する。本発明では、図１に示すように、ソースコード０００１に対して、ソースコード変換装置１０００において、複数の変換ルール０００２を組み合わせた変換処理を行うことにより、既存モデル検査装置に適合した検査コード０００５へ変換する。すなわち、（ａ）“変換”を細粒度に分割し、複数の「変換ルール」０００２の組み合わせとしてパッケージ化することで、柔軟な変換を実現する。（ｂ）利用者（検査者）は、検査対象のソースコード０００１を入力し、対象のソースコードと検査水準に応じた「変換ルール」０００２を選択して、所望の検査コード０００５を得る。
【００２８】
本発明における、「変換ルール」の例を挙げると次の通りである。
（ａ）単純な構文変換
「C言語の条件分岐 (If文・Switch文)」を、「検査コードの条件分岐(If 文)」に変換
「C言語の繰り返し文（for文・while文・…）」を、「検査コードの繰り返し(Do文)」に変換
（ｂ）外部環境のモデル化
「データ読込み」を、「ランダム入力」へ置き換え
（ｃ）抽象化
「繰り返しの除去」
「条件の簡略化」
図２により、本発明のソースコード変換処理における変換ルールの入力インタフェースについて、説明する。
【００２９】
本発明によれば、細粒度に分割された複数の変換ルール０００２を入力するインタフェースを所有するので、利用者による抽象化の変更は、複数の異なる変換ルール０００２を選択・入力する操作により容易に実現される。すなわち、利用者による抽象化の水準の変更は、ドメイン情報、検査したい性質、及び検査水準の情報（抽象化による性質への影響）に応じて、利用者が複数の異なる変換ルール０００２を選択して呼び出し、ソースコード変換装置１０００へ入力する操作により容易に実現される。
【００３０】
本発明によれば、異なる複数の変換ルール０００２を用いて検査対象のソースコード０００１をモデルチェッカの入力言語で記述された検査コード０００５へ変換する手順を含んでいる。前記異なる複数の変換ルールは、実装−汎化変換ルールと、抽象化変換ルールと、汎化−検査変換ルールとに分類され、これらの変換ルールを用いた変換は段階的に実行される。検査対象のソースコードの設計変更に追従する際には、変更に関連する変換ルールのみを変更すればよく、変更が最小限にとどめられる。加えて、実装モデルと、汎化モデルと、検査モデルとをそれぞれメタモデルで定義し、制約を加えることにより、変換ルールによる変換結果が不正でないことを検証可能となる。これによって、本実施形態では、検査対象のソースコードを検査コードへ抽象化しながら変換する一連の処理は、細粒度の変換ルールを組み合わせることで実現されるが、このような一連の処理の実現方法によって生じる変換ルールの検証コストの増大を防ぐことができる。
【００３１】
また、異なる検査ツールにて検査するために、前記検査ツールの形式で出力する際には、メタ・検査モデルと、汎化−検査変換ルールのみを作成すればよく、作成部分が最小限にとどめられる。
【００３２】
（第１の実施例）
次に、本発明の第１の実施例になるソースコード変換装置及び変換処理方法を、図３Ａから図３２を参照しながら説明する。
【００３３】
図３Ａは、第一の実施例となるソースコード変換装置を含むソースコード変換システムの構成例を示す図である。本発明の実施形態に適用されるソースコード変換装置１０００は、検査対象のソースコード０００１を検査コード０００５に変換する装置であり、入力部１１００と、変換処理部１２００と、出力部１３００と、記憶部１４００と、制御部１５００とを備える。２０００はモデル検査ツール、３０００は検査結果を示す。
【００３４】
入力部１１００は、ソースコード０００１及び変換ルール０００２の入力を受け付ける。記憶部１４００には、変換ルール０００２、メタモデル０００３、及び書出しルール０００４が格納される。メタモデル０００３は、変換処理部１２００によるソースコード００１を検査コード０００５へ変換する一連の処理で内部的に保持されるモデルの形式を定義するためのデータである。メタモデル０００３は、上述したように、データ構造の定義と、データに含まれる要素間の制約に関する情報とを保有する。なお、データに含まれる要素は物理要素及び論理要素を含み、物理要素に関する情報を物理要素定義００３１といい、論理要素に関する情報を論理要素定義００３２という。
【００３５】
変換処理部１２００は、検査対象のソースコード０００１を変換ルール０００２に基づいて検査コード０００５に変換する。出力部１３００は書出しルール０００４に基づいて検査コード０００５を出力する。制御部１５００は、ソースコード変換装置１０００の全体の処理を制御するための各種処理を実行するプロセッサである。
【００３６】
図３Ｂに、ソースコード変換装置１０００の構成例を示す。入力部１１００は、ソースコード入力部１１０１、及び変換ルール入力部１１０２を有する。変換処理部１２００は、モデル構築部１２０１、実装−汎化モデル変換部１２０２、抽象化モデル変換部１２０３、及び、汎化−検査モデル変換部１２０４を有する。出力部１３００は、検査コード書出し部１３０１を有する。記憶部１４００は、変換ルールデータベース１４０１、メタモデルデータベース１４０２、及び、書出しルールデータベース１４０３を有する。
【００３７】
ソースコード変換装置１０００は、例えば、１台のコンピュータ、又は、ネットワークを介して接続された複数のコンピュータ上で動作するプログラムとして実施される。ソースコード０００１と変換ルール集合０００２とは、例えば、コンピュータ上の記憶装置から読込む方法と、コンピュータに接続された入力デバイスにより直接入力される方法等の方法により入力される。また、検査コード０００５は、例えば、コンピュータ上の記憶装置に書出す方法と、コンピュータのディスプレイ装置に表示する方法により出力される。
【００３８】
入力部１１００は、ユーザによって入力されるデータを受付け、入力されたデータを変換処理部１２００へ供給する処理を行う。入力部１１００は、ソースコード０００１に関する情報と、細粒度に分割された複数の変換ルール、すなわち「変換ルール集合」０００２に関する情報とを受付け、変換処理部１２００へ供給する。ある実施形態においては、入力部１１００は、ユーザによる、変換処理部の駆動や制御、出力部の駆動や制御、に関する指示を受け付けてもよい。
【００３９】
変換処理部１２００には、入力部１１００から、ソースコード０００１の情報と、ソースコード０００１に適用すべき変換ルール集合０００２の情報とが供給される。また、変換処理部１２００は、ソースコード０００１を、変換ルール集合０００２により変換する処理を行い、変換結果の情報を、出力部１３００に供給する。ある実施形態においては、入力部１１００から供給される変換ルール集合０００２に関する情報は、記憶部１４００に格納された変換ルール０００２を指し示す識別情報のみが含まれていて、変換ルール集合０００２の実体を、前記識別情報を用いて記憶部１４００から取り出し、変換に用いてもよい。
【００４０】
図６を用いて、変換処理部１２００及び出力部１３００の詳細ついて説明する。
【００４１】
変換処理部１２００は、モデル構築部１２０１と、実装−汎化モデル変換部１２０２と、抽象化モデル変換部１２０３と、汎化−検査モデル変換部１２０４とを有する。
【００４２】
本実施形態において、変換処理部１２００は、メタモデル０００３（図３Ａ参照）と、変換ルール０００２を用いたモデル変換により、ソースコード情報１００１を、検査モデル１００８へ変換する。メタ・実装モデル１００２と、メタ・汎化モデル１００３と、メタ・検査モデル１００４とは、例えば、非特許文献２に記載のMOFにて記述する。また、例えば、非特許文献３に記載されているQVTにて、実装−汎化変換ルール１００５と、抽象化変換ルール１００６と、汎化−検査変換ルール１００７とを記述し、モデルの変換を行う。前記変換は、既に例示した方法の他のモデル変換方法でもよく、また、複数の方法を混在させてもよい。
【００４３】
また、ある実施形態においては、実装−汎化モデル変換部１２０２と、抽象化モデル変換部１２０３と、汎化−検査モデル変換部１２０４とをそれぞれ独立させず、同一の部位により行われても良く、さらに、実装モデル１２０５と、汎化モデル１２０６と、検査モデル１００８と、のそれぞれのメタモデルとして、メタ・実装モデル１００２と、メタ・汎化モデル１００３と、メタ・検査モデル１００４とを個別に用意せず、単一のメタモデルにより、実装モデル１２０５と、汎化モデル１２０６と、検査モデル１００８とを定義してもよい。また、ある実施例においては、メタ・実装モデル１００２と、メタ・汎化モデル１００３と、メタ・検査モデル１００４と、は、複数の方式により、それぞれ実装モデル１２０５、汎化モデル１２０６、検査モデル１００８、の形式や制約を定義してもよい。例えば、それぞれのメタモデルは、前記MOFによる定義のほかに、非特許文献４に記載されているOCLにて記載された制約条件を含み、モデルの変換を行った際に、制約条件を満たしているかどうかの検証を行う方法があり得る。
【００４４】
モデル構築部１２０１は、ソースコード入力部１１０１からソースコード情報１００１を受け取り、実装モデル１２０５へ変換する。実装モデル１２０５の形式は、そのメタモデルであるメタ・実装モデル１００２により、定義される。実装モデル１２０５は、本発明の効果を最大限に得るためには、ソースコード情報１００１と相互に変換するのに必要十分な情報を持つことが望ましいが、ある実施形態によっては、検査コードを出力するという目的を逸しない程度にて、情報の省略や、追加があってもかまわない。
【００４５】
ある実施形態においては、モデル構築部１２０１は、ソースコード入力部１１０１と不可分な様態で実装され、ソースコード情報１００１が生じない形態で処理が進んでもよい。
【００４６】
実装−汎化モデル変換部１２０２は、実装−汎化変換ルール１００５と、メタ・実装モデル１００２と、メタ・汎化モデル１００３とを用いて、実装モデル１２０５を汎化モデル１２０６へ変換する。汎化モデル１２０６は、複数のプログラミング言語における構造及び処理を表現可能なデータ構造をもつ。例えば、汎化モデル１２０６中では、ソースコード０００１におけるIf文とSwitch文とを区別せず、選択的実行文として表現する。ある実施形態においては、実装モデル１２０５を、汎化モデル１２０６へ変換する際、実装−汎化変換ルール１００５のみを用いることもあり得る。また、ある実施形態において、実装−汎化変換ルール１００５が、複数の変換ルールを含む場合には、複数の変換ルールを統合して一つの変換ルールとし、実装モデル１２０５から汎化モデル１２０６への変換に利用する方法があり得る。また、ある実施形態において、実装−汎化変換ルール１００５が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、実装モデル１２０５から汎化モデル１２０６への変換を行う手順があり得る。
【００４７】
抽象化モデル変換部１２０３は、抽象化変換ルール１００６と、メタ・汎化モデル１００３とを用いて、汎化モデル１２０６の抽象化を行う。抽象化の例としては、選択文における条件式を、恒真、もしくは恒偽、又は非決定的な選択で置き換える方法があり得る。ある実施形態においては、汎化モデル１２０６を抽象化する際、抽象化変換ルール１００６のみを用いることもあり得る。また、ある実施形態において、抽象化変換ルール１００６が、複数の変換ルールを含む場合には、複数の変換ルールを統合して一つの変換ルールとし、汎化モデル１２０６の抽象化に用いる方法があり得る。また、ある実施形態において、抽象化変換ルール１００６が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、汎化モデル１２０６の変換を行う手順があり得る。
【００４８】
汎化−検査モデル変換部１２０４は、汎化−検査変換ルール１００７と、メタ・汎化モデル１００３と、メタ・検査モデル１００４とを用いて、汎化モデル１２０６を、検査モデル１００８へ変換する。例えば、検査コード０００５がPromela形式である場合、汎化モデルにおいて選択的実行文として表現された要素は、検査モデルにおいてはIf文として表現される。ある実施形態においては、汎化モデル１２０６を、検査モデル１００８へ変換する際、汎化−検査変換ルール１００７のみを用いることもあり得る。また、ある実施形態において、汎化−検査変換ルール１００７が、複数の変換ルールを含む場合には、複数の変換ルールを統合して１つの変換ルールとし、汎化モデル１２０６から検査モデル１００８への変換に利用する方法があり得る。また、ある実施形態において、汎化−検査変換ルール１００７が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、汎化モデル１２０６から検査モデル１００８への変換を行う手順があり得る。
【００４９】
出力部１３００は、変換処理部１２００より供給された、変換結果の情報を用いて、検査コード０００５を出力する。ある実施形態においては、検査コード０００５の出力に際して、例えばモデルチェッカの記述言語の文法情報などの情報を記憶部１４００から供給されてもよい。
【００５０】
検査コード書出し部１３０１は、メタ・検査モデル１００４と、記憶部１４００の書出しルールデータベース１４０３から取得した検査コード書出しルール１００９とを用いて、検査モデル１００８を検査コード０００５へ変換する。例えば、非特許文献５に記載される方法にて、検査コード書出しルール１００９を記述し、検査モデル１００８から、検査コード０００５への変換を行う。ある実施例においては、これに限らず、検査モデル１００８を、検査に利用するモデルチェッカの記述形式へ変換する任意の方法でもよい。検査コード０００５は、例えば、モデルチェッカとしてSPINを用いる場合には、SPINの入力言語である、Ｐｒｏｍｅｌａ言語により記述される。
【００５１】
記憶部１４００において、変換ルールデータベース１４０１、メタモデルデータベース１４０２、及び書出しルールデータベース１４０３のそれぞれは、例えば、関係データベース、又は、階層型データベースなどの、コンピュータ上にて実現される任意のデータ格納方式で実現される。変換ルールデータベース１４０１と、メタモデルデータベース１４０２と、書出しルールデータベース１４０３と、は互いに同一の方式で実現されている必要性は無く、互いに異なる方式で実現されていてもよい。また、変換ルールデータベース１４０１と、メタモデルデータベース１４０２と、書出しルールデータベース１４０３と、のそれぞれは、単一の方式で実現されている必要性は無く、例えば、保有すべき情報の一部を関係データベースに格納し、保有すべき情報の一部を、発明を実現するコンピュータプログラム中に組込むなど、それぞれ異なる方式の組合せで実現されていてもよい。
【００５２】
記憶部１４００は、入力部１１００と、変換処理部１２００と、出力部１３００とが、それぞれの処理を行うのに必要な情報を供給する。例えば、記憶部１４００は、変換ルールに関する情報と、メタモデルに関する情報と、モデルチェッカの記述言語の文法に関する情報とを格納する。
【００５３】
変換ルールデータベース１４０１は、既に述べたとおり、変換ルールを、メタデータとともに保有する。前記メタデータは、変換ルールを選択するためのものであり、実装−汎化変換ルール１００５と、抽象化変換ルール１００６と、汎化−検査変換ルール１００７の、それぞれ異なる情報を持つ方法があり得る。実装−汎化変換ルール１００５のメタデータは、例えば、変換元ソースコードの記述言語の種類があり得る。抽象化変換ルール１００６のメタデータは、例えば、抽象化を分かりやすく端的に表現した名前、簡単な説明、「データの抽象化」、「処理の抽象化」などの抽象化の種別、自然語（例えばアルファベット又は数値）で表現された抽象化による状態数削減効果、自然語（（例えばアルファベット又は数値）で表現された抽象化による性質への影響、及び抽象化の適用できるソフトウェアのドメイン、があり得る。汎化−検査変換ルール１００７のメタデータは、例えば、検査に使用するモデルチェッカを指し示す名前があり得る。
【００５４】
以降、図４ないし図６を参照しながら入力部１１００、変換処理部１２００、出力部１３００、記憶部１４００、及び制御部１５００の詳細を説明する。
【００５５】
まず、本実施例におけるソースコード変換手順の一例を、図４及び図６を参照しながら説明する。本実施例におけるソースコード変換手順は、ソースコード入力ステップＳ１０１と、変換ルール入力ステップＳ１０２と、変換ルール適用ステップＳ１０３と、検査コード出力ステップＳ１０４と、を含む。このソースコード変換手順は、制御部１５００が主体となって実行される。
【００５６】
まず、ソースコード入力ステップＳ１０１において、ソースコード入力部１１０１により、ソースコード０００１がソースコード変換装置１０００に読み込まれ、ソースコード情報１００１へ変換される。
【００５７】
ソースコード入力部１１０１は、利用者から入力された検査対象のソースコード０００１を受け付け、ソースコード情報１００１へ変換する。ソースコード０００１は、例えば、JIS X3010-1993に公開されるプログラミング言語Ｃにより記述される。ソースコード情報１００１は、具体的には、例えば抽象構文木の形式で保持される。ソースコード情報１００１の形式は、抽象構文木に限らず、構造や論理などソースコード０００１の検査に要する情報を保持する、任意の形式でもよい。
【００５８】
ソースコード入力ステップＳ１０１に続き、変換ルール入力ステップＳ１０２において、変換ルール入力部１１０２により、細粒度に分割された複数の変換ルールである変換ルール集合０００２がソースコード変換装置１０００に読み込まれる。この変換ルール入力ステップＳ１０２では、変換前のモデルの要素と変換後のモデル要素との対応関係、及び変換によって変換前のモデルの要素に加えられる操作の少なくとも一方が定義される。変換ルール集合０００２をソースコード変換装置１０００に読み込む処理は、利用者による一度の操作で行われる必要性は無く、繰り返し操作により行われてもよい。また、ソースコード入力ステップＳ１０１、及び変換ルール入力ステップＳ１０２は、必ずしもこの順番で完了する必要性は無く、ソースコード入力部１１０１によりソースコード情報１００１が生成される前にソースコード０００１が入力され、かつ、変換ルール入力部１１０２が変換ルール入力処理のためにソースコード情報１００１を要求する前にソースコード０００１が入力されていればよい。したがって、ソースコード入力ステップＳ１０１の処理と、変換ルール入力ステップＳ１０２の処理とが混在する順番で処理がすすんでもよい。例えば、ソースコード入力部１１０１がソースコード０００１を受け付け、続いて、変換ルール入力部１１０２が、変換ルール集合０００２を受け付け、続いて、ソースコード入力部１１０１が、ソースコード０００１をソースコード情報１００１へ変換する、手順があり得る。
【００５９】
変換ルール入力部１１０２は、利用者から入力された変換ルール集合０００２を受け付ける。利用者から変換ルール集合０００２を受け付ける方法は、例えば、次に示す方法があり得る。
【００６０】
一つめの変換ルール入力方法の例として、変換ルール入力部１１０２は、変換ルール集合０００２の一部として、利用者が手作業で直接入力した変換ルールを受け取る。
【００６１】
二つめの変換ルール入力方法の例として、図５Ａに示すように、変換ルール集合０００２の少なくとも一部は、利用者が記述した変換ルール（記述）００１０により入力してもよい。また、入力部１１００が、記憶部１４００から変換ルールの一覧００１５を取得し、取得した変換ルールの一覧００１５を利用者に一覧などの形式で提示し、前記提示された一覧から変換ルールを利用者が選択することによって、変換ルール集合０００２の入力を受け付けてもよい。すなわち、利用者が、変換ルールの入力に前置して、変換ルールの検索条件００１１を入力部１１００の変換ルール入力部１１０２に入力（記述）し、続いて、変換ルール入力部１１０２が、前記検索条件に合致する変換ルールを、記憶部１４００が有する変換ルールデータベース１４０１から取得し変換ルール一覧００１５として前記利用者に提示する。続いて、前記利用者が、提示された前記変換ルール一覧００１５に含まれる一つ以上の変換ルールを選択する。この利用者によって選択された一つ以上の変換ルールを、変換ルール入力部１１０２が、変換ルール集合０００２の一部として受け付ける。
【００６２】
三つめの変換ルール入力方法の例として、まず、利用者が、変換ルールの入力に前置して、変換ルールの検索条件００１１を変換ルール入力部１１０２に入力し、続いて、変換ルール入力部１１０２が、前記検索条件に合致する変換ルールを、変換ルールデータベース１４０１から取得して、変換ルール集合０００２の一部として受け付けてもよい。
【００６３】
四つめの変換ルール入力方法の例として、図５Ｂに示すように、入力されたソースコード０００１から、変換ルール入力部１１０２が、変換ルールの検索条件００１２を抽出、生成し、さらに、前記検索条件に合致する変換ルールを、変換ルールデータベース１４０１から取得し、変換ルール集合０００２の一部として受け付ける。
【００６４】
二つめの変換ルール入力方法の例と、三つめの変換ルール入力方法の例と、四つめの変換ルール入力方法の例における、変換ルール検索条件の因子としては、例えば、後述する、変換ルールデータベース１４０１において、変換ルールのメタデータとして格納される情報があり得る。
【００６５】
また、五つめの変換ルール入力方法の例として、変換ルール入力部１１０２は、何らかの方法で入力された変換ルールを加工することにより、変換ルールを受け付ける。前記加工方法の例としては、変換ルールデータベース１４０１には、ソースコード０００１中の変数名などをパラメタ化した状態で変換ルールを保持しておき、例えば利用者の明示的な入力による方法などにより、ソースコード０００１の情報にてパラメタを埋めたものを、変換ルール集合０００２に含める方法があり得る。五つめの変換ルール入力方法の例において、加工元の変換ルールの入力方法としては、既に述べた一つめの変換ルール入力方法の例など、入力された変換ルールを加工せずに用いる場合と同様の方法があり得る。
【００６６】
変換ルール入力部１１０２が、変換ルール集合０００２を受け付ける方法は、これらの変換ルール入力方法に限らず、変換処理部１２００で用いる変換ルールの集合を受け付ける任意の方法でよく、また、これらの変換ルール入力方法の一つ以上の組合せにより変換ルール集合０００２を受け付けてもよい。
【００６７】
変換ルール入力ステップＳ１０２に続き、変換ルール適用ステップＳ１０３において、モデル構築部１２０１がソースコード情報１００１を実装モデル１２０５へ変換し、続いて、実装−汎化モデル変換部１２０２が実装モデル１２０５を汎化モデル１２０６へ変換し（Ｓ１０３１）、続いて、抽象化モデル変換部１２０３が汎化モデル１２０６を抽象化し（Ｓ１０３２）、続いて、汎化−検査モデル変換部１２０４が汎化モデル１２０６を検査モデル１００８へ変換する（Ｓ１０３３）。変換ルール入力ステップＳ１０２と、変換ルール適用ステップＳ１０３とは、必ずしもこの順番で処理が完了する必要性は無く、実装−汎化モデル変換部１２０２の処理までに実装−汎化変換ルール１００５が入力され、かつ、抽象化モデル変換部１２０３の処理までに抽象化変換ルール１００６が入力され、かつ、汎化−検査モデル変換部の処理までに汎化−検査変換ルール１００７が入力されていればよい。
【００６８】
変換ルール適用ステップＳ１０３に続き、検査コード出力ステップＳ１０４において、検査コード書出し部１３０１により、検査モデル１００８が、検査コード０００５として書き出される。検査コード０００５の書出し先の指定は、必ずしも変換ルール適用ステップＳ１０３の後である必要性は無く、検査コード０００５の書出しよりも先であればよい。例えば検査コード０００５の書出し先の指定がソースコード入力ステップＳ１０１と平行して行われる手順があり得る。
【００６９】
次に、図７、図８Ａ、図８Ｂを用いて、変換の手順をより詳細に説明する。図７に示すように、本発明では、モデル変換技術を利用し、段階的に変換するために、次のような処理を行う。
【００７０】
（１）ソースコード０００１をこれと（ほぼ）等価な「実装モデル」１２０５へ変換
（２）「実装モデル」を特定のプログラミング言語に依存しない形式にて構造及び論理などのプログラム情報を表現する「汎化モデル」１２０６へ変換
すなわち、異なる複数の第１変換ルール１００５−１〜１００５−ｎの少なくとも一つを用いて、「実装モデル」１２０５を特定のプログラミング言語に依存しない形式である中間形式の「汎化モデル」１２０６へ変換する。図７の例では、第１変換ルールとして、「“ｉｆ文”→条件分岐」、「“ｓｗｉｔｃｈ文”→条件分岐」、「“ｗｈｉｌｅ文”→“繰り返し”」、及び「“ｆｏｒ文”→“繰り返し”」の少なくとも四つの異なる変換ルールが選択されている。
【００７１】
（３）汎化モデル１２０６に対して、抽象化のための変換を実施
すなわち、異なる複数の第２変換ルール１００６−１〜１００６−ｎの少なくとも一つを用いて、前記中間形式の汎化モデル１２０６に対して抽象化処理を行う。図７の例では、第２変換ルールとして、「データ読み込み→ランダム入力」、及び「データの抽象化」の少なくとも二つの異なる変換ルールが選択されている。
【００７２】
（４）汎化モデル１２０６を、「検査モデル」１００８に変換し、コード生成（出力）
すなわち、異なる複数の第３変換ルール１００７−１〜１００７−ｎの少なくとも一つを用いて、前記中間形式の汎化モデル１２０６から検査コードの生成に要する情報を有する検査モデル１００８に変換する。図７の例では、第３変換ルールとして、第１変換ルールに対応した「“条件分岐”→“ｉｆ”文」、及び「“繰り返し”→“ｄｏ”文」の少なくとも二つの異なる変換ルールが選択されている。
【００７３】
また、実装モデル１２０５、汎化モデル１２０６、検査モデル１００８は、それぞれ構文を定義する「メタモデル」によりデータ構造及び意味論が定義される。
【００７４】
このように、実装モデル１２０５から汎化モデル１２０６への変換に際しては、例えば、変換対象ソースコードの記述言語の文法が、繰り返し処理の記法として“ｆｏｒ文” 及び“ｗｈｉｌｅ文”を含む場合、使用者が“ｆｏｒ文”を「繰り返し」へ変換するルールと、“Ｗｈｉｌｅ文”を「繰り返し」へ変換するルールとを、既に述べた変換ルール入力方法を用いて、第１変換ルールとして選択する。汎化モデル１２０６の抽象化の変換に際しては、使用者が検査水準（抽象化の度合い）を決定し、決定した検査水準を達成する変換ルールとして、例えば、外部データの読込みに関する命令及び一連の処理をランダムな入力へ変換するルールと、特定のデータ型をより抽象度の高い型へ変換するルールとを、既に述べた変換ルール入力方法を用いて、第２変換ルール１００６として選択する。さらに、汎化モデル１２０６から検査モデル１００８への変換に当たっては、例えば、モデルチェッカの入力言語の文法が、繰り返し処理の記法として“ｄｏ文”をもつとき、使用者が「繰り返し」を“ｄｏ文”へ変換するルールを、既に述べた変換ルール入力方法を用いて、第３変換ルール１００７として選択する。変換ルールは、複数のソフトウェアにまたがって適用可能な汎用的なルールなど、繰り返し利用可能なものがデータベース化される。データベースに格納された変換ルールは、使用者による検索及びルール選択の判断材料として用いられるメタ情報として、ドメイン情報や検査水準（抽象化による検査への影響）の情報を有する。
【００７５】
また、変換ルールの選択方法としては、次のようなものがある。
【００７６】
（１）汎用的なルール：常に選択
（２）特定のライブラリに依存したルール：使用ライブラリ、及び検査対象のドメイン(カテゴリ)を入力することで、まとめて選択
（３）抽象化に対応したルール：（検査したい性質・検査水準を入力して得た）変換ルール一覧から、利用者が選択、もしくは利用者自身が記述して入力、もしくは検査したい性質などから、自動生成。
【００７７】
図８Ａ、図８Ｂに、それぞれモデルの抽象化の一例を示す。モデルの抽象化により、状態数を削減することができる。しかし、抽象化によりモデルの性質に影響を与えることがある。例えば、検出された欠陥（反例）が、もとのシステムに存在しない、もとのシステムに存在する欠陥を発見できない、等である。一方で、性質に影響を与えない健全な抽象化は、状態数削減効果が小さい傾向がある。
【００７８】
図９に、メタ・実装モデル１００２の一例の一部を示し、図１０にメタ・汎化モデル１００３の一例の一部を示し、図１１にメタ・検査モデル１００４の一例の一部を示す。本実施例におけるメタ・実装モデル１００２と、メタ・汎化モデル１００３と、メタ・検査モデル１００４とは、非特許文献２に開示される記法を用いて示されている。例えば、図９において、IfStatementクラスＣ１０１は、関係Ｒ１０１によりStatementクラスＣ１０２を継承することが示され、関係Ｒ１０２により、属性conditionとしてExpressionクラスＣ１０３を所有することが示され、関係Ｒ１０３により、属性bodyとしてStatementクラスＣ１０２の集合を所有することが示され、関係Ｒ１０４により属性elseBodyとしてStatementクラスＣ１０２の集合を所有することが示されている。また、例えば、図９において、IntegerConstantクラスＣ１０４は、整数値である属性valueを所有することが示され、関係Ｒ１０５により、ExpressionクラスＣ１０３を継承すること等が示されている。また、例えば、図９において、VariableReferenceクラスＣ１０５は、関係Ｒ１０６により、ExpressionクラスＣ１０３を継承することが示され、関係Ｒ１０７により、VariableDeclarationクラスＣ１０６を参照することが示されている。
【００７９】
メタ・実装モデル１００２の各要素、及び、メタ・検査モデル１００４の各要素には、それぞれ、実装プログラミング言語の言語要素、及び、検査用言語の言語要素に対応付く要素が含まれる。本実施例においては、実装プログラミング言語はＣ言語であり、検査用言語はＰｒｏｍｅｌａ言語であるため、それぞれ、メタ・実装モデル１００２はＣ言語の言語要素と対応付く要素を含み、、メタ・検査モデル１００４はＰｒｏｍｅｌａ言語の言語要素と対応付く要素を含む。例えば、図９におけるIfStatementクラスＣ１０１は、Ｃ言語におけるＩｆ文を表現し、IntegerConstantクラスＣ１０４は、Ｃ言語における整数型定数値を表現している。
【００８０】
図１０に示すメタ・汎化モデル１００３には、メタ・実装モデル１００２に含まれる要素と意味的に対応付く要素であるか、メタ・検査モデル１００４に含まれる要素と意味的に対応付く要素である、物理要素が含まれる。本実施例におけるメタ・汎化モデル１００３においては、物理要素は、図１０において、PhysicalElementクラスＣ２０１を推移的に継承する要素として表現されている。例えば、StatementクラスＣ２０３及びSelectionStatementクラスＣ２０４が、物理要素の一例である。それぞれの物理要素は、メタ・実装モデル１００２に含まれる要素、又はメタ・検査モデル１００４に含まれる要素と、一対一で対応付く必要は無く、複数の要素の組合せで、等価な意味を持つ言語要素を表現できればよい。例えば、本実施例においては、メタ・実装モデル１００２でIfStatementクラスＣ１０１として表現されるＣ言語のIf文は、メタ・汎化モデル１００３でSelectionStatementクラスＣ２０４とSelectionItemクラスＣ２０５との組合せで表現される。
【００８１】
メタ・汎化モデル１００３は、上述した物理要素の他に、ソースコードの性質、変換の目的、及び制約条件などに応じて、変換ルールによって対応付けられる要素を変更可能とする論理要素を含む。論理要素は、本実施例においては、図１０における、LogicalElementクラスＣ２０２を推移的に継承する要素として表現される。
【００８２】
LogicalElementクラスＣ２０２は、AttiributeクラスＣ２０６の集合を所有する。AttributeクラスＣ２０６は、クラス及びメソッドなどに対して属性情報を付加する機能を備える。これによって、ある変換ルールは、ある物理要素を論理要素に変換することによって、変換後の論理要素に追加の属性情報を付加できる。また、付加された属性情報は異なる変換ルールによっても利用可能となる。
【００８３】
また、LogicalElementクラスＣ２０２は、任意の物理要素を参照できるRelatedElementクラスＣ２０７の集合を所有する。これによって、変換ルールは、任意の要素に対する関連を、その関連の名前とともに論理要素に付加することができ、また、他の変換ルールは、その関連を利用することが可能となる。
【００８４】
また、論理要素は、例えば、StatementクラスＣ２０３に対するLogical_StatementクラスＣ２０８のように、各物理要素に対して定義される。このため、変換ルールが、任意の物理要素を、当該物理要素に対して情報又は関連を付加した論理要素へ変換することが可能となる。また、すべての論理要素は、何らかの物理要素を継承していることから、ある変換ルールにおいて、ある物理要素が論理要素へ変換された後、異なる変換ルールにおいて、それが論理要素であることを意識せず、物理要素として扱うことも可能である。
【００８５】
論理要素を利用する変換ルールには、例えば、下記（１）〜（３）のような方法があり得る。
【００８６】
（１）あるパターンに一致する汎化モデルの物理要素を、ある構造を有する論理要素（又は、論理要素と物理要素との組み合わせ）へ変換する。
【００８７】
（２）あるパターンに一致する論理要素（又は、論理要素と物理要素との組み合わせ）を、異なる構造を有する論理要素（又は、論理要素と物理要素との組み合わせ）へ変換する。
【００８８】
（３）あるパターンに一致する論理要素（又は、論理要素と物理要素との組み合わせ）を、物理要素へ変換する。
【００８９】
汎化モデル１２０６上で、論理要素を物理要素へ完全に変換してから、汎化モデル１２０６を検査モデル１００８へ変換してもよい。汎化モデル１２０６の論理要素を検査モデル１００８の要素へ変換可能な変換ルールを用い、論理要素を含む汎化モデル１２０６を直接検査モデル１００８へ変換してもよい。また、本実施例の後述する第１の変換例〜第５の変換例における論理要素は、乱数生成方法及び非決定的な値を選択する方法を表現したが、これに限らず、プログラミング言語の文法が直接表現可能な範囲を超える任意の要素を表現してもよい。論理要素によって表現される概念の例としては、例えば、ハードウェア操作など外部環境とのやり取りの抽象化、並びに、データ構造及びモジュールの抽象化などが挙げられる。
【００９０】
また、各メタモデルは、図９〜図１１に示す限りではなく、変換対象となるプログラムを表現可能な任意の形式でよい。また、汎化モデル１２０６における論理要素に関しても、この限りではなく、変換ルールの記述に必要な、論理要素の種類を示す要素、論理要素、及び、他の要素（物理要素又は論理要素）との関連を示す要素、を表現可能な任意の記法でよい。また、論理要素は、特定の頻出する要素に関して、予め構造を定義してもよい。このような論理要素の定義の一例としては、最大値と最小値とを属性として有し、乱数生成を示す論理要素を、LogicalElementクラスＣ２０２を推移的に継承する新たなクラスの定義などがあり得る。乱数生成を示す論理要素は図１６で詳細を説明する。
【００９１】
以降、図９に示すメタ・実装モデル１００２、図１０に示すメタ・汎化モデル１００３、及び図１１に示すメタ・検査モデル１００４を用いた、ソースコード０００１から検査コード０００５への第１の変換例〜第５の変換例を図１２〜図３２に示す。
【００９２】
ソースコード０００１から検査コード０００５への第１の変換例について図１２〜図１７を用いて説明する。
【００９３】
図１２は、Ｃ言語のソースコード０００１の一例の説明図である。
【００９４】
図１２に示すソースコード０００１の行００１では、ランダムな整数値を生成する関数rand()の戻り値を５０で割った余りに１が加算されることによって、１から５０までのランダムな値が生成される。行００２では、行００１で生成したランダムな値を引数として関数do_something()が実行される。
【００９５】
図１３は、Ｐｒｏｍｅｌａ言語による検査コード０００５の一例の説明図である。
【００９６】
図１３に示す検査コード０００５の行００１では、整数型の変数valが定義される。行００２では、１から５０までの整数から変数valの値が選択される。行００３では、行００２で選択された変数valの値を引数として関数do_something()が実行される。
【００９７】
図１４は、図１２に示すソースコード０００１の実装モデル１２０５の一例である。
【００９８】
図１４に示す実装モデル１２０５は、図９に示すメタ・実装モデル１００２による定義を用いて表現される。例えば、図１２に示すソースコード０００１の行００１では、変数valがint型で宣言されているため、当該宣言は、図１４に示す実装モデル１２０５では、属性nameとして”val”を有し、属性typeとして”int”を有するVariableDeclaration要素Ｏ０１０１として表現される。
【００９９】
また、図１２に示すソースコード０００１の行００２における変数valの参照は、VariableDeclaration要素Ｏ０１０１とVariableReference要素Ｏ０１０２とが、declarationをラベルとして有するリンクＬ０１０１を介して接続されることによって、表現される。
【０１００】
図１４に示す実装モデル１２０５が、“ｆｏｒ文”及び“ｗｈｉｌｅ文”を「繰り返し」へ変換する図６に示す実装−汎化変換ルール１００５（図７に示す第１変換ルール１００５−１）によって汎化モデル１２０６へ変換された結果を図１５に示す。図１５は、図１２に示すソースコード０００１の抽象化された汎化モデル１２０６の説明図である。図１２に示すソースコード０００１は“ｆｏｒ文”及び“ｗｈｉｌｅ文”を含まないので、当該変換は実行されず、図１５に示す汎化モデル１２０６は、図１４に示す実装モデル１２０５と実質的に同一である。
【０１０１】
次に、図１５に示す汎化モデル１２０６が、乱数生成処理を抽象化して論理要素に変換する図６に示す抽象化変換ルール１００６（図７に示す第２変換ルール１００６−１）によって変換された汎化モデル１２０６を図１６に示す。図１６は、図１５に示す汎化モデル１２０６の抽象化結果である。
【０１０２】
抽象化変換ルール１００６による変換処理では、図１５に示すBinaryOperation要素Ｏ０４０１、及び当該BinaryOperation要素Ｏ０４０１が推移的に所有する要素集合は、最小値１を示すAttribute要素Ｏ０７０２と最大値５０を示すAttribute要素Ｏ０７０３とを所有する乱数生成式を意味する論理要素（Logical_Expression要素Ｏ０７０１）に変換される。
【０１０３】
図１６に示す抽象化された汎化モデル１２０６が、図６に示す汎化−検査変換ルール１００７（図７に示す第３変換ルール１００７−１）によって検査モデル１００８に変換された結果を図１７に示す。図１７は、図１６に示す抽象化された汎化モデル１２０６から変換された検査モデル１００８の説明図である。
【０１０４】
図１６に示す論理要素であるLogical_Expression要素Ｏ０７０１と、最小値を表すAttribute要素Ｏ０７０２と、最大値を表すAttribute要素Ｏ０７０３と、の組合せは、Ｐｒｏｍｅｌａ言語において非決定的な値の代入を行うselect文を表現するSelectStatement要素Ｏ０８０１と、最小値を意味するIntegerConstant要素Ｏ０８０２と、最大値を意味するIntegerConstant要素０Ｏ８０３と、の組合せに変換される。IntegerConstant要素Ｏ０８０２は、minをラベルとして有するリンクＬ０８０１を介してSelectStatement要素Ｏ０８０１に接続される。IntegerConstant要素Ｏ０８０３は、maxをラベルとして有するリンクＬ０８０２を介してSelectStatement要素Ｏ０８０１に接続される。
【０１０５】
最後に、図１７に示す検査モデル１００８からコードが生成されることによって、図１３に示すＰｒｏｍｅｌａ言語による検査コード０００５が生成される。
【０１０６】
次に、図１８に示すＣ言語のソースコード０００１から図１３に示すＰｒｏｍｅｌａ言語による検査コード０００５へ変換する第２の変換例、及び、図１９に示すＣ言語のソースコード０００１から図１３に示すＰｒｏｍｅｌａ言語による検査コード０００５へ変換する第３の変換例について図１８〜図２３を用いて説明する。図１８及び図１９はＣ言語のソースコード０００１の一例の説明図である。
【０１０７】
図１８及び図１９に示すソースコード０００１は、図１２に示すソースコード０００１と、ある関数do_something()を、１から５０の任意の値を引数として実行するプログラムである点で同じである。しかし、図１２、図１８及び図１９に示すソースコード０００１では、それぞれ、乱数を生成する方法が異なる。
【０１０８】
図１８に示すソースコード０００１では、現在時刻を返すシステム関数time()を、擬似的な乱数発生関数とし、当該乱数発生関数の戻り値を５０で割った余りに１を加えることによって、１から５０のランダムな値が生成される。
【０１０９】
図１９に示すソースコード０００１では、行１０１から行１０７にて独自に定義した乱数生成関数my_rand()の戻り値を５０で割った余りに１を加えることによって、１から５０のランダムな値が生成される。ここで、行１０１から行１０７で定義される乱数発生関数my_rand()は、自身が生成する乱数の範囲の最大値（５０）と最小値（１）を、引数として受け取り、乱数発生関数my_rand()は、最大値から最小値を減算して１を加えた値を除算値とし、ランダムな整数値を生成する関数rand()の戻り値を除算値で割った余りに最小値を加えることによって、１から５０のランダムな値を生成する。なお、乱数発生関数my_rand()が生成する乱数の範囲は行０００１で定義される。
【０１１０】
図１８及び図１９に示すソースコード０００１が示すプログラムは、それぞれ、図２０及び図２１に示す実装モデル１２０５で表現される。
【０１１１】
第１の変換例と同じ実装−汎化変換ルール１００５によって、図２０及び図２１に示す実装モデル１２０５は、図２２及び図２３に示す汎化モデル１２０６に変換される。
【０１１２】
図２２に示す汎化モデル１２０６は、抽象化変換ルール１００６によって抽象化され、図１６に示す汎化モデル１２０６に変換される。この抽象化に用いる抽象化変換ルール１００６は、第１の変換例で用いた抽象化変換ルール１００６を、関数time()を関数rand()と同じく乱数発生関数として扱うように変換したものである。つまり、この抽象化変換ルール１００６によって、図２２に示す汎化モデル１２０６のBinaryOperation要素Ｏ０５０１、及び当該BinaryOperation要素Ｏ０５０１が推移的に所有する要素集合は、図１６に示す論理要素（Logical_Expression要素Ｏ０７０１）に変換される。
【０１１３】
同様に、図２３に示す汎化モデル１２０６は、抽象化変換ルール１００６によって抽象化され、図１６に示す汎化モデル１２０６に変換される。この抽象化に用いる抽象化変換ルール１００６は、第１の変換例で用いた抽象化変換ルール１００６を、関数my_rand()を、第１引数を最小値、第２引数を最大値として、乱数を発生する関数として扱うように変更したものである。つまり、この抽象化変換ルール１００６によって、図２３に示す汎化モデル１２０６のFunctionCall要素Ｏ０６０１、及び当該FunctionCall要素Ｏ０６０１が推移的に所有する要素集合は、図１６に示す論理要素（Logical_Expression要素Ｏ０７０１）に変換される。
【０１１４】
図１６に示す汎化モデル１２０６は、第１の変換例で用いた汎化−検査変換ルール１００７と同じ変換ルールによって、図１７に示す検査モデル１２０７に変換され、最終的には図１３にＰｒｏｍｅｌａ言語による検査コード０００５が出力される。
【０１１５】
第１の変換例〜第３の変換例では、抽象化変換ルール１００６を変更することによって、図１２、図１８及び図１９に示す異なるソースコード０００１から同一の図１３に示す検査コード０００５へ変換するものである。
【０１１６】
本実施例では、抽象化変換ルール１００６を用いて汎化モデル１２０６を抽象化する処理で、所定の条件に適合する要素を論理要素に変換する。これによって、第２の変換例及び第３の変換例で説明したように、入力されたソースコード０００１が変更されたとしても、管理者は、すべての変換ルール１００５〜１００７を変更せずとも、抽象化変換ルール１００６を変更するのみで、当該ソースコード０００１が変更されて変更前と同じ検査コード０００５を出力することができる。
【０１１７】
第４の変換例では、図１２に示すソースコード０００１から図１３に示す検査コード０００５と異なる図２４に示す検査コード０００５への変換例である。
【０１１８】
図２４に示す検査コード０００５について説明する。図１３に示す検査コード０００５では、行００２に示すようにselect文を利用している。select文は、非特許文献１に開示された検査ツールであるＳＰＩＮのバージョン６以降で追加された構文であり、検査ツールがバージョン５以前のＳＰＩＮである場合、select文を利用できない。このため、検査ツールがバージョン５以前のＳＰＩＮである場合、図２４の行１０１から行１１６に示すように、非決定的な実行を表現する構文を検査コード０００５に定義することによって、select文と等価な処理を表現する必要がある。
【０１１９】
本変換例において、図１２に示すソースコード０００１を図２４に示す検査コード０００５へ変換するためには、図１２に示すソースコード０００１を図１４に示す実装モデル１２０５で表現し、続いて、図１５で示される汎化モデル１２０６へ変換し、当該汎化モデル１２０６を抽象化して図１６に示す汎化モデル１２０６に変換する点までは、第１の変換例と同じである。図１６に示す汎化モデル１２０６を検査モデル１００８に変換する汎化−検査変換ルール１００７が第１の変換例と異なる。
【０１２０】
具体的には、第４の変換例の汎化−検査変換ルール１００７では、図１６に示す抽象化された汎化モデル１２０６のnameとして"random value genaration"を有するLogigal_Expression要素Ｏ０７０１の変換先の要素が変更される。この汎化−検査変換ルール１００７によって、図１６に示す汎化モデル１２０６は図２５に示す検査モデル１００８に変換される。
【０１２１】
本変換例で用いる汎化−検査変換ルール１００７では、図１６に示す抽象化された汎化モデル１２０６のLogical_Expression要素Ｏ０７０１と、最小値を示すAttribute要素Ｏ０７０２と、最大値を表すAttribute要素Ｏ０７０３との組合せは、図２５に示す検査モデル１００８の要素Ｏ０９０１〜０９０４の組合せに変換される。
【０１２２】
具体的には、図２５に示す検査モデル１００８のInlineFunctionCall要素Ｏ０９０５は、declarationのラベルを有するリンクＬ０９０１によって参照するInlineFunctionDeclaration要素Ｏ０９０１と、引数を示すargumentのラベルを有するリンクＬ０９０２によって参照するVariableReference要素Ｏ０９０２と、argumentのラベルを有するリンクＬ０９０３によって参照するIntegerConstant要素Ｏ０９０３と、argumentのラベルを有するリンクＬ０９０４によって参照するIntegerConstant要素Ｏ０９０４と、をこの順で所有する。なお、図２５では、InlineFunctionDeclaration要素Ｏ０９０１の宣言内部は省略されているが、InlineFunctionDeclaration要素Ｏ０９０１は、第１引数に変数をとり、第２引数に最小値をとり、第３引数に最大値をとり、非決定的な選択を実現するプログラム構造を所有するように宣言される。VariableReference要素Ｏ０９０２は、値の代入先となる変数を定義する。IntegerConstant要素Ｏ０９０３は最小値となる。IntegerConstant要素Ｏ０９０４は最大値となる。
【０１２３】
なお、図２５に示す検査モデル１００８から図２４に示す検査コード０００５が取得できる。
【０１２４】
以上のように、抽象化変換ルール１００６を用いて汎化モデル１２０６を抽象化する処理で、所定の条件に適合する要素を論理要素に変換する。これによって、出力する検査コード０００５の変更を管理者が所望する場合であっても、すべての変換ルール１００５〜１００７を変更する必要はなく、第１の変換例の汎化−検査変換ルール１００７のみを変更することによって、所望の検査コードを出力できる。したがって、バージョン５以前のＳＰＩＮである検査ツールを使用する場合には、第１の変換例の汎化−検査変換ルール１００７のみを変更するだけで、バージョン５以前のＳＰＩＮに対応させることができる
第２の変換例で用いた変換ルールのうち汎化−検査変換ルール１００７を第４の変換例で用いた汎化−検査変換ルール１００７に変更すれば、図１８に示すソースコード０００１を図２４に示す検査コード０００５に変換することも可能である。また、同様に、第３の変換例で用いた変換ルールのうち汎化−検査変換ルール１００７を第４の変換例で用いた汎化−検査変換ルール１００７に変更すれば、図１９に示すソースコード０００１を図２４に示す検査コード０００５に変換することも可能である。
【０１２５】
次に、汎化モデル１２０６に対する抽象化処理が複数回実行され、ある論理要素から異なる論理要素へ変換される第５の変換例について図２６〜図３２を用いて説明する。第５の変換例では、図２６に示すＣ言語によるソースコード０００１を図２７に示すＰｒｏｍｅｌａ言語による検査コード０００５へ変換する。
【０１２６】
図２６に示すソースコード０００１では、乱数を生成するrand()関数の戻り値を２で割った余りが０である場合にはdo_something1()関数が実行され、余りが０以外である場合にはdo_something2()関数が実行される。換言すれば、図２６に示すソースコード０００１は、do_something1()関数又はdo_something2()関数がランダムに選択され、選択された関数が実行されるプログラムを示す。
【０１２７】
図２６に示すソースコード０００１は、図２８に示す実装モデル１２０５によって表現される。また、図２８に示す実装モデル１２０５は、実装−汎化変換ルール１００５によって、図２９に示す汎化モデル１２０６に変換される。
【０１２８】
次に、図２９に示す汎化モデル１２０６は、第１の変換例と同じ抽象化変換ルール１００６によって抽象化され、図３０に示す汎化モデル１２０６に変換される。この変換において、図３０に示す汎化モデル１２０６における、rand関数の呼出し及びrand関数の戻り値を２で割った余りの算出に対応する、図２９に示すBinaryOperation要素Ｏ１１０１、FunctionCall要素Ｏ１１０２、FunctionDeclaration要素Ｏ１１０３、及びIntegerConstant要素１１０４の組合せは、図３０に示す汎化モデル１２０６における、Logical_Expression要素Ｏ１２０１、Attribute要素Ｏ１２０２、及びAttribute要素Ｏ１２０３の組合せに変換される。
【０１２９】
さらに、図３０に示す汎化モデル１２０６は、図３０に示す汎化モデル１２０６への変換に用いた抽象化変換ルール１００６と異なる抽象化変換ルール１００６によって、図３１に示す汎化モデル１２０６に変換される。この抽象化変換ルール１００６は、条件式に用いられる変数に乱数値が代入される選択的実行文を非決定的な選択的実行文に変換するものである。上述した選択的実行文は、換言すれば、二つの選択肢のうち一つ選択肢がランダムに選択される選択的実行文を示す論理要素に変換される。
【０１３０】
具体的には、図３０に示す汎化モデル１２０６のSelectionStatement要素Ｏ１２０４が図３１に示す汎化モデル１２０６のLogical_SelectionStatement要素Ｏ１３０１に変換される。この理由について以下に説明する。
【０１３１】
図３０に示す汎化モデル１２０６のVariableReference要素Ｏ１２０６は、name属性の値が”random value generation”であるLogical_Expression要素Ｏ１２０１が代入される変数を表す。また、当該VariableReference要素Ｏ１２０６は、リンクＬ１２０１を通じて推移的にSelectionItem要素Ｏ１２０５に接続され、当該SelectionItem要素Ｏ１２０５がSelectionStatement要素Ｏ１２０４に所有される。このため、SelectionStatement要素Ｏ１２０４は、条件式に用いられる変数に乱数値が代入される選択実行文に一致するので、非決定的な選択的実行文を表現する論理要素であるLogical_SelectionStatement要素Ｏ１３０１に変換される。
【０１３２】
また、図３０に示す汎化モデル１２０６におけるSelectionItem要素Ｏ１２０５からconditionラベルを有するリンクＬ１２０１で推移的に接続される要素は、do_something1()関数又はdo_something2()関数を選択するために、乱数を生成し、生成した乱数を２で割った余りが０であるか否かを判定する要素である。図３１に示す汎化モデル１２０６では、非決定的な選択的実行文を表現するLogical_SelectionStatement要素Ｏ１３０１が定義されたため、図３０に示す汎化モデル１２０６の上述した要素は不要となる。このため、これらの要素は削除される。
【０１３３】
以上によって、本変換例では、抽象化処理が複数回実行され、１回目の抽象化処理で変換された論理要素であるLogical_Expression要素Ｏ１２０１を含むSlectionStatement要素Ｏ１２０４は、２回目の抽象化処理で、論理要素であるLogical_SelectionStatement要素Ｏ１３０１に変換される。
【０１３４】
そして、図３１に示す汎化モデル１２０６は、汎化−検査変換ルール１００７によって、図３２に示す検査モデル１００８に変換され、図２７に示す検査コード０００５が出力される。
【０１３５】
以上のように、第５の変換例では、抽象化処理が複数回実行され、ある抽象化処理で変換された論理要素を他の抽象化処理でさらに論理要素に変換するので、より単純化された検査コードを出力でき、検査すべき状態数が膨大な分量となる状態爆発に至ることを防止できる。
【０１３６】
第５の変換例は、図２６に示すソースコード０００１と異なる乱数生成方法を用いるソースコード０００１に変更した場合であっても、第１の変換例〜第４の変換例と同じく、変更後の乱数生成方法に対応する変換ルールのみを変更すれば、他の変換ルールを変換しなくても、変更後のソースコード０００１を所望の検査コード０００５に変換できる。
【０１３７】
本実施例によれば、細粒度に分割された複数の変換ルールを入力するインタフェースを所有することによって、利用者による抽象化の水準の変更は、変換ルールを入力する操作により容易に実現される。すなわち、複数の細粒度の変換ルールを利用者が入力インタフェースにより選択できるため、図８Ａ、図８Ｂに示したような抽象化の水準を、状況に応じて利用者が容易に選定、変更することが可能となる。
【０１３８】
ソースコード変換方法は、複数の変換ルールを用いて検査対象のソースコードをモデルチェッカの入力言語で記述された検査コードへ変換する手順を有し、前記変換ルールは、実装−汎化変換ルールと、抽象化変換ルールと、汎化−検査変換ルールと、に分類され、変換が段階的に行われる。これにより、検査対象のソースコードの設計変更に追従する際には、複数の変換ルールの中の変更に関連する変換ルールのみを変更すればよく、変更が最小限にとどめられる。加えて、実装モデルと、汎化モデルと、検査モデルとをそれぞれメタモデルで定義し、制約を加えることにより、変換ルールによる変換結果が不正でないことを検証可能となる。これにより、検査対象のソースコードを検査コードへ抽象化しながら変換する一連の処理を、細粒度の変換ルールを組み合わせることで実現することによって生じる、変換ルールの検証コストの増大を防ぐことが出来る。
【０１３９】
また、細粒度に分割された複数の変換ルールを入力するインタフェースを所有することによって、利用者による抽象化の水準の変更は、検査したい性質、検査水準に応じて、利用者が変換ルールを選択・入力する操作で容易に実現される。これにより、抽象化の水準の変更が困難であるという課題が解決される。例えば、繰り返し実行時のみに発生する特定の不具合がある場合、その繰返しを除去することで、特定の不具合の検出はできなくなるものの、その繰返しを発生原因に含まない不具合の検出は可能であるままに、大幅に状態数を削減できる。
【０１４０】
さらに、モデルの変換ルールをデータベースに蓄積・再利用することで、検査対象ソースコードの設計変更や、別ソフトウェアへの応用に、低コストで対応可能になる。
【０１４１】
なお、異なる検査ツールにて検査するために、検査ツールの形式で出力する際には、メタ・検査モデルと、汎化−検査変換ルールのみを作成すればよく、作成部分が最小限に留められる。これによって、異なるモデルチェッカにて検査する際のコストを低減できる。
【０１４２】
また、汎化モデルを、検査モデルに変換するために用いる変換ルールにおいて、汎化モデルを直接検査モデルに変換する、又は、汎化モデル上にて物理要素間で変換を行う代わりに、いったん、汎化モデルにおいて論理要素への変換を行った上で、検査モデルへ変換することによって、変換ルールの共通化が可能となる。
【０１４３】
（第２の実施例）
図３３によって、本発明の第二の実施例のソースコード変換装置及び変換処理方法を説明する。この実施例においては、図３３に示す検査コード出力ステップＳ１０４に続き、変換ルール入力ステップＳ１０２へ進むことで、既に入力されたソースコード０００１を、繰り返し、異なる変換ルール集合０００２を用いて、変換する手順をとってもよい。また、ある実施形態においては、検査コード出力ステップＳ１０４に続き、変換ルール入力ステップＳ１０２へ進み、既に入力された変換ルール集合０００２の全てまたは一部と、新たに変換ルール入力ステップＳ１０２で入力された変換ルール集合０００２をあわせて、変換ルール集合０００２として用いてもよい。
【０１４４】
本実施例によれば、細粒度に分割された複数の変換ルールを入力するインタフェースを所有し、入力されたソースコードと、変換に用いた変換ルール集合を保存し、前記ソースコードを前記変換ルール集合の一部を入れ替えて変換できることによって、異なる抽象度の複数の検査コードを生成する場合などの、同一のソースコードを繰り返し変換する手間を削減できる。
【０１４５】
（第３の実施例）
図３４によって、本発明の第三の実施例のソースコード変換装置及び変換処理方法を説明する。本実施例では、ソースコードから検査コードを得る過程において生成される実装モデルと、汎化モデルと、検査モデルとを制約条件に基づいて検証するステップを有する。
【０１４６】
図３４を用いて、変換の妥当性の検証手順を詳細に説明する。
【０１４７】
特定の変換ルールが、その変換に際して対象モデルについての前提条件をもつ場合、変換対象のモデルにおいて、前記特定の変換ルールの前提条件が、他の変換ルールの適用によって満たされなくなることがあり得る。このように前提条件が満たされないときに前記特定の変換ルールによってモデル変換を実施すると、変換結果のモデルが不正な状態になり得る。また、単に変換ルールに誤りが含まれるときも、変換結果のモデルが不正な状態になり得る。
【０１４８】
本実施例では、ソフトウェアのソースコード０００１を入力するステップと、ソースコード情報１００１を有する実装モデル１２０５を特定のプログラミング言語に依存しない形式である中間形式（汎化モデル１２０６）へ変換する第１変換ルールを入力するステップと、中間形式に対して抽象化処理を行う第２変換ルールを入力するステップと、中間形式から検査コードの情報をもつ検査モデル１００８に変換する第３変換ルールを入力するステップと、ソフトウェアのソースコード０００１を解析して実装モデル１２０５へ変換するステップと、前記第１変換ルールを用いてソフトウェアのソースコード０００１を前記中間形式の汎化モデル１２０６へ変換するステップと、第２変換ルールを用いて、前記中間形式で表現されたソフトウェアを抽象化するステップと、第３変換ルールを用いて、前記中間形式を検査モデル１００８に変換するステップと、検査モデル１００８を用いて検証ツールの入力言語で記述された検査コード０００５を生成するステップと、前記各段階のモデルを各々第１の制約条件０３００、第２の制約条件０３０１、及び第３の制約条件０３０２に基づいて検証する充足性検証ステップと、を有する。
【０１４９】
前記各段階のモデルの、各々第１の制約条件０３００、第２の制約条件０３０１、及び第３の制約条件０３０２に基づく充足性検証は、例えば、非特許文献２に開示されるＭＯＦでメタモデルを記述することによって、又は非特許文献４に開示されるＯＣＬによりメタモデルにより定義されるモデルに対する制約条件を記述することによって、実現される。
【０１５０】
本実施例によれば、メタモデル及び制約条件を用いることで、変換ルール同士の衝突や変換ルールの不具合による変換の妥当性を保証できる。このモデル変換では、メタモデルによって定義された形式のモデルが生成される。また、制約条件を追加し、生成されたモデルの妥当性を制約条件０３００〜００３０２で充足性検証することができる。
【０１５１】
以上、本発明者によりなされた発明を実施形態に基づき具体的に説明したが、本発明は上述した実施形態に限定されるものではなく、その要旨を逸脱しない範囲で種々変更可能であることは言うまでもない。
【産業上の利用可能性】
【０１５２】
本願発明は、ソフトウェアのソースコードを検証ツールの入力言語で記述された検査コードに変換するソースコード変換方法に適用可能である。
【符号の説明】
【０１５３】
０００１  ソースコード
０００２  変換ルール
０００３  メタモデル
０００４  書出しモデル
０００５  検査コード
００３１  物理要素定義
００３２  論理要素定義
１０００  ソースコード変換装置
１１００  入力部
１２００  変換処理部
１３００  出力部
１４００  記憶部
１５００  制御部
２０００  モデル検査ツール
３０００  検査結果
【図１】
0005643971.tif 000002
【図２】
0005643971.tif 000003
【図３Ａ】
0005643971.tif 000004
【図３Ｂ】
0005643971.tif 000005
【図４】
0005643971.tif 000006
【図５Ａ】
0005643971.tif 000007
【図５Ｂ】
0005643971.tif 000008
【図６】
0005643971.tif 000009
【図７】
0005643971.tif 000010
【図８Ａ】
0005643971.tif 000011
【図８Ｂ】
0005643971.tif 000012
【図９】
0005643971.tif 000013
【図１０】
0005643971.tif 000014
【図１１】
0005643971.tif 000015
【図１２】
0005643971.tif 000016
【図１３】
0005643971.tif 000017
【図１４】
0005643971.tif 000018
【図１５】
0005643971.tif 000019
【図１６】
0005643971.tif 000020
【図１７】
0005643971.tif 000021
【図１８】
0005643971.tif 000022
【図１９】
0005643971.tif 000023
【図２０】
0005643971.tif 000024
【図２１】
0005643971.tif 000025
【図２２】
0005643971.tif 000026
【図２３】
0005643971.tif 000027
【図２４】
0005643971.tif 000028
【図２５】
0005643971.tif 000029
【図２６】
0005643971.tif 000030
【図２７】
0005643971.tif 000031
【図２８】
0005643971.tif 000032
【図２９】
0005643971.tif 000033
【図３０】
0005643971.tif 000034
【図３１】
0005643971.tif 000035
【図３２】
0005643971.tif 000036
【図３３】
0005643971.tif 000037
【図３４】
0005643971.tif 000038
【図３５】
0005643971.tif 000039