ソースコード変換装置によるソースコード変換方法であって、ソフトウェアのソースコードを入力するステップと、異なる複数の変換ルールを入力するステップと、処理性能に関係する制約である非機能ルールを入力するステップと、前記ソースコードを、前記異なる複数の変換ルール及び前記非機能ルールにより、検証ツールの入力言語で記述された非機能検査コードに変換するステップとを有することを特徴とするソースコード変換方法。請求項1において、前記異なる複数の変換ルールは、検査対象の前記ソースコードを前記非機能検査コードへと変換し抽象化する一連の処理を、細粒度に分割したものであり、前記非機能ルールは、時間的制約もしくは容量的な制約の少なくとも一方を含むことを特徴とするソースコード変換方法。請求項1において、前記変換ルールは、ソースコードを特定のプログラミング言語に依存しない形式である中間形式へと変換する第1変換ルールと、前記中間形式に対して抽象化処理を行う第2変換ルールと、前記中間形式から前記検査コードに変換する第3変換ルールとを含み、ソフトウェアのソースコードを入力するステップと、少なくとも1つの前記第1変換ルールを入力するステップと、少なくとも1つの前記第2変換ルールを入力するステップと、少なくとも1つの前記第3変換ルールを入力するステップと、前記第1変換ルールを用いて、前記ソフトウェアのソースコードを、前記中間形式へと変換するステップと、前記第2変換ルールを用いて、前記中間形式で表現された前記ソフトウェアを抽象化するステップと、前記中間形式に、前記非機能ルールにより、前記抽象化された中間形式に非機能制約を付加するステップと、前記第3変換ルールを用いて、前記非機能制約の付加された前記中間形式を検証ツールの入力言語で記述された非機能検査コードに変換するステップとを有することを特徴とする、ソースコード変換方法。請求項3において、前記非機能ルールは、前記中間形式の条件分岐に与える時間的制約を含むことを特徴とする、ソースコード変換方法。請求項3において、前記非機能ルールは、前記中間形式の繰り返しに与える時間的制約を含むことを特徴とする、ソースコード変換方法。請求項3において、前記非機能ルールは、前記中間形式のサブルーチンに与える時間的制約を含むことを特徴とする、ソースコード変換方法。請求項3において、前記非機能ルールは、前記中間形式の四則演算に与える時間的制約を含むことを特徴とする、ソースコード変換方法。請求項3において、前記非機能ルールは、前記中間形式の整理型に与える容量的な制約を含むことを特徴とする、ソースコード変換方法。請求項3において、前記非機能ルールは、前記中間形式のフロー型に与える容量的な制約を含むことを特徴とする、ソースコード変換方法。請求項3において、非機能検査コードがシステムの制約条件を満たすかの判定を行うステップと、非機能検査コードが前記システムの制約条件を満たさない場合に、前記ソースコードを修正して再入力するステップとを含む、ことを特徴とする、ソースコード変換方法。ソースコード変換装置によるソースコード変換方法であって、ソフトウェアのソースコードを入力するステップと、異なる複数の変換ルールを入力するステップと、異なる複数の逆変換ルールを入力するステップと、前記ソースコードを、前記異なる複数の変換ルールにより、中間形式に変換するステップと、前記中間形式を、前記異なる複数の変換ルールにより、抽象化中間形式に変換するステップと、前記抽象化中間形式に、観測ポイントを付加するステップと、前記観測ポイントが付加された抽象化中間形式を、前記異なる複数の逆変換ルールにより、観測ポイントが付加された中間形式に変換するステップと、前記観測ポイントが付加された中間形式を、前記異なる複数の逆変換ルールにより、観測ポイントが付加されたソースコードに変換するステップを有することを特徴とするソースコード変換方法。請求項11において、前記中間形式に対して検証要件を追加するステップを有することを特徴とする、ソースコード変換方法。請求項11において、処理性能に関係する制約である非機能ルールを入力するステップと、前記ソースコードを、前記異なる複数の変換ルール及び前記非機能ルールにより、検証ツールの入力言語で記述された非機能検査コードに変換するステップとを有することを特徴とする、ソースコード変換方法。請求項11において、前記異なる複数の変換ルールは、前記ソースコードを、該ソースコードの記述言語に依存しない汎化されたプログラム情報をもつ汎化モデルへ変換する実装-汎化変換ルールと、前記汎化モデルを抽象化する抽象化変換ルールと、前記汎化モデルを検証ツールの記述言語へと変換する汎化-検査変換ルールとを含むことを特徴とするソースコード変換方法。請求項14において、前記ソースコード情報を受け取り、実装モデルへと変換し、その変換過程をソースコード-実装モデル変換対応表として逆変換データベースに登録するステップと、前記実装モデルを前記汎化モデルへと変換し、その変換過程を実装-汎化モデル変換対応表として前記逆変換データベースに登録するステップと、前記汎化モデルの抽象化を行い、その変換過程を抽象化変換対応表として前記逆変換データベースに登録するステップと、前記汎化モデルの対応するモデル要素に非機能要件の付加を行い、出力するステップと、前記汎化モデルを、非機能検査モデルへと変換するステップとを含むことを特徴とするソースコード変換方法。請求項15において、前記抽象化変換対応表に従って、抽象化した前記汎化モデルの具体化を行うステップと、前記実装-汎化モデル変換対応表に従って前記汎化モデルを前記実装モデルへと逆変換するステップと、前記ソースコード-実装モデル変換対応表に従って前記実装モデルを計測付きソースコードへと変換し、出力するステップとを含むことを特徴とするソースコード変換方法。少なくとも1台のコンピュータ上で動作し、ソースコード変換装置を構成するプログラムであって、前記コンピュータを、ソフトウェアのソースコードを入力する手段、異なる複数の変換ルールを入力する手段、処理性能に関係する制約である非機能ルールを入力する手段、及び前記ソースコードを、前記異なる複数の変換ルール及び前記非機能ルールにより、検証ツールの入力言語で記述された非機能検査コードに変換する手段として機能させるためのソースコード変換プログラム。請求項17において、前記変換ルールは、前記ソースコードを特定のプログラミング言語に依存しない形式である中間形式へと変換する第1変換ルールと、前記中間形式に対して抽象化処理を行う第2変換ルールと、前記中間形式から前記検査コードに変換する第3変換ルールとを含み、前記コンピュータを、前記ソースコードを入力する手段と、少なくとも1つの前記第1変換ルールを入力する手段、少なくとも1つの前記第2変換ルールを入力する手段、少なくとも1つの前記第3変換ルールを入力する手段、前記第1変換ルールを用いて、前記ソフトウェアのソースコードを、前記中間形式へと変換する手段、前記第2変換ルールを用いて、前記中間形式で表現された前記ソフトウェアを抽象化する手段、前記中間形式に、前記非機能ルールにより、前記抽象化された中間形式に非機能制約を付加する手段、及び前記第3変換ルールを用いて、前記非機能制約の付加された前記中間形式を前記検証ツールの入力言語で記述された非機能検査検証用コードに変換する手段として機能させるためのソースコード変換プログラム。請求項18において、前記コンピュータを、前記抽象化中間形式に、観測ポイントを付加する手段、前記観測ポイントが付加された抽象化中間形式を、前記異なる複数の逆変換ルールにより、観測ポイントが付加された前記中間形式に変換する手段、前記観測ポイントが付加された中間形式を、前記異なる複数の逆変換ルールにより、観測ポイントが付加された前記ソースコードに変換する手段として機能させるためのソースコード変換プログラム。請求項18において、前記コンピュータを、前記中間形式に対して検証要件を追加する手段として機能させるためのソースコード変換プログラム。モデル検査によるソフトウェアの信頼性確保を有効に実施するためには、ソースコードからモデルチェッカの入力言語で記述された検査用コードを自動生成するなどの方法により、検査用コードを得るための労力を低減させること、および、ソフトウェアの仕様および設計を、モデルチェッカによる網羅的検査が現実的な時間計算量および空間計算量で終了するように抽象化することが必要となる。また処理性能に関しては、実際にはキャッシュやバスの利用状況/外部機構の物理的制約等の要因から少なからず設計値から外れてしまうため、選択した抽象レベルに従って実測データを測定し、検証結果の妥当性を確認する必要がある。しかし、特許文献1に開示される方法によると、1抽象化の水準の変更が困難である、2ソフトウェア設計変更への追従コストが高い、3異なるモデルチェッカにて検査する際のコストが高い、4利用者によって選択された抽象化水準で処理時間を測定する際のコストが高い、という課題が存在する。上記1の課題に関して、特許文献1に開示される方法によると、翻訳マップの変更は、ソースコードの改訂など、新しいタイプの命令がソースコード内に導入された場合のみに限定される。そのため、利用者が抽象化の水準を変更する方法は、変換前の検査対象のソースコードに修正を加える方法と、変換後の特定モデルチェッカの入力言語で書かれた検査コードに修正を加える方法と、環境モデルに修正を加える方法とに限定され、いずれの方法においても、利用者が大きな手間を費やすことになる。上記2の課題に関して、特許文献1に開示される方法によると、使用するライブラリの変更などの変更が生じた際には、翻訳マップの修正と、環境モデルの修正とを行う必要がある。しかし、翻訳マップは、前記ソースコードから、前記検査コードへと直接変換するマップ要素で構成されていることと、環境モデルが特定モデルチェッカの入力言語で書かれていることとに起因して、設計変更に追従するように整合性を保ちながら修正することは困難である。上記3の課題に関して、特許文献1に開示される方法によると、異なるモデルチェッカにて検査するためには、翻訳マップの修正と、環境モデルの修正とを行う必要がある。しかし、翻訳マップは、前記ソースコードから前記検査コードへと直接変換するマップ要素で構成されていることや、環境モデルが特定モデルチェッカの入力言語で書かれていることとに起因して、翻訳マップと環境モデルのすべてを修正する必要があり、大きなコストを要する。上記4課題に関して、特許文献2に開示される方法によると、利用者が選択した抽象度に従って観測用のコードを挿入することは出来ず、別途手動でソースコードに挿入する必要があり、大きなコストを要する。また、利用者は機能要件の検査しか実施できない為、非機能要件の検証を行うためには利用者が検査したい水準で検査コードを手動で作成する必要があり、コストが高く、再利用性も低い、等の課題が存在する。また、検査水準と状態数のトレードオフを、利用者側で管理したいというニーズがある。すなわち、複雑なシステムの検査では、状態爆発が容易に発生し、検査を完了することができない。このようなとき、何も検査できないよりも、水準を若干落としてでも、検査を完了できることが望ましい場合がある。例えば、繰り返し実行時のみに発生する特定の不具合がある場合、その繰返しを除去することで、特定の不具合の検出はできなくなるものの、大幅に状態数を削減できる、という場合もある。また、図15に示したモデル検査技術を利用した自動的網羅的な性能検証技術では、理論値が実測値からかけ離れる場合が多くなる。すなわち、実装方法による影響度が大きいため、理論値と実測値との乖離が大きくなり易い。そのため、実測値を計測する手段が必要となる。本発明の目的は、従来の技術の課題を踏まえ、利用者が検査したい水準で非機能要件の検証を行う検査コードを容易に生成可能とし、コスト低減及び再利用性の向上を実現するソースコード変換方法およびソースコード変換プログラムを提供することにある。本発明の他の目的は、抽象化の水準等に柔軟に対応でき、抽象化水準に従った測定観測用のコードをソースコードに挿入でき、理論値と実測値との乖離を測定し、検査水準と状態数のトレードオフを容易にするソースコード変換方法およびソースコード変換プログラムを提供することにある。本発明の代表的なものを示せば、次の通りである。本発明のソースコード変換装置によるソースコード変換方法は、ソースコード変換装置によるソースコード変換方法であって、ソフトウェアのソースコードを入力するステップと、異なる複数の変換ルールを入力するステップと、処理性能に関係する制約である非機能ルールを入力するステップと、前記ソースコードを、前記異なる複数の変換ルール及び前記非機能ルールにより、検証ツールの入力言語で記述された非機能検査コードに変換するステップとを有することを特徴とする。本発明によれば、細粒度に分割された複数の変換ルールや非機能ルールを入力するインタフェースを所有する。そのため、利用者による抽象化の水準の変更や、非機能要件の検証が、検査対象のソースコードに対応した、異なる複数の変換ルールを選択して入力する操作により、容易に実現される。これにより、複雑で大規模なソフトウェアであっても、入力したソースコードの機能要件と非機能要件の検証を利用者が選択した水準で容易に行うことが出来、検査用コード等のソフトウェア開発コストを大幅に低減することができる。本発明では、ソフトウェアの非機能すなわち処理性能を検証できるようにするために、異なる複数の変換ルールを用いて、検査対象のソースコードをモデルチェッカの入力言語で記述された非機能付きの検査コードへと変換する。前記異なる複数の変換ルールは、検査対象のソースコードをモデルチェッカの入力言語で記述された非機能付きの検査コードへと変換し、抽象化する一連の処理を細粒度に分割したものであり、複数の変換ルールを組み合わせて用いることにより、前記ソースコードから前記非機能付きの検査コードへの変換が実現される。本発明において、検査対象のソースコードを非機能付きの検査コードへと変換する一連の処理を、抽象化の処理も含めて、細粒度に分割し、分割されたそれぞれの処理を、変換ルールと呼ぶ。また、非機能付きの検査コードとは、検査コードが、細粒度に分割されたそれぞれの処理に関して、非機能要件と機能要件の検証を可能にする非機能の制約が付加された検査コード以下、単に非機能検査コードを意味する。そして、非機能ルールは、非機能処理性能に関係する制約を検査コードにするための変換ルールを定義したものである。本発明により実現されるソースコード変換装置は、ソースコードを検査コードへ変換する時、異なる複数の変換ルールや非機能ルールが、利用者によって、選択され、入力されるためのインタフェースを所有する。前記変換ルールや非機能ルールは、事前にソースコード変換装置内部に蓄積された複数の変換ルールや非機能ルールの中からの選択と、利用者の記述と、のいずれかの手段により入力される。また、本発明において、変換ルールは、ソースコードを、前記ソースコードの記述言語に依存しない、汎化されたプログラム情報をもつ形式汎化モデルへと変換する実装-汎化変換ルールと、汎化モデルを抽象化する抽象化変換ルールと、汎化モデルをモデルチェッカの記述言語へと変換する汎化-検査変換ルールに分類される。換言すると、異なる複数の変換ルールは、ソースコードを特定のプログラミング言語に依存しない形式である中間形式へと変換する第1変換ルールと、前記中間形式に対して抽象化処理を行う第2変換ルールと、前記中間形式から前記非機能検査コードに変換する第3変換ルールとに分類される。ソースコードから非機能検査コードへの変換は、ソースコードを、実装-汎化変換ルールにより、汎化モデルへと変換するステップと、前記汎化モデルを、抽象化変換ルールにより抽象化するステップと、この抽象化された前記汎化モデルに非機能の制約を付加するステップと、この汎化モデルを、汎化-検査変換ルールにより、非機能検査コードへと変換するステップと、の4つのステップを続けて行うことで実現される。換言すると、ソースコードから検査コードへの変換は、前記第1、第2、第3の変換ルールを各々1つ以上入力するステップと、前記第1変換ルールを用いて、ソフトウェアのソースコードを、前記中間形式へと変換するステップと、前記第2変換ルールを用いて、前記中間形式で表現されたソフトウェアを抽象化するステップと、非機能ルールを用いて前記中間形式に非機能の制約を付加するステップと、前記第3変換ルールを用いて前記中間形式を検証ツールの入力言語で記述された検証用コードに変換するステップの4つのステップを続けて行うことで実現される。また、本発明において、検査対象のソースコードを、検査コードへと変換する一連の処理にて、内部的に保持される情報モデルは、その形式をメタモデルにより定義される。前記モデルは、検査対象のソースコードに対応する情報をもつ実装モデルと、前述の汎化モデルと、モデルチェッカの記述言語に対応する情報をもつ検査モデルと、に分類される。実装モデルは、そのメタモデルであるメタ実装モデルにより定義され、汎化モデルは、そのメタモデルであるメタ汎化モデルにより定義され、検査モデルは、そのメタモデルであるメタ検査モデルにより定義される。前述のそれぞれのメタモデルは、データ構造の定義と、データに含まれる要素間の制約に関する情報とを保有する。また、本発明の他の実施形態によれば、前記中間形式を、前記異なる複数の変換ルールにより、抽象化中間形式に変換し、さらに非機能検査コードに変換するステップと、前記抽象化中間形式に、観測ポイントを付加するステップと、前記観測ポイントが付加された抽象化中間形式を、前記異なる複数の逆変換ルールにより、観測ポイントが付加された中間形式に変換するステップと、前記観測ポイントが付加された中間形式を、前記異なる複数の逆変換ルールにより、観測ポイントが付加されたソースコードに変換するステップを有する。以下、図面を参照して本発明の実施形態について詳しく説明する。まず、図1、図2を参照しながら本発明の基本概念を説明する。本発明では、ソースコードを、複数の変換ルールの組み合わせた変換処理を行うことにより、既存モデル検査装置に適合した非機能検査コードへ変換する。すなわち、a変換を細粒度に分割し、複数の変換ルールの組み合わせとしてパッケージ化することで、柔軟な変換を実現する。b利用者検査者は、検査対象のソースコード0001を入力し、対象のソースコードと検査水準に応じた変換ルール0002を選択し、変換処理1000により中間形式で表現されたソフトウェアを抽象化し、この抽象化されたソフトウェアの各部品機能に非機能ルール0005に基づいた非機能の制約を付加することで、所望の非機能検査コード0006を得る。非機能検査コード0006に対しては、さらに、モデル検査ツール2000においてシステムの制約条件を満たすかの判定がなされる。制約条件を満たさない場合は、ソースコードを修正して変換処理1000を繰り返す。このようにしてシステムの制約条件を満たす非機能検査コード0006が生成される。本発明における、変換ルールの例を挙げると次の通りである。a単純な構文変換C言語の条件分岐If文Switch文を、検査コードの条件分岐If文に変換C言語の繰り返し文for文while文...を、検査コードの繰り返しDo文に変換b外部環境のモデル化データ読込みを、ランダム入力へ置き換えc抽象化繰り返しの除去条件の簡略化また、本発明における、非機能ルールには、時間的制約や、容量的な制約がある。すなわち、本発明における、非機能要件には、処理時間、メモリ使用量、又はその両方を含む。図2により、本発明のソースコード変換処理における変換ルールの入力インタフェースについて、説明を補足する。本発明によれば、細粒度に分割された複数の変換ルール0002を入力するインタフェースを所有することによって、利用者による抽象化の水準の変更は、複数の異なる変換ルールを選択入力する操作により容易に実現される。すなわち、利用者による抽象化の水準の変更は、ドメイン情報や、検査したい性質、検査水準の情報抽象化による性質への影響に応じて、利用者が複数の異なる変換ルールを選択して呼び出し、ソースコード変換処理装置1000へ入力する操作により容易に実現される。本発明は、特に、システムソフトウェアの機能要求と非機能処理性能要求の検証に有効な技術である。すなわち、非機能ルール0005を入力するインタフェースを所有することによって、利用者による抽象化されたソフトウェアの各部品機能に対する非機能の制約を付加した所望の非機能検査コード0006の生成が可能になり、非機能要件の検証が容易となる。また、非機能検査コード0006は、細粒度に分割された状態の中間形式に変換ルールや非機能ルールが適用されて、生成される。この非機能検査コード0006が、システム全体としての制約条件を満たすかを判定する必要があり、これをモデル検査ツール2000に入力し、その結果を判定する機能3000を有している。本発明によれば、ソースコードを利用者が選択した水準で検査コードに変換した後、非機能要件を追加する手段を提供することで、利用者の指定した水準の非機能検査を可能にする。また、本発明によれば、利用者が選択した抽象化の水準に合わせた実測データの観測が可能となり、理論値と実測値との乖離を観測でき、検査水準と状態数のトレードオフを容易に解消することができる。次に、本発明の第一の実施例になるソースコード変換装置および変換処理方法を、図3ないし図11Bを参照しながら説明する。図3は、第一の実施例になるソースコード変換装置を含むソースコード変換システムの構成例を示す図である。本発明の実施形態に適用されるソースコード変換装置1000は、検査対象のソースコードを非機能検査コード0006に変換する装置であり、入力部1100と、変換処理部1200と、出力部1300と、記憶部1400と、制御部1500、とを有する。2000はモデル検査ツール、3000は検査結果の判定機能を示す。記憶部1400には、変換ルール0002、メタモデル0003、書出しルール0004、及び、非機能ルール0005が保持される。また、モデル検査ツー2000に対してはシステム制約条件0009が与えられる。図4に、ソースコード変換装置1000の構成例を示す。入力部1100は、ソースコード入力部1101と、変換ルール入力部1102と、非機能ルール入力部1103とを有する。変換処理部1200は、モデル構築部1201、実装-汎化モデル変換部1202、抽象化モデル変換部1203、非機能制約付加処理部1204、及び、汎化-検査モデル変換部1209を備えている。出力部1300は、非機能検査コード書出力部1301を有する。記憶部1400は、変換ルールデータベース1401、メタモデルデータベース1402、および、書出しルールデータベース1403、及び、非機能ルールデータベース1404を有する。ソースコード変換装置1000は、例えば、1台のコンピュータ、あるいはネットワークを介して接続された複数のコンピュータ上で動作するプログラムとして実施される。ソースコード0001と、変換ルール集合0002と、非機能ルール0005は、例えば、コンピュータ上の記憶装置から読込む方法と、コンピュータに接続された入力デバイスにより直接入力される方法等の方法により入力される。また、非機能検査コード0006は、例えば、コンピュータの記憶装置に書き出す方法と、コンピュータのディスプレイ装置に表示する方法等により出力される。入力部1100は、ユーザによって入力されるデータを受付け、入力されたデータを変換処理部1200へと供給する処理を行う。入力部1100は、ソースコード0001に関する情報を入力し、修正するソースコード入力修正部1101と、細粒度に分割された複数の変換ルーすなわち変換ルール集合0002に関する情報を入力する変換ルール入力部1102と、非機能ルール0005を入力する非機能ルール入力部1103とを備え、受付けた各入力を変換処理部1200へ供給する。ある実施形態においては、入力部1100は、ユーザによる、変換処理部の駆動や制御、出力部の駆動や制御、に関する指示を受け付けてもよい。変換処理部1200は、入力部より、ソースコード0001の情報と、ソースコード0001に適用すべき変換ルール集合0002の情報と、非機能ルール0005とを供給され、ソースコード0001を、変換ルール集合0002により変換し、非機能を付加する処理を行い、変換結果の情報を、出力部1300に供給する。ある実施形態においては、入力部より供給される変換ルール集合0002に関する情報は、記憶部に格納された変換ルールを指し示す識別情報のみが含まれていて、変換ルール集合0002の実体を、前記識別情報を用いて記憶部1400より取り出し、変換に用いてもよい。変換処理部1200は、モデル構築部1201と、実装-汎化モデル変換部1202と、抽象化モデル変換部1203と、非機能制約付加処理部1204と、汎化-検査モデル変換部1209とを有する。本実施形態において、変換処理部1200は、図6に示したように、メタモデルと、変換ルールを用いたモデル変換により、ソースコード情報1001を、検査モデル1008へと変換する。メタ実装モデル1002と、メタ汎化モデル1003と、メタ検査モデル1004と、は、例えば、非特許文献2に記載のMOFにて記述する。また、例えば、非特許文献3に記載されているQVTにて、実装-汎化変換ルール1005と、抽象化変換ルール1006と、汎化-検査変換ルール1007とを記述し、モデルの変換を行う。前記変換は、既に例示した方法の他のモデル変換方法でも良く、また、複数の方法を混在させてもよい。また、ある実施例においては、実装-汎化モデル変換部1202と、抽象化モデル変換部1203と、非機能制約付加処理部1204と、汎化-検査モデル変換部1209とをそれぞれ独立させず、同一の部位により行われても良く、さらに、実装モデル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へと、変換する。汎化モデルは、複数のプログラミング言語における構造や処理を表現可能なデータ構造をもつ。例えば、汎化モデル中では、ソースコード0001におけるIf文とSwitch文とを区別せず、選択的実行文として表現する。ある実施形態においては、実装モデル1205を、汎化モデル1206へと変換する際、実装-汎化変換ルール1005のみを用いることもあり得る。また、ある実施形態において、実装-汎化変換ルール1005が、複数の変換ルールを含む場合には、複数の変換ルールを統合して1つの変換ルールとし、実装モデル1205から汎化モデル1206への変換に利用する方法があり得る。また、ある実施形態において、実装-汎化変換ルール1005が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、実装モデル1205から汎化モデル1206への変換を行う手順があり得る。抽象化モデル変換部1203は、抽象化変換ルール1006と、メタ汎化モデル1003とを用いて、汎化モデル1206の抽象化を行う。抽象化の例としては、選択文における条件式を、恒真、もしくは恒偽、もしくは非決定的な選択で置き換える方法があり得る。ある実施形態においては、汎化モデル1206を抽象化する際、抽象化変換ルール1006のみを用いることもあり得る。また、ある実施形態において、抽象化変換ルール1006が、複数の変換ルールを含む場合には、複数の変換ルールを統合して1つの変換ルールとし、汎化モデル1206の抽象化に用いる方法があり得る。また、ある実施形態において、抽象化変換ルール1006が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、汎化モデル1206の変換を行う手順があり得る。非機能制約付加処理部1204は、抽象化された汎化モデル1206の各部品機能に非機能ルール0005に基づいた非機能の制約を付加し、汎化モデル1207を生成する。汎化-検査モデル変換部1209は、汎化-検査変換ルール1007と、メタ汎化モデル1003と、メタ検査モデル1004とを用いて、非機能の制約が付加された汎化モデル1207を、検査モデル1008へと、変換する。例えば、検査コードがPromela形式である場合、汎化モデルにおいて選択的実行文として表現された要素は、検査モデルにおいてはIf文として表現される。ある実施形態においては、汎化モデル1206を、検査モデル1008へと変換する際、汎化-検査変換ルール1007のみを用いることもあり得る。また、ある実施形態において、汎化-検査変換ルール1007が、複数の変換ルールを含む場合には、複数の変換ルールを統合して1つの変換ルールとし、汎化モデル1206から検査モデル1008への変換に利用する方法があり得る。また、ある実施形態において、汎化-検査変換ルール1007が、複数の変換ルールを含む場合には、変換処理を複数回繰り返すことで、汎化モデル1206から検査モデル1008への変換を行う手順があり得る。出力部1300は、変換処理部1200より供給された、変換結果の情報を用いて、非機能検査コード0006を出力する。ある実施形態においては、検査コードの出力に際して、例えばモデルチェッカの記述言語の文法情報などの情報を記憶部から供給されてもよい。検査コード書出し部1301は、メタ検査モデル1004と、記憶部1400の書出しルールデータベース1403から取得した検査コード書出しルール1009とを用いて、検査モデル1008を非機能検査コード0006へと変換する。たとえば、非特許文献5に記載される方法にて、検査コード書出しルール1009を記述し、検査モデル1008から、非機能検査コード0006への変換を行う。ある実施例においては、これに限らず、検査モデル1008を、検査に利用するモデルチェッカの記述形式へと変換する任意の方法でもよい。非機能検査コード0006は、例えば、モデルチェッカとしてSPINを用いる場合には、SPINの入力言語である、Promelaにより記述される。記憶部1400において、変換ルールデータベース1401と、メタモデルデータベース1402と、書出しルールデータベース1403と、非機能ルールデータベース1404のそれぞれは、例えば、関係データベース、もしくは、階層型データベースなどの、コンピュータ上にて実現される任意のデータ格納方式で実現される。変換ルールデータベース1401と、メタモデルデータベース1402と、書出しルールデータベース1403と、非機能ルールデータベース1404とは互いに同一の方式で実現されている必要性は無く、互いに異なる方式で実現されていてもよい。また、検査ルールデータベース1401と、メタモデルデータベース1402と、書出しルールデータベース1403と、非機能ルールデータベース1404のそれぞれは、単一の方式で実現されている必要性は無く、例えば、保有すべき情報の一部を関係データベースに格納し、保有すべき情報の一部を、発明を実現するコンピュータプログラム中に組込むなど、それぞれ異なる方式の組み合わせで実現されていてもよい。記憶部1400は、入力部1100と、変換処理部1200と、出力部1300とが、それぞれの処理を行うのに必要な情報を供給する。例えば、記憶部1400は、変換ルールに関する情報と、メタモデルに関する情報と、モデルチェッカの記述言語の文法に関する情報とを格納する。変換ルールデータベース1401は、既に述べたとおり、変換ルールを、メタデータとともに保有する。前記メタデータは、変換ルールを選択するためのものであり、実装-汎化変換ルール1005と、抽象化変換ルール1006と、汎化-検査変換ルール1007の、それぞれ異なる情報を持つ方法があり得る。実装-汎化変換ルール1005のメタデータは、例えば、変換元ソースコードの記述言語の種類があり得る。抽象化変換ルール1006のメタデータは、例えば、抽象化を分かりやすく端的に表現した名前、簡単な説明、データの抽象化、処理の抽象化などの抽象化の種別、自然語もしくはアルファベットや数値で表現された抽象化による状態数削減効果、自然語もしくはアルファベットや数値で表現された抽象化による性質への影響、抽象化の適用できるソフトウェアのドメイン、があり得る。汎化-検査変換ルール1007のメタデータは、例えば、検査に使用するモデルチェッカを指し示す名前があり得る。以降、図5ないし図6を参照しながら入力部1100と、変換処理部1200と、出力部1300と、記憶部1400と、制御部1500の詳細に関し、説明する。まず、本実施例におけるソースコード変換手順の一例を、図5を参照しながら説明する。図5は、第一の実施例の処理フローの例を示す図である。本実施例におけるソースコード変換手順は、ソースコード入力ステップS101と、変換ルール入力ステップS102と、変換ルール適用ステップS103と、検査コード出力ステップS104と、システム制約条件の入力ステップS105と、判定のステップS106と、修正のステップS107とからなる。まず、ソースコード入力ステップ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の処理とが混在する順番で処理がすすんでもよい。例えば、ソースコード入力部1102がソースコード0001を受付け、続いて、変換ルール入力部が、変換ルール集合0002を受付け、続いて、ソースコード入力部1102が、ソースコード0001をソースコード情報1001へ変換する、手順があり得る。変換ルール入力部1102は、利用者から入力された変換ルール集合0002を受け付ける。利用者から変換ルール集合0002を受け付ける方法は、例えば、次に示す方法があり得る。1つめの変換ルール入力方法の例として、変換ルール入力部1102は、変換ルール集合0002の一部として、利用者が手作業で直接入力した変換ルールを受け取る。2つめの変換ルール入力方法の例として、変換ルール集合0002の少なくとも一部は、利用者が記述した変換ルール記述により入力しても良い。あるいはまた、入力部1100が、記憶部1400から変換ルールの一覧を取得し、それを利用者に一覧などの形式で提示し、前記一覧から利用者が選択すること、変換ルール集合0002の入力を受け付けてもよい。すなわち、利用者が、変換ルールの入力に前置して、変換ルールの検索条件を入力部1100の変換ルール入力部1102に入力記述し、続いて、変換ルール入力部1102が、前記検索条件に合致する変換ルールを、記憶部1400が有する変換ルールデータベース1401から取得し変換ルール一覧として前記利用者に提示する。続いて、前記利用者が、提示された前記変換ルール一覧に含まれる1つ以上の変換ルールを選択する。この利用者によって選択された1つ以上の変換ルールを、変換ルール入力部1102が、変換ルール集合0002の一部として受け付ける。3つめの変換ルール入力方法の例として、まず、利用者が、変換ルールの入力に前置して、変換ルールの検索条件を変換ルール入力部1102に入力し、続いて、変換ルール入力部1102が、前記検索条件に合致する変換ルールを、変換ルールデータベース1401から取得して、変換ルール集合の一部として受け付けても良い。4つめの変換ルール入力方法の例として、入力されたソースコード0001から、変換ルール入力部1102が、変換ルールの検索条件を抽出、生成し、さらに、前記検索条件に合致する変換ルールを、変換ルールデータベース1401から取得し、変換ルール集合の一部として受け付ける。また、5つめの変換ルール入力方法の例として、変換ルール入力部1102は、何からの方法で入力された変換ルールを加工することにより、変換ルールを受け付ける。前記加工方法の例としては、変換ルールデータベース1401には、ソースコード0001中の変数名などをパラメータ化した状態で変換ルールを保持しておき、例えば利用者の明示的な入力による方法などにより、ソースコード0001の情報にてパラメータを埋めたものを、変換ルール集合に含める方法があり得る。変換ルール入力ステップS102に続き、変換ルール適用ステップS103において、モデル構築部1201がソースコード情報1001を実装モデル1205へと変換し、続いて、実装-汎化モデル変換部1202が実装モデル1205を汎化モデル1206へと変換しS1031、続いて、抽象化モデル変換部1203が汎化モデル1206を抽象化するS1032。抽象化された汎化モデル1206の各部品機能に非機能ルール0005に基づいた非機能の制約を付加し、汎化モデル1207を生成しS1033、続いて、汎化-検査モデル変換部1209が汎化モデル1207を検査モデル1008へと変換するS1034。変換ルール入力ステップS102と、変換ルール適用ステップS103とは、必ずしもこの順番で処理が完了する必要性は無く、実装-汎化モデル変換部1202の処理までに実装-汎化変換ルール1005が入力され、かつ、抽象化モデル変換部1203の処理までに非機能ルール0005及び抽象化変換ルール1006が入力され、かつ、汎化-検査モデル変換部の処理までに汎化-検査変換ルール1007が入力されていればよい。変換ルール適用ステップS103に続き、検査コード出力ステップS104において、検査コード書出し部1301により、検査モデル1008が、非機能検査コード0006として書き出される。非機能検査コード0006の書出し先の指定は、必ずしも変換ルール適用ステップS103の後である必要性は無く、非機能検査コード0006の書出しよりも先であればよい。例えば非機能検査コード0006の書出し先の指定がソースコード入力ステップS101と平行して行われる手順があり得る。なお、検査コード出力ステップS104に続き、変換ルール入力ステップS102へと進むことで、既に入力されたソースコード0001を、繰り返し、異なる変換ルール集合0002を用いて、変換する手順をとってもよい。また、ある実施例においては、検査コード出力ステップS104に続き、変換ルール入力ステップS102へと進み、既に入力された変換ルール集合0002の全てまたは一部と、新たに変換ルール入力ステップS102で入力された変換ルール集合0002をあわせて、変換ルール集合0002として用いてもよい。非機能検査コード0006は、モデル検査ツー2000に入力される。このモデル検査ツー2000には、システム制約条件の入力ステップS105でシステム制約条件0009が与えられるステップS105の入力のタイミングはこれ以前でも良い。そして、ステップS106で、非機能検査コード0006がシステム制約条件0009を満たしているかの判定がなされる。非機能検査コード0006がシステム制約条件0009を満たしていない場合、ステップS107で、ソースコードに対してオペレータによる修正が加えられ、以下、システム制約条件0009を満たすまで、同様処理が繰り返される。次に、図6、図7を用いて、変換処理部4111を詳細に説明する。図6は、第一の実施例のソースコード変換装置の動作を説明する図である。図7は、第一の実施例のソースコード変換の手順をより詳細に説明する図である。本実施形態において、変換処理部4111は、メタモデルと、変換ルールを用いたモデル変換により、ソースコード情報1101を、非機能検査モデル1008へと変換する。まず、モデル構築部1201は、ソースコード入力部1001からソースコード情報1001を受け取り、実装モデル1205へと変換する。実装-汎化モデル変換部1202は、変換ルールデータベースから実装-汎化変換ルール1005を、メタモデルデータベース1からメタ実装モデル1002とメタ汎化モデル1003を取り出し、実装モデル1205を、汎化モデル1206へと、変換する。抽象化モデル変換部1203は、変換ルールデータベースから抽象化変換ルール1006を、メタモデルデータベースからメタ汎化モデル1003を取り出し、汎化モデル1206の抽象化を行う。非機能要件付加処理部1204は、非機能ルールデータベースから非機能要件1600を取り出し、汎化モデル1206の対応するモデル要素に非機能要件の付加を行い非機能要件付き汎化モデル1207の生成を行う。例えば、非機能要件はモデル要素と要件項目のテーブル形式として表現される。汎化-検査モデル変換部1209は、変換ルールデータベースから汎化-検査変換ルール1007を、メタモデルデータベースからメタ汎化モデル1003とメタ検査モデル1004を取り出し、非機能要件付き汎化モデル1207を、検査モデル1008へと、変換する。例えば、非機能要件が処理で、モデル検査ツールがUPPAALの場合では、検査コードを時間オートマトンの形式に変換する。検査コード出力部1301は、メタ検査モデル1004と、書出しルールデータベースから取得した検査コード書出しルールとを用いて、検査モデル1008を非機能検査コード0006へと変換する。例えば、モデル検査ツールとしてUPPAAL用いる場合には、モデルを直接入力することが可能であるため、変換処理することなく書き出せばよい。このように、本発明では、モデル変換技術を利用し、段階的に変換するために、次のような処理を行う。1ソースコード0001をこれとほぼ等価な実装モデル1205へと変換2実装モデルを特定のプログラミング言語に依存しない形式にて構造や論理などのプログラム情報を表現する汎化モデルへと変換すなわち、異なる複数の第1変換ルール1005-1~1005-nの少なくとも1つを用いて、実装モデル1205を特定のプログラミング言語に依存しない形式である中間形式の汎化モデル1206へと変換する。図7の例では、第1変換ルールとして、if文→条件分岐、switch文→条件分岐、while文→繰り返し、for文→繰り返し、int文→整理型、flow文→フロー型、double文→フロー型の少なくとも7つの異なる変換ルールが選択されている。3汎化モデル1206に非機能制約を付加する処理を実施すなわち、非機能ルールを用いて、中間形式の汎化モデル1206を非機能制約付の汎化モデル1207へと変換する。図7の例では、時間の制約単位:秒として、サブルーチン→t>60、繰り返し→t>50、条件分岐→t>30、四則演算→t>10の異なる非機能ルールが選択されている。また、容量の制約として、整理型→4バイト、フロー型→8バイトの異なる非機能ルールが選択されている。4非機能制約付の汎化モデル1207に対して、抽象化のための変換を実施すなわち、異なる複数の第2変換ルール1006-1~1006-nの少なくとも1つを用いて、前記中間形式の汎化モデルに対して抽象化処理を行う。図7の例では、第2変換ルールとして、データ読み込み→ランダム入力、データの抽象化の少なくとも2つの異なる変換ルールが選択されている。5汎化モデルを、非機能検査モデルに変換し、コード生成出力すなわち、異なる複数の第3変換ルール1007-1~1007-nの少なくとも1つを用いて、前記中間形式の汎化モデル1207から非機能検査コードの生成に要する情報を有する非機能検査モデル1008に変換する。図7の例では、第3変換ルールとして、第1変換ルールに対応した条件分岐→if文、繰り返し→do文の少なくとも2つの異なる変換ルールが選択されている。また、実装モデル、汎化モデル、検査モデルは、それぞれ構文を定義するメタモデルによりデータ構造と意味論が定義される。このように、実装モデルから汎化モデルへの変換に際しては、例えば、変換対象ソースコードの記述言語の文法が、繰り返し処理の記法としてfor文やwhile文を含むとき、使用者がfor文を繰り返しへ変換するルールと、while文を繰り返しへ変換するルールとを、既に述べた変換ルール入力方法を用いて、第1変換ルールとして選択する。汎化モデルの抽象化の変換に際しては、使用者が検査水準抽象化の度合いを決定し、決定した検査水準を達成する変換ルールとして、例えば、外部データ読込みに関する命令および一連の処理をランダムな入力へと変換するルールと、特定のデータ型をより抽象度の高い型へと変換するルールとを、既に述べた変換ルール入力方法を用いて、第2変換ルールとして選択する。さらに、汎化モデルから検査モデルへの変換に当たっては、例えば、モデルチェッカの入力言語の文法が、繰り返し処理の記法としてdo文をもつとき、使用者が繰り返しをdo文へ変換するルールを、既に述べた変換ルール入力方法を用いて、第3変換ルールとして選択する。変換ルールは、複数のソフトウェアにまたがって適用可能な汎用的なルールなど、繰り返し利用可能なものがデータベース化される。データベースに格納された変換ルールは、使用者による検索やルール選択の判断材料として用いられるメタ情報として、ドメイン情報や検査水準抽象化による検査への影響の情報を有する。また、変換ルールの選択方法としては、次のようなものがある。1汎用的なルール:常に選択2特定のライブラリに依存したルール:使用ライブラリや、検査対象のドメインカテゴリを入力することで、まとめて選択3抽象化に対応したルール:検査したい性質検査水準を入力して得た変換ルール一覧から、利用者が選択、もしくは利用者自身が記述して入力、もしくは検査したい性質などから、自動生成。本発明では、ソースコードから変換ルールに従って検査モデルを生成する際に、抽象化されたソフトウェアの各部品機能に、各々実行環境に対応した処理時間を記述することで、オートマトンに時間の概念を与えることができる。例えば、図8Aのオートマトンに示したように、抽象化されたソフトウェアの各部品機能、すなわち各状態A~Eに対して、各々実行環境に対応した制約として処理時間PCを記述することができる。これにより、利用者が、対象ソースコードと、検査水準抽象化の度合いに応じて、変換ルールや非機能ルールを選択することで、検査可能な非機能検査コードに変換することが可能となり、利用者の選択した抽象化の水準での非機能検証の課題が解決される。本発明によれば、図8Bに示したように、抽象度に対応した機能要求や非機能要求の検証が可能であり、また、変換ルールの変更のみで種々の実行環境に対応可能となる。すなわち、モデルの抽象化により、状態数を削減することができる。しかし、抽象化によりモデルの性質に影響を与えることがある。たとえば、検出された欠陥反例が、もとのシステムに存在しない、もとのシステムに存在する欠陥を発見できない、等である。一方で、性質に影響を与えない健全な抽象化は、状態数削減効果が小さい傾向がある。本発明によれば、細粒度に分割された複数の変換ルールを入力するインタフェースを所有することによって、利用者による抽象化の水準の変更や、非機能制約の付加は、変換ルールを入力する操作により容易に実現される。すなわち、複数の細粒度の変換ルールや非機能制約の付加を利用者が入力インタフェースにより選択できる。ソースコード変換法は、複数の変換ルールを用いて検査対象のソースコードをモデルチェッカの入力言語で記述された検査コードへと変換する手順を有し、前記変換ルールは、実装-汎化変換ルールと、抽象化変換ルールと、汎化-検査変換ルールと、に分類され、変換が段階的に行われる。これにより、検査対象のソースコードの設計変更に追従する際には、複数の変換ルールの中の変更に関連する変換ルールや非機能制約の付加のみを変更すればよく、変更が最小限にとどめられる。加えて、実装モデルと、汎化モデルと、検査モデルとをそれぞれメタモデルで定義し、制約を加えることにより、変換ルールによる変換結果が不正でないことを検証可能となる。これにより、検査対象のソースコードを検査コードへと抽象化しながら変換する一連の処理を、細粒度の変換ルール及び非機能ルールと組み合わせることで実現することによって生じる、変換ルール及び非機能ルールの検証コストの増大を防ぐことが出来る。また、細粒度に分割された複数の変換ルールを入力するインタフェースを所有することによって、利用者による抽象化の水準の変更は、検査したい性質、検査水準に応じて、利用者が変換ルール及び非機能ルールを選択入力する操作で容易に実現される。これにより、抽象化の水準の変更が困難で、あるという課題が解決され、モデル検査ツールの入力言語で検査コードを記述するコストを低減させることが可能となる。例えば、繰り返し実行時のみに発生する特定の不具合がある場合、その繰返しを除去することで、特定の不具合の検出はできなくなるものの、その繰返しを発生原因に含まない不具合の検出は可能であるままに、大幅に状態数を削減できる。さらに、モデルの変換ルール及び非機能ルールをデータベースに蓄積再利用することで、検査対象ソースコードの設計変更や、別ソフトウェアへの応用に、低コストで対応可能になる。本発明によるシステムソフトウェアの非機能検証の例として、システムの時間制約に関する検証の例を挙げると、次のようなものがある。1DTVのチャンネル切り替えが、1秒以内に切り替わること確認する。2超解像アルゴリズムが、1画面あたり1/120秒以内で終了することを確認する。3装置の異常をセンサにて検出した場合、5秒以内でユーザに通知することを確認する。次に、図9乃至図14を使って、本発明の第2の実施例になるソースコード変換装置および変換処理方法を説明する。本実施例では、抽象化変換後の中間形式に対して抽象化フラグを付加するステップを有することを特徴とする。すなわち、ソースコード変換装置によるソースコード変換方法であって、ソースコード変換装置に、ソフトウェアのソースコードと、異なる複数の変換ルールと、異なる複数の逆変換ルールとを入力し、ソースコードを、異なる複数の変換ルールにより、中間形式に変換し、さらに、中間形式を、異なる複数の変換ルールにより、抽象化中間形式に変換する。そして、抽象化中間形式に、観測ポイントを付加する。さらに、観測ポイントが付加された抽象化中間形式を、異なる複数の逆変換ルールにより、観測ポイントが付加された中間形式に変換し、この観測ポイントが付加された中間形式を、異なる複数の逆変換ルールにより、観測ポイントが付加されたソースコードに変換する。図9は、第2の実施例になるソースコード変換装置を含むソースコード変換システムの構成例を示す図である。本発明の実施形態に適用されるソースコード変換装置1000は、検査対象のソースコード0001を非機能検査コード0007に変換し、計測付きソースコード0008を出力する装置であり、入力部1110と、変換処理部1200と、出力部1300と、記憶部1400と、制御部1500とを有する。2000はモデル検査ツール、4000は実測装置を示す。図10は、ソースコード変換装置1000の構成例を示す図である。入力部1100は、ソースコード入力修正部1101と、変換ルール入力部1102と、非機能ルール入力部1103とを有する。変換処理部1200は、モデル構築部1201、実装-汎化モデル変換部1202、抽象化モデル変換部1203、非機能要件付加処理部1204、汎化-検査モデル変換部1209、具体化モデル変換部1210、汎化-実装モデル変換部1211、及び、コード生成部1212を備えている。出力部1300は、非機能検査コード出力部1301と計測付きソースコード出力部1302とを有する。記憶部1400は、変換ルールデータベース1401、メタモデルデータベース1402、書出しルールデータベース1403、非機能ルールデータベース1404、および、逆変換ルールデータベース1405を有する。ソースコード変換装置1000は、例えば、1台のコンピュータ、あるいはネットワークを介して接続された複数のコンピュータ上で動作するプログラムとして実施される。ソースコード0001と変換ルール集合0002とは、例えば、コンピュータ上の記憶装置から読込む方法と、コンピュータに接続された入力デバイスにより直接入力される方法等の方法により入力される。また、非機能検査コード0007と計測付きソースコード0008は、例えば、コンピュータ上の記憶装置に書出す方法と、コンピュータのディスプレイ装置に表示する方法により出力される。入力部1100は、ユーザによって入力されるデータであるソースコード0001に関する情報と、細粒度に分割された複数の変換ルール、すなわち変換ルール集合0002に関する情報とを受付け、変換処理部1202へ供給する。ある実施形態においては、入力部1100は、ユーザによる、変換処理部の駆動や制御、出力部の駆動や制御、に関する指示を受け付けてもよい。図11は、本発明の第二の実施例になるソースコード変換装置の処理フローの例を示す図である。変換処理部1200は、入力部1100からソースコード0001の情報と、ソースコード0001に適用すべき変換ルール集合0002の情報とを供給され図11のS101、S102、ソースコード0001を、変換ルール集合0002により変換する処理S1031~1034、S104~S107と逆変換処理S1035~S1038を行い、変換結果の情報と、ユーザの抽象化水準に会った計測処理が追加された計測付きソースコード0008を出力部1300に供給するS108。出力部13000は、変換処理部1200より供給された、変換結果の情報を用いて、非機能検査コード0007を出力する。以降、図12~図14を参照しながら変換処理部1200の構成、機能を詳細に説明する。まず、図12は、第二の実施例のソースコード変換装置の動作を説明する図である。図13は、ソースコード-実装モデル変換対応表Table-A~Cの構成例及び機能について説明する図である。本実施形態において、変換処理部1200は、メタモデルと、変換ルールを用いたモデル変換により、ソースコード情報0001を、非機能検査モデル1207へと変換し、計測付きソースコード0008を出力する。モデル構築部1201は、ソースコード入力修正部1201からソースコード情報を受け取り、実装モデル1205へと変換し、その変換過程をソースコード-実装モデル変換対応表Table-Aとして逆変換データベース1405に登録する。ソースコード-実装モデル変換対応表Table-Aには、例えば、if→if文、switch→switch文、while→while文のように記録される。実装-汎化モデル変換部1202は、変換ルールデータベース1401から実装-汎化変換ルールを、メタモデルデータベース1402からメタ実装モデルとメタ汎化モデルとを取り出し、実装モデルを汎化モデルへと変換し、その変換過程を実装-汎化モデル変換対応表Table-Bとして逆変換データベース1405に登録する。ソースコード-実装モデル変換対応表Table-Bには、例えば、位置10、繰り返し→while文Step10、位置20、繰り返し→while文Step15、位置30、繰り返し→for文Step30のように記録される。抽象化モデル変換部1203は、変換ルールデータベース1401から抽象化変換ルールを、メタモデルデータベース1402からメタ汎化モデルを取り出し、汎化モデルの抽象化を行い、その変換過程を抽象化変換対応表Table-Cとして逆変換データベース1405に登録する。ソースコード-実装モデル変換対応表Table-Cには、例えば、位置20、ランダム入力→位置50、データ読み込みのように記録される。非機能要件付加処理部1204は、非機能ルールデータベース1404から非機能要件を取り出し、汎化モデルの対応するモデル要素に非機能要件の付加を行い、汎化-検査モデル変換部1209と具体化モデル変換部1210に出力する。汎化-検査モデル変換部1209は、変換ルールデータベースから汎化-検査変換ルールを、メタモデルデータベースからメタ汎化モデルとメタ検査モデルを取り出し、汎化モデルを、検査モデルへと変換する。具体化モデル変換部1210は、逆変換ルールデータベース1405から抽象化変換対応表Table-Cを取得し、対応表に従って抽象化した汎化モデルの具体化を行う。汎化-実装モデル変換部1211は、逆変換ルールデータベース1405から実装-汎化モデル変換対応表Table-Bを取得し、対応表に従って汎化モデルを実装モデルへと逆変換する。コード生成部1212は、逆変換ルールデータベース1405からソースコード-実装モデル変換対応表Table-Aを取得し、対応表に従って実装モデルを計測付きソースコード0008へと変換し、ソースコード出力部1302へ出力する。検査コード出力部は、メタ検査モデルと、記憶部1400の書出しルールデータベース1403から取得した検査コード書出しルールとを用いて、検査モデルを非機能検査コード0007へと変換する。例えば、モデル検査ツールとしてUPPAAL用いる場合には、モデルを直接入力することが可能であるため、変換処理することなく書き出せばよい。ソースコード出力部では、入力された測定付きソースコードをシステム外部に出力する。例えば、外部記憶媒体へ保存したり、ディスプレイに表示したりする。次に、図14は、ソースコード変換の手順を説明する図である。本発明による、非機能ルール、例えば、時間変換ルールを用いた、自動生成技術によれば、1検証したい抽象度まで抽象プログラムモデルを変換し、2検査対象の抽象プログラムモデルに計測用のチェックを追加し、3逆変換ルールに従ってソースコードに変換、計測チェックされた箇所に計測用のコードを埋め込み、計測コード付きソースコードとする。さらに、4実環境を使って実行時間を計測し、時間変換ルールを生成する。5上記生成された時間変換ルールを用いて非機能検査用コード0007を生成する。なお、図12、図13で説明したように、時間変換ルールを付与してから計測コード付きソースコードを生成するようにしても良い。これにより、利用者による抽象化の水準の変更に応じた観測用プローブを実際のソフトウェアのソースコードに自動的に挿入が可能となり、利用者が選択した抽象化水準での非機能、例えば実行処理時間の観測が困難であるという課題が解決される。すなわち、本実施例によれば、利用者による抽象化の水準の変更は、検査対象のソースコードに対応した、異なる複数の変換ルールを選択して入力する操作により、自動的に実現される。そして、利用者が選択した抽象化の水準に合わせて、ソフトウェアの理論上の位置と実際の位置を1:1に対応付けた実測データの観測が可能となる。