ソフトウェアの検証を行うソフトウェア検証装置と、前記ソフトウェア検証装置が行った検証の結果を取得し、記憶する検証結果記憶手段を有するソフトウェア管理装置と、からなるソフトウェア管理システムであって、前記ソフトウェア検証装置は、プログラムの仕様をモデル記述言語で記述したアプリケーションモデルを取得するアプリケーションモデル取得手段と、前記プログラムを動作させるための基本ソフトもしくはハードウェアであるプラットフォームの仕様をモデル記述言語で記述したプラットフォームモデルを記憶するプラットフォームモデル記憶手段と、前記プラットフォームモデルと前記アプリケーションモデルとを用いて、前記アプリケーションモデルと前記プラットフォームモデルとの互換性を検証するモデル検証手段と、前記モデル検証手段による検証結果を前記ソフトウェア管理装置に出力する検証結果出力手段と、を有することを特徴とする、ソフトウェア管理システム。前記モデル検証手段は、前記プログラムがプラットフォームに対して行っているインタフェース呼び出しが、検証対象のプラットフォームモデルが有するインタフェース定義に対して適合するかを検証することを特徴とする、請求項1に記載のソフトウェア管理システム。前記ソフトウェア管理装置は、検証対象のプラットフォームに対応するプラットフォームモデルを記憶する第二のプラットフォームモデル記憶手段をさらに有し、前記ソフトウェア検証装置は、前記第二のプラットフォームモデル記憶手段からプラットフォームモデルを取得して、前記プラットフォームモデル記憶手段に格納することを特徴とする、請求項1または2に記載のソフトウェア管理システム。複数の前記ソフトウェア検証装置と、単一の前記ソフトウェア管理装置と、からなる、請求項1ないし3のいずれかに記載のソフトウェア管理システム。プログラムの仕様をモデル記述言語で記述したアプリケーションモデルを取得するアプリケーションモデル取得手段と、前記プログラムを動作させるための基本ソフトもしくはハードウェアであるプラットフォームの仕様をモデル記述言語で記述したプラットフォームモデルを記憶するプラットフォームモデル記憶手段と、前記プラットフォームモデルと前記アプリケーションモデルとを用いて、前記アプリケーションモデルと前記プラットフォームモデルとの互換性を検証するモデル検証手段と、前記モデル検証手段による検証結果を外部に出力する検証結果出力手段と、を有するソフトウェア検証装置。ソフトウェアの検証を行うソフトウェア検証装置と、前記ソフトウェア検証装置が行った検証の結果を取得し、記憶するソフトウェア管理装置と、が行うソフトウェア管理方法であって、ソフトウェア検証装置が、プログラムの仕様をモデル記述言語で記述したアプリケーションモデルと、前記プログラムを動作させるための基本ソフトもしくはハードウェアであるプラットフォームの仕様をモデル記述言語で記述したプラットフォームモデルと、を用いて、前記アプリケーションモデルと前記プラットフォームモデルとの互換性を検証し、検証を行った結果を前記ソフトウェア管理装置に出力するステップを含むことを特徴とする、ソフトウェア管理方法。特許文献1に記載の発明は、利用者が実際に使用したアプリケーションの不具合情報を収集するための発明であるため、公開前のアプリケーションに対する品質の判定には用いることができないという問題がある。また、管理される情報はエンドユーザが不具合であると判断したもののみであり、特定のルールに沿って検証されたものではないため、収集される情報に偏りが生じるおそれがある。特許文献2に記載の発明では上記の問題を解決することができるが、当該発明は会社など組織の内部で作成されるソフトウェアを想定した発明である。したがって、これをオープンプラットフォームなど、管理者と別の拠点で開発を行うシステムに適用した場合、開発者から管理者へソフトウェアの設計情報を送信しなければならないため、知的財産の保護が難しくなるという別の問題がある。このように、既存の技術では、オープンプラットフォームを利用し、開発者によって開発されたアプリケーションを配布業者が管理し配布する形態において、作成されたアプリケーションの品質情報を、ソフトウェアの設計情報を秘匿したままで管理することが難しいという問題があった。本発明は上記の問題点を考慮してなされたものであり、ソフトウェア開発者が作成したソフトウェアの品質に関する情報を、ソフトウェアの設計情報を秘匿したままで一元管理できるソフトウェア管理システムを提供することを目的とする。本発明に係るソフトウェア管理システム、ソフトウェア検証装置、およびソフトウェア管理方法では、上記課題を以下の手段により解決する。本発明に係るソフトウェア管理システムは、ソフトウェアの検証を行うソフトウェア検証装置と、前記ソフトウェア検証装置が行った検証の結果を取得し、記憶する検証結果記憶手段を有するソフトウェア管理装置と、からなるソフトウェア管理システムである。また、前記ソフトウェア検証装置は、プログラムの仕様をモデル記述言語で記述したアプリケーションモデルを取得するアプリケーションモデル取得手段と、前記プログラムを動作させるための基本ソフトもしくはハードウェアであるプラットフォームの仕様をモデル記述言語で記述したプラットフォームモデルを記憶するプラットフォームモデル記憶手段と、前記プラットフォームモデルと前記アプリケーションモデルとを用いて、前記アプリケーションモデルと前記プラットフォームモデルとの互換性を検証するモデル検証手段と、前記モデル検証手段による検証結果を外部に出力する検証結果出力手段と、を有することを特徴とする。モデルとは、仕様記述言語の一種であるモデル記述言語によってソフトウェアの仕様を表現したものである。アプリケーションモデルとは、作成対象のアプリケーションプログラムの仕様をモデル記述言語で表現したものであり、プラットフォームモデルとは、プログラムを動作させるための、ミドルウェアを含む基本ソフトOS、もしくはハードウェアの仕様をモデル記述言語で表現したものである。本発明は、これらのモデルを検証しながら開発プロセスを進めるという開発手法に適用することができる。本発明に係るソフトウェア検証装置は、アプリケーションのモデルと、当該アプリケーションが動作するプラットフォームのモデルを用いて、モデル間の情報の交換に互換性があるかをチェックし、その結果を外部に出力する。このように構成することにより、開発者によって検証されたアプリケーションの詳細な検証結果、すなわち品質情報を出力することができる。また、出力されるデータには、ソフトウェアの設計に関する情報は含まれないため、アプリケーション開発に係る機密を保持することができる。また、本発明に係るソフトウェア管理システムが有するソフトウェア管理装置は、前記検証結果を取得し記憶する検証結果取得手段を含む。ソフトウェア検証装置によって出力された検証結果をソフトウェア管理装置が取得し、記録することで、ソフトウェア開発者によって作成されたソフトウェアの品質を一元的に管理することができる。また、前記モデル検証手段は、前記プログラムがプラットフォームに対して行っているインタフェース呼び出しが、検証対象のプラットフォームが有するインタフェース定義に対して適合するかを検証してもよい。モデル間の情報交換に互換性があることの確認は、基本ソフトやハードウェアが有しているAPI等のインタフェースに対する呼び出しが、アプリケーション側から正しく行われているかをモデル検証手段が検証することによって行う。検証は、アプリケーションモデルから呼び出しているインタフェースがプラットフォームモデルに存在しているか、または、アプリケーションモデルで定義されているインタフェースの型がプラットフォームモデルと整合しているかを確認すること等によって行う。このように構成することにより、ある特定のプラットフォーム上でプログラムが正常に動作することを確認することができる。また、前記ソフトウェア管理装置は、検証対象のプラットフォームに対応するプラットフォームモデルを記憶する第二のプラットフォームモデル記憶手段をさらに有し、前記ソフトウェア検証装置は、前記第二のプラットフォームモデル記憶手段からプラットフォームモデルを取得して、前記プラットフォームモデル記憶手段に格納してもよい。このように構成することにより、ソフトウェア検証装置は、任意のプラットフォームモデルを検証の対象としてソフトウェア管理装置から取得し、検証を行うことができる。また、本発明に係るソフトウェア管理システムは、複数の前記ソフトウェア検証装置と、単一の前記ソフトウェア管理装置と、からなってもよい。このように構成することにより、複数のソフトウェア検証装置が生成した検証結果を一元的に管理することができる。複数の開発者が複数の拠点で開発を行う形態に適用することができるため、オープンプラットフォームを採用した製品に好適である。本発明によれば、ソフトウェア開発者が作成したソフトウェアの品質に関する情報を、ソフトウェアの設計情報を秘匿したままで一元管理できるソフトウェア管理システムを提供することができる。第一の実施形態本発明の第一の実施形態に係るソフトウェア検証装置は、検証機能と共に開発機能を有するソフトウェア作成装置として実装される。第一の実施形態に係るソフトウェア作成装置、およびソフトウェア管理装置について、図を用いて詳細な説明を行う。図1は、本実施形態におけるソフトウェア作成装置およびソフトウェア管理装置のシステム構成を表した図である。ソフトウェア作成装置100は、アプリケーションの開発に用いられるコンピュータであり、中央演算処理装置CPUおよび主記憶装置RAM、補助記憶装置記憶媒体等にて構成される。ソフトウェア作成装置100は、モデル作成部101、プラットフォームモデル記憶部102a、アプリケーションモデル記憶部102b、モデルチェック部103、検証結果出力部104、プログラム生成部105を含んでおり、補助記憶装置に記憶されたプログラムコードをCPUが読み出して実行することにより、前記各部の機能が実現される。また、ソフトウェア管理装置200は、アプリケーション配布業者以降、アプリケーションプロバイダと称するが有しており、アプリケーションの管理に用いられるコンピュータである。ソフトウェア管理装置200は、検証結果入力部201、検証結果記憶部202、品質情報検索部203、アプリケーションプログラム記憶部204、プラットフォームモデル管理部205から構成される。まず、ソフトウェア作成装置100について説明を行う。モデル作成部101は、開発対象となるアプリケーションをモデルで表したアプリケーションモデルを作成するための手段である。アプリケーションモデルとは、アプリケーションを、AADLTheSAEArchitectureAnalysisandDesignLanguageなどのモデル記述言語によって表したものである。なお、本実施形態においては、アプリケーションモデルをソフトウェア検証装置上で作成するので、モデル作成部101が、本発明におけるアプリケーションモデル取得手段となる。プラットフォームモデル記憶部102aは、開発対象のアプリケーションが動作するプラットフォームのモデルを格納する手段であり、本発明におけるプラットフォームモデル記憶手段である。プラットフォームモデルとは、アプリケーションが動作するOS、ミドルウェア、ないしは仮想化されたハードウェアを、アプリケーションモデルと同様にモデル記述言語によって表したものである。アプリケーションモデル記憶部102bは、モデル作成部101で作成されたアプリケーションモデルを記憶する手段である。モデルチェック部103は、プラットフォームモデル記憶部102aに記憶されたプラットフォームモデルと、アプリケーションモデル記憶部102bに記憶されたアプリケーションモデルとを用いてアプリケーションの検証を行う手段であり、本発明におけるモデル検証手段である。検証の具体的な内容については後述する。検証結果出力部104は、アプリケーションの検証結果を出力する手段である。検証結果は、たとえばTCP/IPを利用してネットワーク経由でソフトウェア管理装置200へ送信してもよいし、ファイルとして出力してもよい。ファイルとして出力した場合、検証結果は外部媒体を介してソフトウェア管理装置200へ取り込まれる。検証結果を出力できる形式であれば、出力先の媒体はどのようなものであってもよい。出力される情報の具体的な内容については後述する。プログラム生成部105は、作成したアプリケーションモデル102bをソースコード、もしくは実行形式のプログラムに変換する手段である。モデル記述言語で記述されたアプリケーションモデルを、コンパイラやモデルコンパイラ等によってソースコードないしは実行形式のプログラムに変換する。次に、ソフトウェア管理装置200について説明を行う。検証結果入力部201は、検証結果出力部104が出力した検証結果を取得する手段である。検証結果出力部104と同様に、入力元の媒体はどのようなものであってもよい。ネットワーク経由で検証結果が送信される場合、検証結果入力部201はたとえばTCP/IPによってデータを受信し、検証結果がファイルである場合、光学ドライブなどを用いて記憶媒体より読み込みを行う。検証結果記憶部202は、取得した検証結果を保存する手段である。ソフトウェア管理装置200は、複数の開発者が作成した複数アプリケーションの検証結果を記録することができる。検証結果入力部201と検証結果記憶部202が、本発明における検証結果記憶手段に該当する。品質情報検索部203は、検証結果記憶部202に記録された検証結果より、指定した問い合わせ要求に該当する情報を検索する手段である。指定した条件に合致するアプリケーションを検索することもでき、指定したアプリケーションの検証結果を要求することもできる。アプリケーションプログラム記憶部204は、開発者より送付された、完成したアプリケーション本体を記憶する手段である。アプリケーションプログラム記憶部204に記憶されたアプリケーションが、最終的に利用者に配布される。プラットフォームモデル管理部205は、ソフトウェア作成装置100に対して配布する複数のプラットフォームモデルを記憶する手段である。プラットフォームモデルの配布および使用方法については後述する。次に、アプリケーションプロバイダによって配布される開発ソフトウェアと、ソフトウェア作成装置との関係を示し、アプリケーションモデルおよびプラットフォームモデルを用いてアプリケーションを検証する方法を説明する。図2は、ソフトウェア作成装置上で動作する開発ソフトウェア、および作成されるアプリケーションを表した図である。開発環境400は、開発ソフトウェアのパッケージであり、複数のコンポーネントによって成り立つ。開発者は、開発環境400をアプリケーションプロバイダより取得し、ソフトウェア作成装置に格納する。開発環境は、ネットワーク経由で送信されてもよいし、記憶媒体によって移動されてもよい。開発基盤408は、例えばオープンソースで提供されているEclipseのような統合開発環境である。開発基盤408上で動作するエディタ405は、通常のアプリケーションモデル作成にて使用されるコンポーネントであり、既存の技術によるものである。エディタ405はモデル作成部101にて実行される。作成されたアプリケーションモデル301は、前述したようにアプリケーションモデル記憶部102bに格納される。作成されたアプリケーションモデルは、モデルコンパイラ406によって、ソースコードに変換することができる。ソースコードは、コンパイラ407によって実行形式のプログラムに変換することができる。また、変換されたプログラムは、エミュレータ402によって仮想環境で実行することが可能である。モデルコンパイラ406、コンパイラ407、エミュレータ402、およびライブラリ404は、プログラム生成部105に格納され実行される。プラットフォームモデル403は、プラットフォームモデル記憶部102aに格納される。従来技術では、プラットフォームモデルは開発者に配布されるものではないが、本実施形態では、プラットフォームモデル管理部205から取得され、開発環境400と一緒に開発者に配布される。ここで、アプリケーションとプラットフォームとの関係について説明する。図3は、アプリケーション、プラットフォーム、ハードウェアの関係を示した図である。実施形態の説明におけるプラットフォームとは、ハードウェアの差異を吸収するためのオペレーティングシステムOS、ミドルウェア、または仮想化されたハードウェアを指す。アプリケーションは、プラットフォームに対してAPIApplicationProgramInterfaceを経由して入出力を行うことで各種の機能を実現する。従って、APIが定義されているアプリケーションモデルとプラットフォームモデルを組み合わせることによって、アプリケーションがプラットフォーム上でどのように動作するのかを検証することができる。図2に戻り、説明を続ける。本実施形態に係るソフトウェア作成装置では、アプリケーションモデルとプラットフォームモデルとを、モデルチェッカ401によりモデルレベルで対比させることによって検証を行う。モデルチェッカ401は、モデルチェック部103に格納され、実行される。検証の方法を説明する前に、検証ルールについて説明する。検証ルールとは、試験項目仕様書に該当するものであり、アプリケーションのどのような項目について検証を行い、どのような情報を保存するかが定義されている情報である。この検証ルールに従ってモデルチェッカは検証動作を行う。例えば、OSの互換性チェックが要求されていた場合、モデルチェッカは、複数バージョンのプラットフォームモデルを用い、アプリケーションモデルで定義されているインタフェース呼び出しが全てプラットフォームモデル側と整合しているかを確認する。また、アプリケーションに固有なインタフェースの検証が要求されていた場合、必須とされるインタフェースがアプリケーションモデルに備わっているかを確認する。モデル記述言語にAADLを用いた場合、検証の対象はソフトウェアの構造に限られるが、ソフトウェアの振る舞いを記述できる言語を使用し、ソフトウェアの振る舞いについての検証を行ってもよい。この場合、定められた通りにイベントが発生するかを検証ルールとして定義する。このように、検証ルールは自由に定義することができる。検証ルールは、開発者が作成してもよいが、複数の開発者のアプリケーションを一元管理するという発明の性質上、アプリケーションプロバイダが提供することが望ましい。検証ルールは、開発環境400に含まれる形で、たとえばモデルチェッカ401に含まれて配布される。アプリケーションモデル、プラットフォームモデル、検証ルールを用いた検証の方法を、AADLを用いた場合を例に具体的に説明する。AADLの開発環境であるOSATEOpenSourceAADLToolEnvironmentでは、整合性解析、リソース解析、フロー解析の三つを用いてAADLモデルの検証を行うことができる。整合性解析は、アプリケーションモデルとプラットフォームモデル間のインタフェースの整合性が取れているかを確認し、設計仕様のエラーを検出する検証方法である。例えば、音楽ファイルを読み込んで再生するアプリケーションにおいては、ファイルの読み込みが完了する前に再生ボタンを押すとエラーが発生してしまう。そのため、読み込みが完了したことを通知するAPIを呼び出す実装が必須となる。検証ルールにはアプリケーションモデルに当該APIが実装されているかといった定義を行ってもよいし、呼び出しの型引数がプラットフォームモデルと整合しているかといった定義を行ってもよい。また、プラットフォームモデルに、アプリケーションモデルから行われる呼び出しに対応するインタフェースが全て定義されており、型が一致しているかといったルールを用いてもよい。整合性解析によって、プラットフォームとアプリケーションとの互換性エラーを検出することができる。リソース解析では、アプリケーションが稼働した状態でのプロセッサの利用率占有時間を知ることができる。アプリケーションモデルには、オブジェクトごとに演算時間とデッドラインが定義されている。AADLスレッドをプロセッサに配置することにより、複数のアプリケーションが稼働した場合の負荷の見積もりを行うことができる。検証ルールには、例えばCPUに制限値以上の負荷をかけていないかといった定義を行うことができる。フロー解析では、AADLのフローを使って定義したデータやイベントの経路において、伝送遅延時間の要求値を満足するか検証することができる。モデル間の通信に要する時間と演算時間を合計して、遅延時間に問題がないかをチェックする。検証ルールには、例えば要求性能値を満たしていないフローが無いかといった定義を行うことができる。検証結果は、モデルチェッカ401によって集計され、検証結果出力部104に出力される。検証結果は、例えばOSのバージョンごとに集計し、OSバージョン2.2における動作=問題なしといった形式で出力してもよいし、検証ルールに定義されたチェック項目ごとにOSバージョン2.2におけるフローXに対する遅延時間=問題なしといった形式で出力してもよい。また、測定結果の数値を入れてもよいし、動作に問題があるAPIの名称のみをリスト化してもよい。ネットワークを経由して検証結果の出力を行う場合、検証結果出力部104は、例えば検証結果をネットワーク経由で送信するプラグインを開発基盤408に追加することによって実現することができる。次に、具体的なアプリケーション開発の手順を説明する。図4は、ソフトウェア作成装置100を用いて開発者がアプリケーション開発を行う手順を示したフローチャート図である。アプリケーション開発において、開発者はまずアプリケーションモデルを作成するS11。アプリケーションモデルは、前述のOSATEといった開発ソフトウェアをEclipse上に構築すること等により作成することができる。次に、作成したモデルを、モデルチェッカによって検証しS12、検証結果を出力するS13。検証結果は、前述の通りネットワーク経由でソフトウェア管理装置200へ送信してもよいし、単体で出力してもよい。アプリケーションプロバイダに提出できる形態であれば、どのようなものであってもよい。検証結果を出力した後、開発者は、アプリケーションモデルからプログラムのソースコードを生成するS14。そして、ソースコードから実行形式のプログラムを生成し、アプリケーションプロバイダに送付するS15。なお、アプリケーションモデルから自動でコードを生成せず、開発者が自らコーディングを行っても良い。また、検証の実施と同時にソースコードないしはプログラムを生成してもよい。検証と成果物の生成を同時に行うことで、検証結果と生成された成果物の内容が一致していることが保証できるようになる。送られたアプリケーション本体は、アプリケーションプログラム記憶部204に格納される。アプリケーション本体についても、検証結果と同様に、ネットワーク経由で送信されてもよいし、記憶媒体によって移動されてもよい。次に、アプリケーションプロバイダ側にて、品質管理を行う方法の説明を行う。図5は、ソフトウェア作成装置へ送信される検証結果を表形式で表した例である。本例では、アプリケーションプロバイダ側にて把握したい情報を評価項目に分類し、対応する評価値を、開発者IDおよびアプリケーションIDごとに保持する形式をとっている。検証結果は検証結果記憶部202へ保存される。図5aは、APIの名称を評価項目とし、アプリケーションモデルに当該APIが備わっているかを評価値とした例である。このようにすることで、実装しているべきAPIがアプリケーションに備わっているか否かを知ることができる。また、図5bは、OSごとの互換性を評価項目とし、プラットフォームモデルとの互換性の有無を評価値とした例である。複数のプラットフォームモデルを使用して、アプリケーションに実装されている全てのAPIについてチェックを行い、問題が無かったバージョンのみをYES動作可とすることができる。この他にも、遅延時間の計測結果や、特定の機能が実装されているかといった評価項目を設けてもよい。このように、評価項目は、モデルチェッカによって取得できる情報であればどのような情報であってもよい。これにより、アプリケーションプロバイダは、未公開のアプリケーションのうち、定められた条件を満たすアプリケーションを抽出し、公開を決定することができる。また、ユーザの求めに応じて、公開中のアプリケーションのうち一定の条件を満たすものを抽出してもよい。品質情報検索部203は、検証結果記憶部202に記録されたデータに対して検索を行い、結果を取得することができる。取得された結果に対応するアプリケーションをアプリケーションプログラム記憶部204から取得することで、条件を満たすアプリケーションを利用者に提供することができる。なお、プログラム生成部105、品質情報検索部203、アプリケーションプログラム記憶部204については、検証結果に基づいてアプリケーションをユーザに提供するための付随的な役割を果たすものであり、本発明の必須構成ではない。また、プラットフォームモデル管理部205も、プラットフォームモデルをソフトウェア作成装置に提供することができれば、ソフトウェア管理装置内に保持される必要はない。また、本実施形態では評価値を文字列によって記録する例を挙げたが、他の形式であっても構わない。例えば、不具合発生時のメモリダンプ情報であってもよいし、開発者による試験時の操作ログであってもよい。また、文字列だけでなく、バイナリ形式のオブジェクトが格納されていてもよい。本実施形態によれば、オープンプラットフォームを用いて複数の開発者がアプリケーションを作成する開発形態において、ソフトウェア管理装置が、複数のアプリケーションの品質情報を一括して管理することができる。また、開発者はアプリケーションの検証結果のみをアプリケーションプロバイダに送信すればよいため、設計情報を外部に提供する必要がなく、秘匿性が確保できるという利点がある。変形例なお、各実施形態の説明は本発明を説明する上での例示にすぎず、本発明は、発明の趣旨を逸脱しない範囲で適宜変更して実施することができる。例えば、第一の実施形態では、ソフトウェア作成装置を例示し、本発明に係るソフトウェア検証装置の一例としたが、アプリケーションモデルを作成できる手段があれば、アプリケーションモデルの作成と検証は別個に行ってもよい。この場合、モデル作成部101が、アプリケーションモデル取得手段に置き換えられる。また、図1では検証結果とアプリケーション本体が別個にソフトウェア管理装置へ送付される形態を記載したが、同時に送られてもよい。また、アプリケーションモデルは、モデル記述言語による設計を行わず、テキスト形式や表計算ソフトにて仕様を記述した後、記述した仕様を変換ツールによってモデル記述言語に変換してもよい。また、第一の実施形態では、ネットワークを経由して検証結果を送信するが、ネットワーク経由で送信する場合、暗号化技術を用いて検証結果の改変を防いでもよい。例えば、検証結果出力部104が、検証結果にメッセージ認証コードを付加してもよいし、公開鍵暗号方式を用いた電子署名を付加してもよい。これによって、ソフトウェア管理装置は、受信した検証結果が改変されていないことを確認することができる。また、検証結果には、検証に使用したモデルの名称を含ませてもよい。これによって、ソフトウェア管理装置は、特定のモデルを用いて検証が実施されたことを確認することができる。また、第一の実施形態では、モデル記述言語として、静的なアーキテクチャを記述する言語であるAADLを例に挙げたが、ソフトウェアの振る舞いを記述することができるPromelaProcessorProtocolMetaLanguageなどの検証用モデリング言語を用いてもよい。Promelaによる記述は、SPINモデルチェッカによって検証することができ、これをモデルチェック部103にて実行してもよい。第一の実施形態では、AADLによって三種類の検証を行う例を挙げたが、他のモデル記述言語を用いる場合、それぞれの言語に適した検証方法を使用することができる。また、検証結果の内容についても、例示したものに限られない。また、開発環境を開発者に直接配布せず、Webサービスとしてネットワーク経由で利用できるようにしてもよい。この方法を用いた場合、プラットフォームのバージョンアップ等によってプラットフォームモデルに変更が生じても、モデルを配布し直さなくてもよいという利点がある。ただし、通信文の暗号化等によるデータの保護が必要となる。