ソフトウェアのソースコードを、異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換するソースコード変換装置で実行されるソースコード変換方法であって、前記異なる複数の変換ルールは、前記ソースコードを前記検査コードへ変換し抽象化する一連の処理を、細粒度に分割したものであり、前記変換ルールは、前記ソースコードを特定のプログラミング言語に依存しない形式である中間形式へ変換する第1変換ルールと、前記変換された中間形式を抽象化する第2変換ルールと、前記抽象化された中間形式を前記検査コードに変換する第3変換ルールと、を含み、前記方法は、前記ソースコードを入力するステップと、少なくとも一つの前記第1変換ルールの入力を受け付けるステップと、少なくとも一つの前記第2変換ルールの入力を受け付けるステップと、少なくとも一つの前記第3変換ルールの入力を受け付けるステップと、前記入力された第1変換ルールを用いて、前記ソースコードを前記中間形式へ変換するステップと、前記入力された第2変換ルールを用いて、前記変換された中間形式を抽象化するステップと、前記入力された第3変換ルールを用いて、前記抽象化された中間形式を前記検査コードへ変換するステップと、を含み、前記中間形式は、前記ソースコード又は前記検査コードの要素と等価な要素である物理要素の他に、前記変換された中間形式を抽象化するステップで生成される要素である論理要素を表現可能であることを特徴とするソースコード変換方法。請求項1に記載のソースコード変換方法において、前記論理要素は、関連する物理要素への参照及び任意の情報を含み、前記変換された中間形式を抽象化するステップは、前記第2変換ルールで定められた所定の条件と合致する要素を前記論理要素に変換することによって、追加の属性情報を付与するステップを含み、前記検査コードに変換するステップは、前記論理要素を前記検査コードの要素と等価な要素に変換するステップを含むことを特徴とするソースコード変換方法。請求項1又は請求項2に記載のソースコード変換方法において、前記変換された中間形式を抽象化するステップは複数回実行可能であって、ある回の前記ソフトウェアを抽象化するステップで生成された論理要素は、当該回よりも後の回の前記ソフトウェアを抽象化するステップで新たな論理要素に変換されることを特徴とするソースコード変換方法。請求項1から請求項3のいずれか一つに記載のソースコード変換方法において、前記第1変換ルール、前記第2変換ルール、及び前記第3変換ルールの少なくとも一つは、前記ソースコード変換装置の内部に蓄積された複数の変換ルールの中から選択されることによって、入力が受け付けられることを特徴とするソースコード変換方法。請求項1から請求項4のいずれか一つに記載のソースコード変換方法において、前記第1変換ルール、前記第2変換ルール、及び前記第3変換ルールの少なくとも一つは、利用者の記述によって入力が受け付けられることを特徴とするソースコード変換方法。ソースコード変換装置によるソースコード変換方法であって、ソフトウェアのソースコードを入力するステップと、異なる複数の変換ルールを入力するステップと、前記ソースコードを、前記異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換するステップと、を含み、前記複数の変換ルールの少なくとも一部は、前記ソースコード変換装置の内部に蓄積された複数の変換ルールの中から選択して入力され、前記異なる複数の変換ルールは、前記ソースコードを、該ソースコードの記述言語に依存しない汎化されたプログラム情報をもつ汎化モデルへ変換する実装-汎化変換ルールと、前記汎化モデルを抽象化する抽象化変換ルールと、前記汎化モデルを前記検査コードへ変換する汎化-検査変換ルールとを含み、前記ソースコードを前記検査コードに変換するステップは、前記実装-汎化変換ルールを用いて、前記ソースコードを前記汎化モデルへ変換するステップと、前記抽象化変換ルールを用いて、前記汎化モデルを抽象化するステップと、前記汎化-検査変換ルールを用いて、前記汎化モデルを前記検査コードに変換するステップと、を含み、前記検査対象のソースコードを前記検査コードへ変換する一連のステップにおいて、内部的に保持される情報であるモデルの形式はメタモデルによって定義され、前記モデルは、前記ソースコードに対応する情報をもつ実装モデルと、前記汎化モデルと、前記検査コードに対応する情報をもつ検査モデルとを含み、前記実装モデルは、そのメタモデルであるメタ実装モデルによって定義され、前記汎化モデルは、そのメタモデルであるメタ汎化モデルによって定義され、前記検査モデルは、そのメタモデルであるメタ検査モデルによって定義され、前記各メタモデルは、データ構造の定義と、データに含まれる要素間の制約に関する情報とを保持し、前記メタ汎化モデルは、前記メタ実装モデルの要素に等価な要素である第1物理要素の定義と、前記メタ検査モデルの要素に等価な要素である第2物理要素の定義と、前記抽象化変換ルールを用いて前記汎化モデルを抽象化するステップで生成される要素である論理要素の定義と、を含むことを特徴とするソースコード変換方法。請求項6に記載のソースコード変換方法において、前記メタ汎化モデルでは、前記メタ汎化モデルで定義される前記論理要素が、前記メタ汎化モデルで定義される前記第1物理要素又は前記第2物理要素を継承するように定義されることを特徴とするソースコード変換方法。請求項6又は請求項7に記載のソースコード変換方法において、前記論理要素は、関連する物理要素への参照及び任意の情報を含み、前記汎化モデルを抽象化するステップは、前記抽象化変換ルールで定められた所定の条件と合致する要素を前記論理要素に変換することによって、追加の属性情報を付与するステップを含み、前記汎化モデルを前記検査コードに変換するステップは、前記論理要素を前記検査コードの要素と等価な要素に変換するステップを含むことを特徴とするソースコード変換方法。請求項6から請求項8のいずれか一つに記載のソースコード変換方法において、前記汎化モデルを前記検査コードに変換するステップは複数回実行可能であって、ある回の汎化モデルを抽象化するステップで生成された論理要素は、当該回よりも後の回の前記汎化モデルを抽象化するステップで新たな論理要素に変換されることを特徴とするソースコード変換方法。請求項6から請求項9のいずれか一つに記載のソースコード変換方法において、前記変換ルールに関する情報は、ソースコード変換装置の記憶部に格納された変換ルールを指し示す識別情報のみが含まれており、前記変換ルールの実体を、前記識別情報を用いて前記記憶部から取り出し、前記取り出された変換ルールの実態を変換に用いることを特徴とするソースコード変換方法。請求項6から請求項10のいずれか一つに記載のソースコード変換方法において、前記入力されたソースコードから、前記変換ルールの検索条件を抽出又は生成し、前記検索条件と合致する変換ルールを、ソースコード変換装置の記憶部から取得し、前記取得された変換ルールを前記変換ルールとして受け付けることを特徴とするソースコード変換方法。請求項6から請求項11のいずれか一つに記載のソースコード変換方法において、前記実装モデル、前記抽象プログラムモデル、及び前記検査モデルの各中間のモデルは、それぞれ構文を定義するメタモデルによってデータ構造と意味論が定義されることを特徴とするソースコード変換方法。プロセッサ及び記憶領域を備えるソースコード変換装置に、ソフトウェアのソースコードを、前記異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換する処理を実行させるソースコード変換プログラムであって、前記異なる複数の変換ルールは、前記ソースコードを前記検査コードへ変換し抽象化する一連の処理を、細粒度に分割したものであり、前記変換ルールは、前記ソースコードを特定のプログラミング言語に依存しない形式である中間形式へ変換する第1変換ルールと、前記変換された中間形式を抽象化する第2変換ルールと、前記抽象化された中間形式を前記検査コードへ変換する第3変換ルールと、を含み、前記処理は、前記ソースコードを入力するステップと、少なくとも一つの前記第1変換ルールの入力を受け付けるステップと、少なくとも一つの前記第2変換ルールの入力を受け付けるステップと、少なくとも一つの前記第3変換ルールの入力を受け付けるステップと、前記入力された第1変換ルールを用いて、前記ソースコードを前記中間形式へ変換するステップと、前記入力された第2変換ルールを用いて、前記変換された中間形式を抽象化するステップと、前記入力された第3変換ルールを用いて、前記抽象化された中間形式を前記検査コードへ変換するステップと、を含み、前記中間形式は、前記ソースコード又は前記検査コードの要素と等価な要素である物理要素の他に、前記変換された中間形式を抽象化するステップで生成される要素である論理要素を表現可能であることを特徴とするソースコード変換プログラム。モデル検査によるソフトウェアの信頼性確保を有効に実施するためには、ソースコードからモデルチェッカの入力言語で記述された検査コードを自動生成するなどの方法により、検査コードを得るための労力を低減させること、並びに、ソフトウェアの仕様及び設計を、モデルチェッカによる網羅的検査が現実的な時間計算量及び空間計算量で終了するように抽象化することが必要となる。特許文献1に開示される方法によると、抽象化記述の再利用性が低いという課題が存在する。特許文献1に開示される方法によると、モデル検査に必要な抽象化の手段である、翻訳マップ及び環境モデルは、ソースプログラムの改訂など、新しいタイプの命令がソースコード内に導入された場合に限定されているが、現実の検査においては、1新しいタイプの命令の導入に限らない、ソフトウェアの設計変更2対象ソフトウェアの抽象化方法の変更3異なるモデルチェッカによる検査への対応の3種類の変更があり得る。1の例としては、ソフトウェアの構造変更による、環境モデルとの対応付けの変更、及び、複数の命令をまたがる、手続きの変更があり得る。ソフトウェアは改訂ごとに構造変更が伴うことが多く、この種類の変更が頻繁に加わる。また、2の例としては、乱数等を関数の定数又は非決定的な値への置き換え、及び処理の簡略がある。現実的なソフトウェアのモデル検査では状態爆発が容易に生じるため、検査項目に応じた抽象化、及び、検査水準自体の調整が必要となる。3の例としては、異なる検査が可能なモデルチェッカへの変更、及び、もっと単純に、モデルチェッカのバージョン変更への対応があり得る。モデルチェッカはそれぞれに特長が存在するため、効果的な検査の為にはモデルチェッカの複数対応が望ましい。特許文献1に開示される方法によると、上述した3種類の変更のいずれに対応する場合にも、ソースコードの言語からモデルチェッカの言語へのマップである翻訳マップと、モデルチェッカの言語で記述された環境モデルとの、少なくとも一方を修正しなければならない。そのため、ある目的1例えば、抽象化方法の変更の為の変更を行った上で、異なる目的2例えば、設計変更の為の変更を行った時、これらの変更前の翻訳マップ及び環境モデルに対し、目的2及び新たな目的3例えば、モデルチェッカの変更の変更を行おうとした場合、最初に行った目的2の為の変更を再利用できず、新たに目的2と目的3とを同時に満たす変更を行わなければならない。本発明は、従来の技術の課題を踏まえ、抽象化記述の変更を柔軟に行うことができ、さらに、抽象化記述を効率的に再利用可能な、ソースコード変換方法及びソースコード変換プログラムを提供することを目的とする。本発明の代表的な一例を示せば、ソフトウェアのソースコードを、異なる複数の変換ルールを用いて、検証ツールの入力言語で記述された検査コードに変換するソースコード変換装置で実行されるソースコード変換方法であって、前記異なる複数の変換ルールは、前記ソースコードを前記検査コードへ変換し抽象化する一連の処理を、細粒度に分割したものであり、前記変換ルールは、前記ソースコードを特定のプログラミング言語に依存しない形式である中間形式へ変換する第1変換ルールと、前記変換された中間形式を抽象化する第2変換ルールと、前記変換された中間形式を前記検査コードに変換する第3変換ルールと、を含み、前記方法は、前記ソースコードを入力するステップと、少なくとも一つの前記第1変換ルールの入力を受け付けるステップと、少なくとも一つの前記第2変換ルールの入力を受け付けるステップと、少なくとも一つの前記第3変換ルールの入力を受け付けるステップと、前記入力された第1変換ルールを用いて、前記ソースコードを前記中間形式へ変換するステップと、前記入力された第2変換ルールを用いて、前記変換された中間形式を抽象化するステップと、前記入力された第3変換ルールを用いて、前記変換された中間形式を前記検査コードへ変換するステップと、を含み、前記中間形式は、前記ソースコード又は前記検査コードの要素と等価な要素である物理要素の他に、前記変換された中間形式を抽象化するステップで生成される要素である論理要素を表現可能であることを特徴とする。本願において開示される発明のうち代表的なものによって得られる効果を簡潔に説明すれば、下記の通りである。すなわち、抽象化記述の変更を柔軟に行うことができ、さらに、抽象化記述を効率的に再利用可能な、ソースコード変換方法及びソースコード変換プログラムを提供できる。本発明では、異なる複数の変換ルールを用いて検査対象のソースコードをモデルチェッカの入力言語で記述された検査コードへ変換する。前記異なる複数の変換ルールは、検査対象のソースコードをモデルチェッカの入力言語で記述された検査コードへ変換し、抽象化する一連の処理を細粒度に分割したものであり、複数の変換ルールを組み合わせて用いることにより、前記ソースコードから前記検査コードへの変換が実現される。本発明において、検査対象のソースコードを検査コードへ変換する一連の処理を、抽象化の処理も含めて、細粒度に分割し、分割されたそれぞれを、変換ルールと呼ぶ。本発明により実現されるソースコード変換装置は、ソースコードを検査コードへ変換する場合、異なる複数の変換ルールが、利用者によって、選択され、又は入力されるためのインタフェースを所有する。前記変換ルールは、事前にソースコード変換装置内部に蓄積された複数の変換ルールの中からの選択と、利用者の記述と、のいずれかの手段により入力される。また、本発明において、変換ルールは、ソースコードを、前記ソースコードの記述言語に依存しない、汎化されたプログラム情報をもつ形式汎化モデルへ変換する実装-汎化変換ルールと、汎化モデルを抽象化する抽象化変換ルールと、汎化モデルをモデルチェッカの記述言語へ変換する汎化-検査変換ルールに分類される。換言すると、異なる複数の変換ルールは、ソースコードを特定のプログラミング言語に依存しない形式である中間形式へ変換する第1変換ルールと、前記中間形式に対して抽象化処理を行う第2変換ルールと、前記中間形式から前記検査コードに変換する第3変換ルールとに分類される。ソースコードから検査コードへの変換は、ソースコードを、実装-汎化変換ルールにより、汎化モデルへ変換するステップと、前記汎化モデルを、抽象化変換ルールにより抽象化するステップと、前記汎化モデルを、汎化-検査変換ルールにより、検査コードへ変換するステップと、の3つのステップを続けて行うことで実現される。換言すると、ソースコードから検査コードへの変換は、前記第1、第2、第3の変換ルールを各々1つ以上入力するステップと、前記第1変換ルールを用いて、ソフトウェアのソースコードを、前記中間形式へ変換するステップと、前記第2変換ルールを用いて、前記中間形式で表現されたソフトウェアを抽象化するステップと、前記第3変換ルールを用いて、前記中間形式を検証ツールの入力言語で記述された検証用コードに変換するステップの3つのステップを続けて行うことで実現される。また、本発明において、検査対象のソースコードを、検査コードへ変換する一連の処理にて、内部的に保持される情報モデルは、その形式をメタモデルにより定義される。前記モデルは、検査対象のソースコードに対応する情報をもつ実装モデルと、前述の汎化モデルと、モデルチェッカの記述言語に対応する情報をもつ検査モデルと、に分類される。実装モデルは、そのメタモデルであるメタ実装モデルにより定義され、汎化モデルは、そのメタモデルであるメタ汎化モデルにより定義され、検査モデルは、そのメタモデルであるメタ検査モデルにより定義される。前述のそれぞれのメタモデルは、データ構造の定義と、データに含まれる要素間の制約に関する情報とを保有する。また、本発明において、汎化モデルには、実装モデルもしくは検査モデルの要素に対応付く等価な要素が存在する物理要素と、抽象化の変換の過程で用いる論理要素との、2種類の要素が含まれる。論理要素は、属性情報と、関連する物理要素への参照を持つことができる、物理要素の特性を継承した要素である。物理要素それぞれには、対応した論理要素が存在する。例えば、物理要素を、対応した論理要素に置き換えることで追加の属性情報を与えること、新たな論理要素へ置き換えること、及び、論理要素を異なる物理要素へ置き換えることを、変換ルールとして記述することにより、抽象化記述を段階ごとに再利用可能とすることができる。以下、図面を参照して本発明の実施形態について詳しく説明する。まず、図1、図2を参照しながら本発明の基本概念を説明する。本発明では、図1に示すように、ソースコード0001に対して、ソースコード変換装置1000において、複数の変換ルール0002を組み合わせた変換処理を行うことにより、既存モデル検査装置に適合した検査コード0005へ変換する。すなわち、a変換を細粒度に分割し、複数の変換ルール0002の組み合わせとしてパッケージ化することで、柔軟な変換を実現する。b利用者検査者は、検査対象のソースコード0001を入力し、対象のソースコードと検査水準に応じた変換ルール0002を選択して、所望の検査コード0005を得る。本発明における、変換ルールの例を挙げると次の通りである。a単純な構文変換C言語の条件分岐を、検査コードの条件分岐に変換C言語の繰り返し文for文while文...を、検査コードの繰り返しに変換b外部環境のモデル化データ読込みを、ランダム入力へ置き換えc抽象化繰り返しの除去条件の簡略化図2により、本発明のソースコード変換処理における変換ルールの入力インタフェースについて、説明する。本発明によれば、細粒度に分割された複数の変換ルール0002を入力するインタフェースを所有するので、利用者による抽象化の変更は、複数の異なる変換ルール0002を選択入力する操作により容易に実現される。すなわち、利用者による抽象化の水準の変更は、ドメイン情報、検査したい性質、及び検査水準の情報抽象化による性質への影響に応じて、利用者が複数の異なる変換ルール0002を選択して呼び出し、ソースコード変換装置1000へ入力する操作により容易に実現される。本発明によれば、異なる複数の変換ルール0002を用いて検査対象のソースコード0001をモデルチェッカの入力言語で記述された検査コード0005へ変換する手順を含んでいる。前記異なる複数の変換ルールは、実装-汎化変換ルールと、抽象化変換ルールと、汎化-検査変換ルールとに分類され、これらの変換ルールを用いた変換は段階的に実行される。検査対象のソースコードの設計変更に追従する際には、変更に関連する変換ルールのみを変更すればよく、変更が最小限にとどめられる。加えて、実装モデルと、汎化モデルと、検査モデルとをそれぞれメタモデルで定義し、制約を加えることにより、変換ルールによる変換結果が不正でないことを検証可能となる。これによって、本実施形態では、検査対象のソースコードを検査コードへ抽象化しながら変換する一連の処理は、細粒度の変換ルールを組み合わせることで実現されるが、このような一連の処理の実現方法によって生じる変換ルールの検証コストの増大を防ぐことができる。また、異なる検査ツールにて検査するために、前記検査ツールの形式で出力する際には、メタ検査モデルと、汎化-検査変換ルールのみを作成すればよく、作成部分が最小限にとどめられる。第1の実施例次に、本発明の第1の実施例になるソースコード変換装置及び変換処理方法を、図3Aから図32を参照しながら説明する。図3Aは、第一の実施例となるソースコード変換装置を含むソースコード変換システムの構成例を示す図である。本発明の実施形態に適用されるソースコード変換装置1000は、検査対象のソースコード0001を検査コード0005に変換する装置であり、入力部1100と、変換処理部1200と、出力部1300と、記憶部1400と、制御部1500とを備える。2000はモデル検査ツール、3000は検査結果を示す。入力部1100は、ソースコード0001及び変換ルール0002の入力を受け付ける。記憶部1400には、変換ルール0002、メタモデル0003、及び書出しルール0004が格納される。メタモデル0003は、変換処理部1200によるソースコード001を検査コード0005へ変換する一連の処理で内部的に保持されるモデルの形式を定義するためのデータである。メタモデル0003は、上述したように、データ構造の定義と、データに含まれる要素間の制約に関する情報とを保有する。なお、データに含まれる要素は物理要素及び論理要素を含み、物理要素に関する情報を物理要素定義0031といい、論理要素に関する情報を論理要素定義0032という。変換処理部1200は、検査対象のソースコード0001を変換ルール0002に基づいて検査コード0005に変換する。出力部1300は書出しルール0004に基づいて検査コード0005を出力する。制御部1500は、ソースコード変換装置1000の全体の処理を制御するための各種処理を実行するプロセッサである。図3Bに、ソースコード変換装置1000の構成例を示す。入力部1100は、ソースコード入力部1101、及び変換ルール入力部1102を有する。変換処理部1200は、モデル構築部1201、実装-汎化モデル変換部1202、抽象化モデル変換部1203、及び、汎化-検査モデル変換部1204を有する。出力部1300は、検査コード書出し部1301を有する。記憶部1400は、変換ルールデータベース1401、メタモデルデータベース1402、及び、書出しルールデータベース1403を有する。ソースコード変換装置1000は、例えば、1台のコンピュータ、又は、ネットワークを介して接続された複数のコンピュータ上で動作するプログラムとして実施される。ソースコード0001と変換ルール集合0002とは、例えば、コンピュータ上の記憶装置から読込む方法と、コンピュータに接続された入力デバイスにより直接入力される方法等の方法により入力される。また、検査コード0005は、例えば、コンピュータ上の記憶装置に書出す方法と、コンピュータのディスプレイ装置に表示する方法により出力される。入力部1100は、ユーザによって入力されるデータを受付け、入力されたデータを変換処理部1200へ供給する処理を行う。入力部1100は、ソースコード0001に関する情報と、細粒度に分割された複数の変換ルール、すなわち変換ルール集合0002に関する情報とを受付け、変換処理部1200へ供給する。ある実施形態においては、入力部1100は、ユーザによる、変換処理部の駆動や制御、出力部の駆動や制御、に関する指示を受け付けてもよい。変換処理部1200には、入力部1100から、ソースコード0001の情報と、ソースコード0001に適用すべき変換ルール集合0002の情報とが供給される。また、変換処理部1200は、ソースコード0001を、変換ルール集合0002により変換する処理を行い、変換結果の情報を、出力部1300に供給する。ある実施形態においては、入力部1100から供給される変換ルール集合0002に関する情報は、記憶部1400に格納された変換ルール0002を指し示す識別情報のみが含まれていて、変換ルール集合0002の実体を、前記識別情報を用いて記憶部1400から取り出し、変換に用いてもよい。図6を用いて、変換処理部1200及び出力部1300の詳細ついて説明する。変換処理部1200は、モデル構築部1201と、実装-汎化モデル変換部1202と、抽象化モデル変換部1203と、汎化-検査モデル変換部1204とを有する。本実施形態において、変換処理部1200は、メタモデル0003図3A参照と、変換ルール0002を用いたモデル変換により、ソースコード情報1001を、検査モデル1008へ変換する。メタ実装モデル1002と、メタ汎化モデル1003と、メタ検査モデル1004とは、例えば、非特許文献2に記載のMOFにて記述する。また、例えば、非特許文献3に記載されているQVTにて、実装-汎化変換ルール1005と、抽象化変換ルール1006と、汎化-検査変換ルール1007とを記述し、モデルの変換を行う。前記変換は、既に例示した方法の他のモデル変換方法でもよく、また、複数の方法を混在させてもよい。また、ある実施形態においては、実装-汎化モデル変換部1202と、抽象化モデル変換部1203と、汎化-検査モデル変換部1204とをそれぞれ独立させず、同一の部位により行われても良く、さらに、実装モデル1205と、汎化モデル1206と、検査モデル1008と、のそれぞれのメタモデルとして、メタ実装モデル1002と、メタ汎化モデル1003と、メタ検査モデル1004とを個別に用意せず、単一のメタモデルにより、実装モデル1205と、汎化モデル1206と、検査モデル1008とを定義してもよい。また、ある実施例においては、メタ実装モデル1002と、メタ汎化モデル1003と、メタ検査モデル1004と、は、複数の方式により、それぞれ実装モデル1205、汎化モデル1206、検査モデル1008、の形式や制約を定義してもよい。例えば、それぞれのメタモデルは、前記MOFによる定義のほかに、非特許文献4に記載されているOCLにて記載された制約条件を含み、モデルの変換を行った際に、制約条件を満たしているかどうかの検証を行う方法があり得る。モデル構築部1201は、ソースコード入力部1101からソースコード情報1001を受け取り、実装モデル1205へ変換する。実装モデル1205の形式は、そのメタモデルであるメタ実装モデル1002により、定義される。実装モデル1205は、本発明の効果を最大限に得るためには、ソースコード情報1001と相互に変換するのに必要十分な情報を持つことが望ましいが、ある実施形態によっては、検査コードを出力するという目的を逸しない程度にて、情報の省略や、追加があってもかまわない。ある実施形態においては、モデル構築部1201は、ソースコード入力部1101と不可分な様態で実装され、ソースコード情報1001が生じない形態で処理が進んでもよい。実装-汎化モデル変換部1202は、実装-汎化変換ルール1005と、メタ実装モデル1002と、メタ汎化モデル1003とを用いて、実装モデル1205を汎化モデル1206へ変換する。汎化モデル1206は、複数のプログラミング言語における構造及び処理を表現可能なデータ構造をもつ。例えば、汎化モデル1206中では、ソースコード0001におけるIf文とSwitch文とを区別せず、選択的実行文として表現する。ある実施形態においては、実装モデル1205を、汎化モデル1206へ変換する際、実装-汎化変換ルール1005のみを用いることもあり得る。また、ある実施形態において、実装-汎化変換ルール1005が、複数の変換ルールを含む場合には、複数の変換ルールを統合して一つの変換ルールとし、実装モデル1205から汎化モデル1206への変換に利用する方法があり得る。また、ある実施形態において、実装-汎化変換ルール1005が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、実装モデル1205から汎化モデル1206への変換を行う手順があり得る。抽象化モデル変換部1203は、抽象化変換ルール1006と、メタ汎化モデル1003とを用いて、汎化モデル1206の抽象化を行う。抽象化の例としては、選択文における条件式を、恒真、もしくは恒偽、又は非決定的な選択で置き換える方法があり得る。ある実施形態においては、汎化モデル1206を抽象化する際、抽象化変換ルール1006のみを用いることもあり得る。また、ある実施形態において、抽象化変換ルール1006が、複数の変換ルールを含む場合には、複数の変換ルールを統合して一つの変換ルールとし、汎化モデル1206の抽象化に用いる方法があり得る。また、ある実施形態において、抽象化変換ルール1006が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、汎化モデル1206の変換を行う手順があり得る。汎化-検査モデル変換部1204は、汎化-検査変換ルール1007と、メタ汎化モデル1003と、メタ検査モデル1004とを用いて、汎化モデル1206を、検査モデル1008へ変換する。例えば、検査コード0005がPromela形式である場合、汎化モデルにおいて選択的実行文として表現された要素は、検査モデルにおいてはIf文として表現される。ある実施形態においては、汎化モデル1206を、検査モデル1008へ変換する際、汎化-検査変換ルール1007のみを用いることもあり得る。また、ある実施形態において、汎化-検査変換ルール1007が、複数の変換ルールを含む場合には、複数の変換ルールを統合して1つの変換ルールとし、汎化モデル1206から検査モデル1008への変換に利用する方法があり得る。また、ある実施形態において、汎化-検査変換ルール1007が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、汎化モデル1206から検査モデル1008への変換を行う手順があり得る。出力部1300は、変換処理部1200より供給された、変換結果の情報を用いて、検査コード0005を出力する。ある実施形態においては、検査コード0005の出力に際して、例えばモデルチェッカの記述言語の文法情報などの情報を記憶部1400から供給されてもよい。検査コード書出し部1301は、メタ検査モデル1004と、記憶部1400の書出しルールデータベース1403から取得した検査コード書出しルール1009とを用いて、検査モデル1008を検査コード0005へ変換する。例えば、非特許文献5に記載される方法にて、検査コード書出しルール1009を記述し、検査モデル1008から、検査コード0005への変換を行う。ある実施例においては、これに限らず、検査モデル1008を、検査に利用するモデルチェッカの記述形式へ変換する任意の方法でもよい。検査コード0005は、例えば、モデルチェッカとしてSPINを用いる場合には、SPINの入力言語である、Promela言語により記述される。記憶部1400において、変換ルールデータベース1401、メタモデルデータベース1402、及び書出しルールデータベース1403のそれぞれは、例えば、関係データベース、又は、階層型データベースなどの、コンピュータ上にて実現される任意のデータ格納方式で実現される。変換ルールデータベース1401と、メタモデルデータベース1402と、書出しルールデータベース1403と、は互いに同一の方式で実現されている必要性は無く、互いに異なる方式で実現されていてもよい。また、変換ルールデータベース1401と、メタモデルデータベース1402と、書出しルールデータベース1403と、のそれぞれは、単一の方式で実現されている必要性は無く、例えば、保有すべき情報の一部を関係データベースに格納し、保有すべき情報の一部を、発明を実現するコンピュータプログラム中に組込むなど、それぞれ異なる方式の組合せで実現されていてもよい。記憶部1400は、入力部1100と、変換処理部1200と、出力部1300とが、それぞれの処理を行うのに必要な情報を供給する。例えば、記憶部1400は、変換ルールに関する情報と、メタモデルに関する情報と、モデルチェッカの記述言語の文法に関する情報とを格納する。変換ルールデータベース1401は、既に述べたとおり、変換ルールを、メタデータとともに保有する。前記メタデータは、変換ルールを選択するためのものであり、実装-汎化変換ルール1005と、抽象化変換ルール1006と、汎化-検査変換ルール1007の、それぞれ異なる情報を持つ方法があり得る。実装-汎化変換ルール1005のメタデータは、例えば、変換元ソースコードの記述言語の種類があり得る。抽象化変換ルール1006のメタデータは、例えば、抽象化を分かりやすく端的に表現した名前、簡単な説明、データの抽象化、処理の抽象化などの抽象化の種別、自然語例えばアルファベット又は数値で表現された抽象化による状態数削減効果、自然語例えばアルファベット又は数値で表現された抽象化による性質への影響、及び抽象化の適用できるソフトウェアのドメイン、があり得る。汎化-検査変換ルール1007のメタデータは、例えば、検査に使用するモデルチェッカを指し示す名前があり得る。以降、図4ないし図6を参照しながら入力部1100、変換処理部1200、出力部1300、記憶部1400、及び制御部1500の詳細を説明する。まず、本実施例におけるソースコード変換手順の一例を、図4及び図6を参照しながら説明する。本実施例におけるソースコード変換手順は、ソースコード入力ステップS101と、変換ルール入力ステップS102と、変換ルール適用ステップS103と、検査コード出力ステップS104と、を含む。このソースコード変換手順は、制御部1500が主体となって実行される。まず、ソースコード入力ステップS101において、ソースコード入力部1101により、ソースコード0001がソースコード変換装置1000に読み込まれ、ソースコード情報1001へ変換される。ソースコード入力部1101は、利用者から入力された検査対象のソースコード0001を受け付け、ソースコード情報1001へ変換する。ソースコード0001は、例えば、JISX30101993に公開されるプログラミング言語Cにより記述される。ソースコード情報1001は、具体的には、例えば抽象構文木の形式で保持される。ソースコード情報1001の形式は、抽象構文木に限らず、構造や論理などソースコード0001の検査に要する情報を保持する、任意の形式でもよい。ソースコード入力ステップS101に続き、変換ルール入力ステップS102において、変換ルール入力部1102により、細粒度に分割された複数の変換ルールである変換ルール集合0002がソースコード変換装置1000に読み込まれる。この変換ルール入力ステップS102では、変換前のモデルの要素と変換後のモデル要素との対応関係、及び変換によって変換前のモデルの要素に加えられる操作の少なくとも一方が定義される。変換ルール集合0002をソースコード変換装置1000に読み込む処理は、利用者による一度の操作で行われる必要性は無く、繰り返し操作により行われてもよい。また、ソースコード入力ステップS101、及び変換ルール入力ステップS102は、必ずしもこの順番で完了する必要性は無く、ソースコード入力部1101によりソースコード情報1001が生成される前にソースコード0001が入力され、かつ、変換ルール入力部1102が変換ルール入力処理のためにソースコード情報1001を要求する前にソースコード0001が入力されていればよい。したがって、ソースコード入力ステップS101の処理と、変換ルール入力ステップS102の処理とが混在する順番で処理がすすんでもよい。例えば、ソースコード入力部1101がソースコード0001を受け付け、続いて、変換ルール入力部1102が、変換ルール集合0002を受け付け、続いて、ソースコード入力部1101が、ソースコード0001をソースコード情報1001へ変換する、手順があり得る。変換ルール入力部1102は、利用者から入力された変換ルール集合0002を受け付ける。利用者から変換ルール集合0002を受け付ける方法は、例えば、次に示す方法があり得る。一つめの変換ルール入力方法の例として、変換ルール入力部1102は、変換ルール集合0002の一部として、利用者が手作業で直接入力した変換ルールを受け取る。二つめの変換ルール入力方法の例として、図5Aに示すように、変換ルール集合0002の少なくとも一部は、利用者が記述した変換ルール記述0010により入力してもよい。また、入力部1100が、記憶部1400から変換ルールの一覧0015を取得し、取得した変換ルールの一覧0015を利用者に一覧などの形式で提示し、前記提示された一覧から変換ルールを利用者が選択することによって、変換ルール集合0002の入力を受け付けてもよい。すなわち、利用者が、変換ルールの入力に前置して、変換ルールの検索条件0011を入力部1100の変換ルール入力部1102に入力記述し、続いて、変換ルール入力部1102が、前記検索条件に合致する変換ルールを、記憶部1400が有する変換ルールデータベース1401から取得し変換ルール一覧0015として前記利用者に提示する。続いて、前記利用者が、提示された前記変換ルール一覧0015に含まれる一つ以上の変換ルールを選択する。この利用者によって選択された一つ以上の変換ルールを、変換ルール入力部1102が、変換ルール集合0002の一部として受け付ける。三つめの変換ルール入力方法の例として、まず、利用者が、変換ルールの入力に前置して、変換ルールの検索条件0011を変換ルール入力部1102に入力し、続いて、変換ルール入力部1102が、前記検索条件に合致する変換ルールを、変換ルールデータベース1401から取得して、変換ルール集合0002の一部として受け付けてもよい。四つめの変換ルール入力方法の例として、図5Bに示すように、入力されたソースコード0001から、変換ルール入力部1102が、変換ルールの検索条件0012を抽出、生成し、さらに、前記検索条件に合致する変換ルールを、変換ルールデータベース1401から取得し、変換ルール集合0002の一部として受け付ける。二つめの変換ルール入力方法の例と、三つめの変換ルール入力方法の例と、四つめの変換ルール入力方法の例における、変換ルール検索条件の因子としては、例えば、後述する、変換ルールデータベース1401において、変換ルールのメタデータとして格納される情報があり得る。また、五つめの変換ルール入力方法の例として、変換ルール入力部1102は、何らかの方法で入力された変換ルールを加工することにより、変換ルールを受け付ける。前記加工方法の例としては、変換ルールデータベース1401には、ソースコード0001中の変数名などをパラメタ化した状態で変換ルールを保持しておき、例えば利用者の明示的な入力による方法などにより、ソースコード0001の情報にてパラメタを埋めたものを、変換ルール集合0002に含める方法があり得る。五つめの変換ルール入力方法の例において、加工元の変換ルールの入力方法としては、既に述べた一つめの変換ルール入力方法の例など、入力された変換ルールを加工せずに用いる場合と同様の方法があり得る。変換ルール入力部1102が、変換ルール集合0002を受け付ける方法は、これらの変換ルール入力方法に限らず、変換処理部1200で用いる変換ルールの集合を受け付ける任意の方法でよく、また、これらの変換ルール入力方法の一つ以上の組合せにより変換ルール集合0002を受け付けてもよい。変換ルール入力ステップS102に続き、変換ルール適用ステップS103において、モデル構築部1201がソースコード情報1001を実装モデル1205へ変換し、続いて、実装-汎化モデル変換部1202が実装モデル1205を汎化モデル1206へ変換しS1031、続いて、抽象化モデル変換部1203が汎化モデル1206を抽象化しS1032、続いて、汎化-検査モデル変換部1204が汎化モデル1206を検査モデル1008へ変換するS1033。変換ルール入力ステップS102と、変換ルール適用ステップS103とは、必ずしもこの順番で処理が完了する必要性は無く、実装-汎化モデル変換部1202の処理までに実装-汎化変換ルール1005が入力され、かつ、抽象化モデル変換部1203の処理までに抽象化変換ルール1006が入力され、かつ、汎化-検査モデル変換部の処理までに汎化-検査変換ルール1007が入力されていればよい。変換ルール適用ステップS103に続き、検査コード出力ステップS104において、検査コード書出し部1301により、検査モデル1008が、検査コード0005として書き出される。検査コード0005の書出し先の指定は、必ずしも変換ルール適用ステップS103の後である必要性は無く、検査コード0005の書出しよりも先であればよい。例えば検査コード0005の書出し先の指定がソースコード入力ステップS101と平行して行われる手順があり得る。次に、図7、図8A、図8Bを用いて、変換の手順をより詳細に説明する。図7に示すように、本発明では、モデル変換技術を利用し、段階的に変換するために、次のような処理を行う。1ソースコード0001をこれとほぼ等価な実装モデル1205へ変換2実装モデルを特定のプログラミング言語に依存しない形式にて構造及び論理などのプログラム情報を表現する汎化モデル1206へ変換すなわち、異なる複数の第1変換ルール1005-1~1005-nの少なくとも一つを用いて、実装モデル1205を特定のプログラミング言語に依存しない形式である中間形式の汎化モデル1206へ変換する。図7の例では、第1変換ルールとして、if文→条件分岐、switch文→条件分岐、while文→繰り返し、及びfor文→繰り返しの少なくとも四つの異なる変換ルールが選択されている。3汎化モデル1206に対して、抽象化のための変換を実施すなわち、異なる複数の第2変換ルール1006-1~1006-nの少なくとも一つを用いて、前記中間形式の汎化モデル1206に対して抽象化処理を行う。図7の例では、第2変換ルールとして、データ読み込み→ランダム入力、及びデータの抽象化の少なくとも二つの異なる変換ルールが選択されている。4汎化モデル1206を、検査モデル1008に変換し、コード生成出力すなわち、異なる複数の第3変換ルール1007-1~1007-nの少なくとも一つを用いて、前記中間形式の汎化モデル1206から検査コードの生成に要する情報を有する検査モデル1008に変換する。図7の例では、第3変換ルールとして、第1変換ルールに対応した条件分岐→if文、及び繰り返し→do文の少なくとも二つの異なる変換ルールが選択されている。また、実装モデル1205、汎化モデル1206、検査モデル1008は、それぞれ構文を定義するメタモデルによりデータ構造及び意味論が定義される。このように、実装モデル1205から汎化モデル1206への変換に際しては、例えば、変換対象ソースコードの記述言語の文法が、繰り返し処理の記法としてfor文及びwhile文を含む場合、使用者がfor文を繰り返しへ変換するルールと、While文を繰り返しへ変換するルールとを、既に述べた変換ルール入力方法を用いて、第1変換ルールとして選択する。汎化モデル1206の抽象化の変換に際しては、使用者が検査水準抽象化の度合いを決定し、決定した検査水準を達成する変換ルールとして、例えば、外部データの読込みに関する命令及び一連の処理をランダムな入力へ変換するルールと、特定のデータ型をより抽象度の高い型へ変換するルールとを、既に述べた変換ルール入力方法を用いて、第2変換ルール1006として選択する。さらに、汎化モデル1206から検査モデル1008への変換に当たっては、例えば、モデルチェッカの入力言語の文法が、繰り返し処理の記法としてdo文をもつとき、使用者が繰り返しをdo文へ変換するルールを、既に述べた変換ルール入力方法を用いて、第3変換ルール1007として選択する。変換ルールは、複数のソフトウェアにまたがって適用可能な汎用的なルールなど、繰り返し利用可能なものがデータベース化される。データベースに格納された変換ルールは、使用者による検索及びルール選択の判断材料として用いられるメタ情報として、ドメイン情報や検査水準抽象化による検査への影響の情報を有する。また、変換ルールの選択方法としては、次のようなものがある。1汎用的なルール:常に選択2特定のライブラリに依存したルール:使用ライブラリ、及び検査対象のドメインを入力することで、まとめて選択3抽象化に対応したルール:検査したい性質検査水準を入力して得た変換ルール一覧から、利用者が選択、もしくは利用者自身が記述して入力、もしくは検査したい性質などから、自動生成。図8A、図8Bに、それぞれモデルの抽象化の一例を示す。モデルの抽象化により、状態数を削減することができる。しかし、抽象化によりモデルの性質に影響を与えることがある。例えば、検出された欠陥反例が、もとのシステムに存在しない、もとのシステムに存在する欠陥を発見できない、等である。一方で、性質に影響を与えない健全な抽象化は、状態数削減効果が小さい傾向がある。図9に、メタ実装モデル1002の一例の一部を示し、図10にメタ汎化モデル1003の一例の一部を示し、図11にメタ検査モデル1004の一例の一部を示す。本実施例におけるメタ実装モデル1002と、メタ汎化モデル1003と、メタ検査モデル1004とは、非特許文献2に開示される記法を用いて示されている。例えば、図9において、IfStatementクラスC101は、関係R101によりStatementクラスC102を継承することが示され、関係R102により、属性conditionとしてExpressionクラスC103を所有することが示され、関係R103により、属性bodyとしてStatementクラスC102の集合を所有することが示され、関係R104により属性elseBodyとしてStatementクラスC102の集合を所有することが示されている。また、例えば、図9において、IntegerConstantクラスC104は、整数値である属性valueを所有することが示され、関係R105により、ExpressionクラスC103を継承すること等が示されている。また、例えば、図9において、VariableReferenceクラスC105は、関係R106により、ExpressionクラスC103を継承することが示され、関係R107により、VariableDeclarationクラスC106を参照することが示されている。メタ実装モデル1002の各要素、及び、メタ検査モデル1004の各要素には、それぞれ、実装プログラミング言語の言語要素、及び、検査用言語の言語要素に対応付く要素が含まれる。本実施例においては、実装プログラミング言語はC言語であり、検査用言語はPromela言語であるため、それぞれ、メタ実装モデル1002はC言語の言語要素と対応付く要素を含み、、メタ検査モデル1004はPromela言語の言語要素と対応付く要素を含む。例えば、図9におけるIfStatementクラスC101は、C言語におけるIf文を表現し、IntegerConstantクラスC104は、C言語における整数型定数値を表現している。図10に示すメタ汎化モデル1003には、メタ実装モデル1002に含まれる要素と意味的に対応付く要素であるか、メタ検査モデル1004に含まれる要素と意味的に対応付く要素である、物理要素が含まれる。本実施例におけるメタ汎化モデル1003においては、物理要素は、図10において、PhysicalElementクラスC201を推移的に継承する要素として表現されている。例えば、StatementクラスC203及びSelectionStatementクラスC204が、物理要素の一例である。それぞれの物理要素は、メタ実装モデル1002に含まれる要素、又はメタ検査モデル1004に含まれる要素と、一対一で対応付く必要は無く、複数の要素の組合せで、等価な意味を持つ言語要素を表現できればよい。例えば、本実施例においては、メタ実装モデル1002でIfStatementクラスC101として表現されるC言語のIf文は、メタ汎化モデル1003でSelectionStatementクラスC204とSelectionItemクラスC205との組合せで表現される。メタ汎化モデル1003は、上述した物理要素の他に、ソースコードの性質、変換の目的、及び制約条件などに応じて、変換ルールによって対応付けられる要素を変更可能とする論理要素を含む。論理要素は、本実施例においては、図10における、LogicalElementクラスC202を推移的に継承する要素として表現される。LogicalElementクラスC202は、AttiributeクラスC206の集合を所有する。AttributeクラスC206は、クラス及びメソッドなどに対して属性情報を付加する機能を備える。これによって、ある変換ルールは、ある物理要素を論理要素に変換することによって、変換後の論理要素に追加の属性情報を付加できる。また、付加された属性情報は異なる変換ルールによっても利用可能となる。また、LogicalElementクラスC202は、任意の物理要素を参照できるRelatedElementクラスC207の集合を所有する。これによって、変換ルールは、任意の要素に対する関連を、その関連の名前とともに論理要素に付加することができ、また、他の変換ルールは、その関連を利用することが可能となる。また、論理要素は、例えば、StatementクラスC203に対するLogicalStatementクラスC208のように、各物理要素に対して定義される。このため、変換ルールが、任意の物理要素を、当該物理要素に対して情報又は関連を付加した論理要素へ変換することが可能となる。また、すべての論理要素は、何らかの物理要素を継承していることから、ある変換ルールにおいて、ある物理要素が論理要素へ変換された後、異なる変換ルールにおいて、それが論理要素であることを意識せず、物理要素として扱うことも可能である。論理要素を利用する変換ルールには、例えば、下記1~3のような方法があり得る。1あるパターンに一致する汎化モデルの物理要素を、ある構造を有する論理要素又は、論理要素と物理要素との組み合わせへ変換する。2あるパターンに一致する論理要素又は、論理要素と物理要素との組み合わせを、異なる構造を有する論理要素又は、論理要素と物理要素との組み合わせへ変換する。3あるパターンに一致する論理要素又は、論理要素と物理要素との組み合わせを、物理要素へ変換する。汎化モデル1206上で、論理要素を物理要素へ完全に変換してから、汎化モデル1206を検査モデル1008へ変換してもよい。汎化モデル1206の論理要素を検査モデル1008の要素へ変換可能な変換ルールを用い、論理要素を含む汎化モデル1206を直接検査モデル1008へ変換してもよい。また、本実施例の後述する第1の変換例~第5の変換例における論理要素は、乱数生成方法及び非決定的な値を選択する方法を表現したが、これに限らず、プログラミング言語の文法が直接表現可能な範囲を超える任意の要素を表現してもよい。論理要素によって表現される概念の例としては、例えば、ハードウェア操作など外部環境とのやり取りの抽象化、並びに、データ構造及びモジュールの抽象化などが挙げられる。また、各メタモデルは、図9~図11に示す限りではなく、変換対象となるプログラムを表現可能な任意の形式でよい。また、汎化モデル1206における論理要素に関しても、この限りではなく、変換ルールの記述に必要な、論理要素の種類を示す要素、論理要素、及び、他の要素物理要素又は論理要素との関連を示す要素、を表現可能な任意の記法でよい。また、論理要素は、特定の頻出する要素に関して、予め構造を定義してもよい。このような論理要素の定義の一例としては、最大値と最小値とを属性として有し、乱数生成を示す論理要素を、LogicalElementクラスC202を推移的に継承する新たなクラスの定義などがあり得る。乱数生成を示す論理要素は図16で詳細を説明する。以降、図9に示すメタ実装モデル1002、図10に示すメタ汎化モデル1003、及び図11に示すメタ検査モデル1004を用いた、ソースコード0001から検査コード0005への第1の変換例~第5の変換例を図12~図32に示す。ソースコード0001から検査コード0005への第1の変換例について図12~図17を用いて説明する。図12は、C言語のソースコード0001の一例の説明図である。図12に示すソースコード0001の行001では、ランダムな整数値を生成する関数randの戻り値を50で割った余りに1が加算されることによって、1から50までのランダムな値が生成される。行002では、行001で生成したランダムな値を引数として関数dosomethingが実行される。図13は、Promela言語による検査コード0005の一例の説明図である。図13に示す検査コード0005の行001では、整数型の変数valが定義される。行002では、1から50までの整数から変数valの値が選択される。行003では、行002で選択された変数valの値を引数として関数dosomethingが実行される。図14は、図12に示すソースコード0001の実装モデル1205の一例である。図14に示す実装モデル1205は、図9に示すメタ実装モデル1002による定義を用いて表現される。例えば、図12に示すソースコード0001の行001では、変数valがint型で宣言されているため、当該宣言は、図14に示す実装モデル1205では、属性nameとしてvalを有し、属性typeとしてintを有するVariableDeclaration要素O0101として表現される。また、図12に示すソースコード0001の行002における変数valの参照は、VariableDeclaration要素O0101とVariableReference要素O0102とが、declarationをラベルとして有するリンクL0101を介して接続されることによって、表現される。図14に示す実装モデル1205が、for文及びwhile文を繰り返しへ変換する図6に示す実装-汎化変換ルール1005図7に示す第1変換ルール1005-1によって汎化モデル1206へ変換された結果を図15に示す。図15は、図12に示すソースコード0001の抽象化された汎化モデル1206の説明図である。図12に示すソースコード0001はfor文及びwhile文を含まないので、当該変換は実行されず、図15に示す汎化モデル1206は、図14に示す実装モデル1205と実質的に同一である。次に、図15に示す汎化モデル1206が、乱数生成処理を抽象化して論理要素に変換する図6に示す抽象化変換ルール1006図7に示す第2変換ルール1006-1によって変換された汎化モデル1206を図16に示す。図16は、図15に示す汎化モデル1206の抽象化結果である。抽象化変換ルール1006による変換処理では、図15に示すBinaryOperation要素O0401、及び当該BinaryOperation要素O0401が推移的に所有する要素集合は、最小値1を示すAttribute要素O0702と最大値50を示すAttribute要素O0703とを所有する乱数生成式を意味する論理要素LogicalExpression要素O0701に変換される。図16に示す抽象化された汎化モデル1206が、図6に示す汎化-検査変換ルール1007図7に示す第3変換ルール1007-1によって検査モデル1008に変換された結果を図17に示す。図17は、図16に示す抽象化された汎化モデル1206から変換された検査モデル1008の説明図である。図16に示す論理要素であるLogicalExpression要素O0701と、最小値を表すAttribute要素O0702と、最大値を表すAttribute要素O0703と、の組合せは、Promela言語において非決定的な値の代入を行うselect文を表現するSelectStatement要素O0801と、最小値を意味するIntegerConstant要素O0802と、最大値を意味するIntegerConstant要素0O803と、の組合せに変換される。IntegerConstant要素O0802は、minをラベルとして有するリンクL0801を介してSelectStatement要素O0801に接続される。IntegerConstant要素O0803は、maxをラベルとして有するリンクL0802を介してSelectStatement要素O0801に接続される。最後に、図17に示す検査モデル1008からコードが生成されることによって、図13に示すPromela言語による検査コード0005が生成される。次に、図18に示すC言語のソースコード0001から図13に示すPromela言語による検査コード0005へ変換する第2の変換例、及び、図19に示すC言語のソースコード0001から図13に示すPromela言語による検査コード0005へ変換する第3の変換例について図18~図23を用いて説明する。図18及び図19はC言語のソースコード0001の一例の説明図である。図18及び図19に示すソースコード0001は、図12に示すソースコード0001と、ある関数dosomethingを、1から50の任意の値を引数として実行するプログラムである点で同じである。しかし、図12、図18及び図19に示すソースコード0001では、それぞれ、乱数を生成する方法が異なる。図18に示すソースコード0001では、現在時刻を返すシステム関数timeを、擬似的な乱数発生関数とし、当該乱数発生関数の戻り値を50で割った余りに1を加えることによって、1から50のランダムな値が生成される。図19に示すソースコード0001では、行101から行107にて独自に定義した乱数生成関数myrandの戻り値を50で割った余りに1を加えることによって、1から50のランダムな値が生成される。ここで、行101から行107で定義される乱数発生関数myrandは、自身が生成する乱数の範囲の最大値50と最小値1を、引数として受け取り、乱数発生関数myrandは、最大値から最小値を減算して1を加えた値を除算値とし、ランダムな整数値を生成する関数randの戻り値を除算値で割った余りに最小値を加えることによって、1から50のランダムな値を生成する。なお、乱数発生関数myrandが生成する乱数の範囲は行0001で定義される。図18及び図19に示すソースコード0001が示すプログラムは、それぞれ、図20及び図21に示す実装モデル1205で表現される。第1の変換例と同じ実装-汎化変換ルール1005によって、図20及び図21に示す実装モデル1205は、図22及び図23に示す汎化モデル1206に変換される。図22に示す汎化モデル1206は、抽象化変換ルール1006によって抽象化され、図16に示す汎化モデル1206に変換される。この抽象化に用いる抽象化変換ルール1006は、第1の変換例で用いた抽象化変換ルール1006を、関数timeを関数randと同じく乱数発生関数として扱うように変換したものである。つまり、この抽象化変換ルール1006によって、図22に示す汎化モデル1206のBinaryOperation要素O0501、及び当該BinaryOperation要素O0501が推移的に所有する要素集合は、図16に示す論理要素LogicalExpression要素O0701に変換される。同様に、図23に示す汎化モデル1206は、抽象化変換ルール1006によって抽象化され、図16に示す汎化モデル1206に変換される。この抽象化に用いる抽象化変換ルール1006は、第1の変換例で用いた抽象化変換ルール1006を、関数myrandを、第1引数を最小値、第2引数を最大値として、乱数を発生する関数として扱うように変更したものである。つまり、この抽象化変換ルール1006によって、図23に示す汎化モデル1206のFunctionCall要素O0601、及び当該FunctionCall要素O0601が推移的に所有する要素集合は、図16に示す論理要素LogicalExpression要素O0701に変換される。図16に示す汎化モデル1206は、第1の変換例で用いた汎化-検査変換ルール1007と同じ変換ルールによって、図17に示す検査モデル1207に変換され、最終的には図13にPromela言語による検査コード0005が出力される。第1の変換例~第3の変換例では、抽象化変換ルール1006を変更することによって、図12、図18及び図19に示す異なるソースコード0001から同一の図13に示す検査コード0005へ変換するものである。本実施例では、抽象化変換ルール1006を用いて汎化モデル1206を抽象化する処理で、所定の条件に適合する要素を論理要素に変換する。これによって、第2の変換例及び第3の変換例で説明したように、入力されたソースコード0001が変更されたとしても、管理者は、すべての変換ルール1005~1007を変更せずとも、抽象化変換ルール1006を変更するのみで、当該ソースコード0001が変更されて変更前と同じ検査コード0005を出力することができる。第4の変換例では、図12に示すソースコード0001から図13に示す検査コード0005と異なる図24に示す検査コード0005への変換例である。図24に示す検査コード0005について説明する。図13に示す検査コード0005では、行002に示すようにselect文を利用している。select文は、非特許文献1に開示された検査ツールであるSPINのバージョン6以降で追加された構文であり、検査ツールがバージョン5以前のSPINである場合、select文を利用できない。このため、検査ツールがバージョン5以前のSPINである場合、図24の行101から行116に示すように、非決定的な実行を表現する構文を検査コード0005に定義することによって、select文と等価な処理を表現する必要がある。本変換例において、図12に示すソースコード0001を図24に示す検査コード0005へ変換するためには、図12に示すソースコード0001を図14に示す実装モデル1205で表現し、続いて、図15で示される汎化モデル1206へ変換し、当該汎化モデル1206を抽象化して図16に示す汎化モデル1206に変換する点までは、第1の変換例と同じである。図16に示す汎化モデル1206を検査モデル1008に変換する汎化-検査変換ルール1007が第1の変換例と異なる。具体的には、第4の変換例の汎化-検査変換ルール1007では、図16に示す抽象化された汎化モデル1206のnameとしてrandomvaluegenarationを有するLogigalExpression要素O0701の変換先の要素が変更される。この汎化-検査変換ルール1007によって、図16に示す汎化モデル1206は図25に示す検査モデル1008に変換される。本変換例で用いる汎化-検査変換ルール1007では、図16に示す抽象化された汎化モデル1206のLogicalExpression要素O0701と、最小値を示すAttribute要素O0702と、最大値を表すAttribute要素O0703との組合せは、図25に示す検査モデル1008の要素O0901~0904の組合せに変換される。具体的には、図25に示す検査モデル1008のInlineFunctionCall要素O0905は、declarationのラベルを有するリンクL0901によって参照するInlineFunctionDeclaration要素O0901と、引数を示すargumentのラベルを有するリンクL0902によって参照するVariableReference要素O0902と、argumentのラベルを有するリンクL0903によって参照するIntegerConstant要素O0903と、argumentのラベルを有するリンクL0904によって参照するIntegerConstant要素O0904と、をこの順で所有する。なお、図25では、InlineFunctionDeclaration要素O0901の宣言内部は省略されているが、InlineFunctionDeclaration要素O0901は、第1引数に変数をとり、第2引数に最小値をとり、第3引数に最大値をとり、非決定的な選択を実現するプログラム構造を所有するように宣言される。VariableReference要素O0902は、値の代入先となる変数を定義する。IntegerConstant要素O0903は最小値となる。IntegerConstant要素O0904は最大値となる。なお、図25に示す検査モデル1008から図24に示す検査コード0005が取得できる。以上のように、抽象化変換ルール1006を用いて汎化モデル1206を抽象化する処理で、所定の条件に適合する要素を論理要素に変換する。これによって、出力する検査コード0005の変更を管理者が所望する場合であっても、すべての変換ルール1005~1007を変更する必要はなく、第1の変換例の汎化-検査変換ルール1007のみを変更することによって、所望の検査コードを出力できる。したがって、バージョン5以前のSPINである検査ツールを使用する場合には、第1の変換例の汎化-検査変換ルール1007のみを変更するだけで、バージョン5以前のSPINに対応させることができる第2の変換例で用いた変換ルールのうち汎化-検査変換ルール1007を第4の変換例で用いた汎化-検査変換ルール1007に変更すれば、図18に示すソースコード0001を図24に示す検査コード0005に変換することも可能である。また、同様に、第3の変換例で用いた変換ルールのうち汎化-検査変換ルール1007を第4の変換例で用いた汎化-検査変換ルール1007に変更すれば、図19に示すソースコード0001を図24に示す検査コード0005に変換することも可能である。次に、汎化モデル1206に対する抽象化処理が複数回実行され、ある論理要素から異なる論理要素へ変換される第5の変換例について図26~図32を用いて説明する。第5の変換例では、図26に示すC言語によるソースコード0001を図27に示すPromela言語による検査コード0005へ変換する。図26に示すソースコード0001では、乱数を生成するrand関数の戻り値を2で割った余りが0である場合にはdosomething1関数が実行され、余りが0以外である場合にはdosomething2関数が実行される。換言すれば、図26に示すソースコード0001は、dosomething1関数又はdosomething2関数がランダムに選択され、選択された関数が実行されるプログラムを示す。図26に示すソースコード0001は、図28に示す実装モデル1205によって表現される。また、図28に示す実装モデル1205は、実装-汎化変換ルール1005によって、図29に示す汎化モデル1206に変換される。次に、図29に示す汎化モデル1206は、第1の変換例と同じ抽象化変換ルール1006によって抽象化され、図30に示す汎化モデル1206に変換される。この変換において、図30に示す汎化モデル1206における、rand関数の呼出し及びrand関数の戻り値を2で割った余りの算出に対応する、図29に示すBinaryOperation要素O1101、FunctionCall要素O1102、FunctionDeclaration要素O1103、及びIntegerConstant要素1104の組合せは、図30に示す汎化モデル1206における、LogicalExpression要素O1201、Attribute要素O1202、及びAttribute要素O1203の組合せに変換される。さらに、図30に示す汎化モデル1206は、図30に示す汎化モデル1206への変換に用いた抽象化変換ルール1006と異なる抽象化変換ルール1006によって、図31に示す汎化モデル1206に変換される。この抽象化変換ルール1006は、条件式に用いられる変数に乱数値が代入される選択的実行文を非決定的な選択的実行文に変換するものである。上述した選択的実行文は、換言すれば、二つの選択肢のうち一つ選択肢がランダムに選択される選択的実行文を示す論理要素に変換される。具体的には、図30に示す汎化モデル1206のSelectionStatement要素O1204が図31に示す汎化モデル1206のLogicalSelectionStatement要素O1301に変換される。この理由について以下に説明する。図30に示す汎化モデル1206のVariableReference要素O1206は、name属性の値がrandomvaluegenerationであるLogicalExpression要素O1201が代入される変数を表す。また、当該VariableReference要素O1206は、リンクL1201を通じて推移的にSelectionItem要素O1205に接続され、当該SelectionItem要素O1205がSelectionStatement要素O1204に所有される。このため、SelectionStatement要素O1204は、条件式に用いられる変数に乱数値が代入される選択実行文に一致するので、非決定的な選択的実行文を表現する論理要素であるLogicalSelectionStatement要素O1301に変換される。また、図30に示す汎化モデル1206におけるSelectionItem要素O1205からconditionラベルを有するリンクL1201で推移的に接続される要素は、dosomething1関数又はdosomething2関数を選択するために、乱数を生成し、生成した乱数を2で割った余りが0であるか否かを判定する要素である。図31に示す汎化モデル1206では、非決定的な選択的実行文を表現するLogicalSelectionStatement要素O1301が定義されたため、図30に示す汎化モデル1206の上述した要素は不要となる。このため、これらの要素は削除される。以上によって、本変換例では、抽象化処理が複数回実行され、1回目の抽象化処理で変換された論理要素であるLogicalExpression要素O1201を含むSlectionStatement要素O1204は、2回目の抽象化処理で、論理要素であるLogicalSelectionStatement要素O1301に変換される。そして、図31に示す汎化モデル1206は、汎化-検査変換ルール1007によって、図32に示す検査モデル1008に変換され、図27に示す検査コード0005が出力される。以上のように、第5の変換例では、抽象化処理が複数回実行され、ある抽象化処理で変換された論理要素を他の抽象化処理でさらに論理要素に変換するので、より単純化された検査コードを出力でき、検査すべき状態数が膨大な分量となる状態爆発に至ることを防止できる。第5の変換例は、図26に示すソースコード0001と異なる乱数生成方法を用いるソースコード0001に変更した場合であっても、第1の変換例~第4の変換例と同じく、変更後の乱数生成方法に対応する変換ルールのみを変更すれば、他の変換ルールを変換しなくても、変更後のソースコード0001を所望の検査コード0005に変換できる。本実施例によれば、細粒度に分割された複数の変換ルールを入力するインタフェースを所有することによって、利用者による抽象化の水準の変更は、変換ルールを入力する操作により容易に実現される。すなわち、複数の細粒度の変換ルールを利用者が入力インタフェースにより選択できるため、図8A、図8Bに示したような抽象化の水準を、状況に応じて利用者が容易に選定、変更することが可能となる。ソースコード変換方法は、複数の変換ルールを用いて検査対象のソースコードをモデルチェッカの入力言語で記述された検査コードへ変換する手順を有し、前記変換ルールは、実装-汎化変換ルールと、抽象化変換ルールと、汎化-検査変換ルールと、に分類され、変換が段階的に行われる。これにより、検査対象のソースコードの設計変更に追従する際には、複数の変換ルールの中の変更に関連する変換ルールのみを変更すればよく、変更が最小限にとどめられる。加えて、実装モデルと、汎化モデルと、検査モデルとをそれぞれメタモデルで定義し、制約を加えることにより、変換ルールによる変換結果が不正でないことを検証可能となる。これにより、検査対象のソースコードを検査コードへ抽象化しながら変換する一連の処理を、細粒度の変換ルールを組み合わせることで実現することによって生じる、変換ルールの検証コストの増大を防ぐことが出来る。また、細粒度に分割された複数の変換ルールを入力するインタフェースを所有することによって、利用者による抽象化の水準の変更は、検査したい性質、検査水準に応じて、利用者が変換ルールを選択入力する操作で容易に実現される。これにより、抽象化の水準の変更が困難であるという課題が解決される。例えば、繰り返し実行時のみに発生する特定の不具合がある場合、その繰返しを除去することで、特定の不具合の検出はできなくなるものの、その繰返しを発生原因に含まない不具合の検出は可能であるままに、大幅に状態数を削減できる。さらに、モデルの変換ルールをデータベースに蓄積再利用することで、検査対象ソースコードの設計変更や、別ソフトウェアへの応用に、低コストで対応可能になる。なお、異なる検査ツールにて検査するために、検査ツールの形式で出力する際には、メタ検査モデルと、汎化-検査変換ルールのみを作成すればよく、作成部分が最小限に留められる。これによって、異なるモデルチェッカにて検査する際のコストを低減できる。また、汎化モデルを、検査モデルに変換するために用いる変換ルールにおいて、汎化モデルを直接検査モデルに変換する、又は、汎化モデル上にて物理要素間で変換を行う代わりに、いったん、汎化モデルにおいて論理要素への変換を行った上で、検査モデルへ変換することによって、変換ルールの共通化が可能となる。第2の実施例図33によって、本発明の第二の実施例のソースコード変換装置及び変換処理方法を説明する。この実施例においては、図33に示す検査コード出力ステップS104に続き、変換ルール入力ステップS102へ進むことで、既に入力されたソースコード0001を、繰り返し、異なる変換ルール集合0002を用いて、変換する手順をとってもよい。また、ある実施形態においては、検査コード出力ステップS104に続き、変換ルール入力ステップS102へ進み、既に入力された変換ルール集合0002の全てまたは一部と、新たに変換ルール入力ステップS102で入力された変換ルール集合0002をあわせて、変換ルール集合0002として用いてもよい。本実施例によれば、細粒度に分割された複数の変換ルールを入力するインタフェースを所有し、入力されたソースコードと、変換に用いた変換ルール集合を保存し、前記ソースコードを前記変換ルール集合の一部を入れ替えて変換できることによって、異なる抽象度の複数の検査コードを生成する場合などの、同一のソースコードを繰り返し変換する手間を削減できる。第3の実施例図34によって、本発明の第三の実施例のソースコード変換装置及び変換処理方法を説明する。本実施例では、ソースコードから検査コードを得る過程において生成される実装モデルと、汎化モデルと、検査モデルとを制約条件に基づいて検証するステップを有する。図34を用いて、変換の妥当性の検証手順を詳細に説明する。特定の変換ルールが、その変換に際して対象モデルについての前提条件をもつ場合、変換対象のモデルにおいて、前記特定の変換ルールの前提条件が、他の変換ルールの適用によって満たされなくなることがあり得る。このように前提条件が満たされないときに前記特定の変換ルールによってモデル変換を実施すると、変換結果のモデルが不正な状態になり得る。また、単に変換ルールに誤りが含まれるときも、変換結果のモデルが不正な状態になり得る。本実施例では、ソフトウェアのソースコード0001を入力するステップと、ソースコード情報1001を有する実装モデル1205を特定のプログラミング言語に依存しない形式である中間形式汎化モデル1206へ変換する第1変換ルールを入力するステップと、中間形式に対して抽象化処理を行う第2変換ルールを入力するステップと、中間形式から検査コードの情報をもつ検査モデル1008に変換する第3変換ルールを入力するステップと、ソフトウェアのソースコード0001を解析して実装モデル1205へ変換するステップと、前記第1変換ルールを用いてソフトウェアのソースコード0001を前記中間形式の汎化モデル1206へ変換するステップと、第2変換ルールを用いて、前記中間形式で表現されたソフトウェアを抽象化するステップと、第3変換ルールを用いて、前記中間形式を検査モデル1008に変換するステップと、検査モデル1008を用いて検証ツールの入力言語で記述された検査コード0005を生成するステップと、前記各段階のモデルを各々第1の制約条件0300、第2の制約条件0301、及び第3の制約条件0302に基づいて検証する充足性検証ステップと、を有する。前記各段階のモデルの、各々第1の制約条件0300、第2の制約条件0301、及び第3の制約条件0302に基づく充足性検証は、例えば、非特許文献2に開示されるMOFでメタモデルを記述することによって、又は非特許文献4に開示されるOCLによりメタモデルにより定義されるモデルに対する制約条件を記述することによって、実現される。本実施例によれば、メタモデル及び制約条件を用いることで、変換ルール同士の衝突や変換ルールの不具合による変換の妥当性を保証できる。このモデル変換では、メタモデルによって定義された形式のモデルが生成される。また、制約条件を追加し、生成されたモデルの妥当性を制約条件0300~00302で充足性検証することができる。以上、本発明者によりなされた発明を実施形態に基づき具体的に説明したが、本発明は上述した実施形態に限定されるものではなく、その要旨を逸脱しない範囲で種々変更可能であることは言うまでもない。