(57)【要約】【課題】コンポーネントを結合してプログラムを生成するユーザ端末において、実際にプログラムを生成する前にプログラムの正当性を検証できるようにすること。【解決手段】本発明は、コンポーネントに動作を検証するための検証情報および実装を記述しておき、このコンポーネントを用いてプログラムを生成するのに先立って、このコンポーネントの検証情報が生成しようとするプログラムの仕様を満たすか否かを検証するようにした。これにより、コンポーネントを用いて実際にプログラムを生成しなくても、コンポーネントの検証情報がプログラムの仕様を満たすか判断することにより、選択したコンポーネントがプログラム仕様を満たすか検証できる。【選択図】      図１
2004326366.tif 000002
【特許請求の範囲】
【請求項１】
動作を検証するための検証情報および実装が記述されたコンポーネントを格納するコンポーネント格納部と、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を格納するプログラム仕様格納部と、前記プログラム仕様の前記識別情報に基づいて前記コンポーネントを選択し、選択した前記コンポーネントの前記検証情報を用いて前記選択したコンポーネントが前記プログラムの前記仕様を満たすか否かを検証する検証実行部と、前記検証実行部が前記選択したコンポーネントが前記プログラムの仕様を満たすと検証した場合に前記プログラムの仕様を用いて前記選択したコンポーネントの前記実装を組み合わせて前記プログラムを生成するプログラム生成部と、を具備したことを特徴とするプログラム検証生成装置。
【請求項２】
前記プログラムの仕様には前記必要なコンポーネントの接続関係および満たすべき要求仕様であるプログラム要求仕様が記述され、前記コンポーネントの前記検証情報には前記コンポーネントの作成時に動作の正しさを検証した検証結果が記述され、
前記検証実行部は、前記プログラム要求仕様と前記コンポーネントの前記検証結果とを比較することにより、前記選択したコンポーネントが前記プログラム仕様を満たすか否かを検証することを特徴とする請求項１記載のプログラム検証生成装置。
【請求項３】
前記プログラムの仕様には前記必要なコンポーネントの接続関係および満たすべき要求仕様であるプログラム要求仕様と、前記プログラムの入出力関係を満たす入出力モデルと、が記述され、
前記コンポーネントの前記検証情報には前記コンポーネントの入出力部分の動作の抽象化モデルが記載されたモデル記述が記述され、
前記検証実行部は、前記選択したコンポーネントの前記モデル記述を前記入出力モデルに従って繋ぎ合わせて検証データを生成し、生成した前記検証データを解析し、解析した結果が前記プログラム要求仕様を満たすか判断することにより、前記選択したコンポーネントが前記プログラム仕様を満たすか否かを検証することを特徴とする請求項１記載のプログラム検証生成装置。
【請求項４】
前記プログラムの仕様には前記プログラムの仕様には必要なコンポーネントの接続関係および満たすべき要求仕様であるプログラム要求仕様と、前記プログラムの入出力関係を満たす入出力モデルと、が記述され、
前記コンポーネントの前記検証情報には前記コンポーネントの作成時に動作の正しさを検証した検証結果および前記コンポーネントの動作モデルが記載されたモデル記述が記述され、
前記検証実行部は、前記プログラム要求仕様と前記コンポーネントの前記検証結果とを比較し前記選択したコンポーネントが前記プログラム仕様を満たさないと検証した場合に、前記選択したコンポーネントの前記モデル記述を前記入出力モデルに従って繋ぎ合わせて検証データを生成し、生成した検証データを解析し、解析した結果が前記プログラム要求仕様を満たすか判断することにより、前記選択したコンポーネントが前記プログラム仕様を満たすか否かを最終的に検証することを特徴とする請求項１記載のプログラム検証生成装置。
【請求項５】
前記コンポーネントの更新を検出する更新受信部と、前記更新受信部の指示により更新された前記コンポーネントを取得する取得部と、を具備し、
前記検証実行部は前記更新されたコンポーネントが前記プログラム仕様を満たすか検証し、前記プログラム生成部は前記検証実行部が前記更新されたコンポーネントが前記プログラム仕様を満たすと検証した場合に前記更新されたコンポーネントと前記プログラム仕様を用いた更新プログラムを生成することを特徴とする請求項１から請求項４のいずれかに記載のプログラム検証生成装置。
【請求項６】
動作を検証するための検証情報および実装が記述されたコンポーネントを伝送するコンポーネント伝送部と、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を伝送するプログラム仕様伝送部と、を具備したことを特徴とするプログラム配信装置。
【請求項７】
請求項６記載のプログラム配信装置と、請求項１記載のプログラム検証生成装置と、を具備し、前記プログラム検証生成装置は前記プログラム配信装置から伝送されてきた前記プログラム仕様および前記コンポーネントを格納することを特徴とするプログラム検証生成システム。
【請求項８】
動作を検証するための検証情報および実装が記述されたコンポーネントを取得するステップと、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を取得するステップ、前記プログラム仕様の前記識別情報に基づいて前記コンポーネントを選択するステップと、選択した前記コンポーネントの前記検証情報を用いて前記選択したコンポーネントが前記プログラムの前記仕様を満たすか否かを検証するステップと、前記選択したコンポーネントが前記プログラムの仕様を満たすと検証した場合に前記プログラムの仕様を用いて前記選択したコンポーネントの前記実装を組み合わせて前記プログラムを生成するステップと、を具備したことを特徴とするプログラム検証生成方法。
【請求項９】
動作を検証するための検証情報および実装が記述されたコンポーネントを伝送するステップと、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を伝送するステップと、を具備したことを特徴とするプログラム配信方法。
【請求項１０】
コンピュータに、動作を検証するための検証情報および実装が記述されたコンポーネントを取得するステップと、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を取得するステップ、前記プログラム仕様の前記識別情報に基づいて前記コンポーネントを選択するステップと、選択した前記コンポーネントの前記検証情報を用いて前記選択したコンポーネントが前記プログラムの前記仕様を満たすか否かを検証するステップと、前記選択したコンポーネントが前記プログラムの仕様を満たすと検証した場合に前記プログラムの仕様を用いて前記選択したコンポーネントの前記実装を組み合わせて前記プログラムを生成するステップと、を行わせることを特徴としたプログラム。
【請求項１１】
コンピュータに、動作を検証するための検証情報および実装が記述されたコンポーネントを伝送するステップと、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を伝送するステップと、を行わせることを特徴としたプログラム。
【請求項１２】
請求項１０または請求項１１記載のプログラムを格納したことを特徴とするコンピュータ読み取り可能な記憶媒体。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、コンポーネントがプログラムの要求仕様を満たすか否かを検証するプログラム検証生成装置およびプログラム検証生成方法に関する。
【０００２】
【従来の技術】
従来のプログラムソフトウェア開発手法において、プログラムの再利用性を高めるため、プログラムを機能レベルで分割し、各機能を統合してひとつの製品を開発する手法が存在する。このような、機能レベルで分割されたプログラム部品をコンポーネントと呼ぶ。各コンポーネントは、他のコンポーネントとの依存関係が極力少なくなるよう設計するため、コンポーネントを他の用途へ転用することが容易となっている。
【０００３】
コンポーネントベースのプログラム開発の例としては、例えば、特許文献１に記載の方法や、Ｊａｖａ（Ｒ）Ｂｅａｎｓが挙げられる。Ｊａｖａ（Ｒ）Ｂｅａｎｓを用いたプログラム開発では、ビルダーと呼ばれるグラフィカルなツールを用いてＪａｖａ（Ｒ）Ｂｅａｎｓコンポーネントを接続することでプログラムを開発可能であり、従来のようなコーディングが不要である。
【０００４】
【特許文献１】
特開平１１−２３４２７６号公報
【０００５】
【発明が解決しようとする課題】
従来、コンポーネントを結合し、検証を行うことでプログラムを生成する作業は、プログラムの開発元において行われるものであった。しかしながら、実現するプログラムのフレームワークをプログラムの実行端末、すなわち、ユーザ端末に与え、フレームワークに基づいてコンポーネントを自動的に結合することで実現するシステムを考えた場合には、コンポーネントの結合は開発元ではなく、プログラムの実行端末で行われることになる。
【０００６】
このようなプログラムの構成方法を適用すると、コンポーネントの選択はユーザに任されることになり、ユーザに自由度の高いカスタマイズをさせることができる。
【０００７】
しかし、このような方法の場合、コンポーネントの結合後の検証はユーザ端末で行わなければならず、検証作業がユーザの負担となる。また、開発元でユーザと同じ実行端末を準備して、予め全ての組み合わせに対してコンポーネントの結合、検証を行うという方法も考えられる。しかしながら、多数のコンポーネントが存在する場合には全ての組み合わせを検証することは困難である。
【０００８】
上記の課題を鑑み、本発明では、コンポーネントを結合してプログラムを生成する装置において、実際にプログラムを生成する前にプログラムの正当性を検証できるようにすることを目的とする。
【０００９】
【課題を解決するための手段】
本発明は、コンポーネントに動作を検証するための検証情報および実装を記述しておき、このコンポーネントを用いてプログラムを生成するのに先立って、このコンポーネントの検証情報が生成しようとするプログラムの仕様を満たすか否かを検証するようにした。
【００１０】
これにより、実際にプログラムを生成する前にプログラムの正当性を検証できる。
【００１１】
【発明の実施の形態】
本発明の第１の態様にかかるプログラム検証生成装置は、動作を検証するための検証情報および実装が記述されたコンポーネントを格納するコンポーネント格納部と、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を格納するプログラム仕様格納部と、前記プログラム仕様の前記識別情報に基づいて前記コンポーネントを選択し、選択した前記コンポーネントの前記検証情報を用いて前記選択したコンポーネントが前記プログラムの前記仕様を満たすか否かを検証する検証実行部と、前記検証実行部が前記選択したコンポーネントが前記プログラムの仕様を満たすと検証した場合に前記プログラムの仕様を用いて前記選択したコンポーネントの前記実装を組み合わせて前記プログラムを生成するプログラム生成部と、を具備した構成を採る。
【００１２】
これにより、選択したコンポーネントを用いて実際にプログラムを生成しなくても、選択したコンポーネントの検証情報がプログラムの仕様を満たすか判断することにより、選択したコンポーネントがプログラム仕様を満たすか検証できる。この結果、実際に生成したプログラムを動作させなくてもプログラムの動作の検証を行うことができる。
【００１３】
本発明の第２の態様は、第１の態様にかかるプログラム検証生成装置において、前記プログラムの仕様には前記必要なコンポーネントの接続関係および満たすべき要求仕様であるプログラム要求仕様が記述され、前記コンポーネントの前記検証情報には前記コンポーネントの作成時に動作の正しさを検証した検証結果が記述され、前記検証実行部は、前記プログラム要求仕様と前記コンポーネントの前記検証結果とを比較することにより、前記選択したコンポーネントが前記プログラム仕様を満たすか否かを検証する。
【００１４】
これにより、コンポーネントの動作の正しさを検証した検証結果とプログラム要求仕様を比較することにより、選択したコンポーネントがプログラム仕様を満たすか否かを検証できる。また、検証結果は、コンポーネントの全ての動作に対して検証を行ったものではないので、検証結果を用いた検証することにより、コンポーネントの代表的な動作がプログラム仕様を満たすか検証できる。つまり、検証結果を用いた検証を行うことにより、処理コストの少ない検証を行うことができる。
【００１５】
本発明の第３の態様は、第１の態様にかかるプログラム検証生成装置において、前記プログラムの仕様には前記必要なコンポーネントの接続関係および満たすべき要求仕様であるプログラム要求仕様と、前記プログラムの入出力関係を満たす入出力モデルと、が記述され、前記コンポーネントの前記検証情報には前記コンポーネントの入出力部分の動作の抽象化モデルが記載されたモデル記述が記述され、前記検証実行部は、前記選択したコンポーネントの前記モデル記述を前記入出力モデルに従って繋ぎ合わせて検証データを生成し、生成した前記検証データを解析し、解析した結果が前記プログラム要求仕様を満たすか判断することにより、前記選択したコンポーネントが前記プログラム仕様を満たすか否かを検証する。
【００１６】
これにより、モデル記述を用いてコンポーネントがプログラム仕様を満たすか検証できる。モデル記述には、コンポーネントの入出力部分の動作を抽象化した記述がなされているので、モデル記述を用いた検証により、コンポーネントの入出力部分に関する仕様が、プログラム仕様を満たすか確実に検証できる。
【００１７】
本発明の第４の態様は、第１の態様にかかるプログラム検証生成装置において、前記プログラムの仕様には前記プログラムの仕様には必要なコンポーネントの接続関係および満たすべき要求仕様であるプログラム要求仕様と、前記プログラムの入出力関係を満たす入出力モデルと、が記述され、前記コンポーネントの前記検証情報には前記コンポーネントの作成時に動作の正しさを検証した検証結果および前記コンポーネントの動作モデルが記載されたモデル記述が記述され、前記検証実行部は、前記プログラム要求仕様と前記コンポーネントの前記検証結果とを比較し前記選択したコンポーネントが前記プログラム仕様を満たさないと検証した場合に、前記選択したコンポーネントの前記モデル記述を前記入出力モデルに従って繋ぎ合わせて検証データを生成し、生成した検証データを解析し、解析した結果が前記プログラム要求仕様を満たすか判断することにより、前記選択したコンポーネントが前記プログラム仕様を満たすか否かを最終的に検証する。
【００１８】
これにより、まず、検証結果を用いた検証により、コンポーネントがプログラム仕様を満たすかどうかを高速に検証し、必要なら、次に、モデル記述を用いた検証により、コンポーネントがプログラム仕様を満たすかどうかを確実に検証するという、２段階の検証ができる。
【００１９】
本発明の第５の態様は、第１の態様から第４の態様のいずれかにかかるプログラム検証生成装置において、前記コンポーネントの更新を検出する更新受信部と、前記更新受信部の指示により更新された前記コンポーネントを取得する取得部と、を具備し、前記検証実行部は前記更新されたコンポーネントが前記プログラム仕様を満たすか検証し、前記プログラム生成部は前記検証実行部が前記更新されたコンポーネントが前記プログラム仕様を満たすと検証した場合に前記更新されたコンポーネントと前記プログラム仕様を用いた更新プログラムを生成する。
【００２０】
これにより、更新されたコンポーネントがプログラム仕様を満たすか検証でき、今まで正常に動作していたプログラムがコンポーネントの更新により動作しなくなるという課題を解決することができる。
【００２１】
本発明の第６の態様にかかるプログラム配信装置は、動作を検証するための検証情報および実装が記述されたコンポーネントを伝送するコンポーネント伝送部と、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を伝送するプログラム仕様伝送部と、を具備した構成を採る。
【００２２】
このようなコンポーネントとプログラム仕様を伝送することにより、受信側で、コンポーネントを用いて実際にプログラムを生成しなくても、コンポーネントの検証情報がプログラムの仕様を満たすか判断することにより、コンポーネントがプログラム仕様を満たすか検証できる。
【００２３】
本発明の第７の態様は、第６の態様のプログラム配信装置と、第１の態様のプログラム検証生成装置と、を具備し、前記プログラム検証生成装置は前記プログラム配信装置から伝送されてきた前記プログラム仕様および前記コンポーネントを格納することを特徴とするプログラム検証生成システムである。
【００２４】
本発明の第８の態様は、動作を検証するための検証情報および実装が記述されたコンポーネントを取得するステップと、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を取得するステップ、前記プログラム仕様の前記識別情報に基づいて前記コンポーネントを選択するステップと、選択した前記コンポーネントの前記検証情報を用いて前記選択したコンポーネントが前記プログラムの前記仕様を満たすか否かを検証するステップと、前記選択したコンポーネントが前記プログラムの仕様を満たすと検証した場合に前記プログラムの仕様を用いて前記選択したコンポーネントの前記実装を組み合わせて前記プログラムを生成するステップと、を具備したことを特徴とするプログラム検証生成方法である。
【００２５】
本発明の第９の態様は、動作を検証するための検証情報および実装が記述されたコンポーネントを伝送するステップと、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を伝送するステップと、を具備したことを特徴とするプログラム配信方法である。
【００２６】
本発明の第１０の態様は、コンピュータに、動作を検証するための検証情報および実装が記述されたコンポーネントを取得するステップと、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を取得するステップ、前記プログラム仕様の前記識別情報に基づいて前記コンポーネントを選択するステップと、選択した前記コンポーネントの前記検証情報を用いて前記選択したコンポーネントが前記プログラムの前記仕様を満たすか否かを検証するステップと、前記選択したコンポーネントが前記プログラムの仕様を満たすと検証した場合に前記プログラムの仕様を用いて前記選択したコンポーネントの前記実装を組み合わせて前記プログラムを生成するステップと、を行わせることを特徴としたプログラムである。
【００２７】
本発明の第１１の態様は、コンピュータに、動作を検証するための検証情報および実装が記述されたコンポーネントを伝送するステップと、あるプログラムに必要な前記コンポーネントに関する識別情報および前記プログラムの満たすべき仕様を記述したプログラム仕様を伝送するステップと、を行わせることを特徴としたプログラムである。
【００２８】
本発明の第１２の態様は、第１０の態様または第１１の態様のプログラムを格納したことを特徴とするコンピュータ読み取り可能な記憶媒体である。
【００２９】
（実施の形態１）
以下、本発明の実施の形態１にかかるプログラム検証生成システムについて添付図面を用いて説明する。
【００３０】
まず、実施の形態１にかかるプログラム検証生成システムの構成について図１を用いて説明する。図１は、実施の形態１にかかるプログラム検証生成システムの構成を説明する図である。
【００３１】
実施の形態１にかかるプログラム検証生成システム１０は、プログラムを配信する配信装置であるコンポーネント生成装置１００およびプログラム仕様生成装置２００と、実際にプログラムを生成するプログラム検証生成装置３００と、がネットワーク４０を介して接続された構成を採る。
【００３２】
コンポーネント生成装置１００は、プログラムを機能レベルで分割したプログラム部品であるコンポーネントを生成し、伝送する装置である。
【００３３】
コンポーネント生成装置１００には、コンポーネント生成に必要な情報を格納するコンポーネント情報格納部１０１が設けられている。コンポーネント情報格納部１０１は、具体的には、ハードディスクドライブに代表される蓄積媒体である。
【００３４】
コンポーネント情報格納部１０１には、検証結果記述格納部１０２と、モデル記述格納部１０３と、実装格納部１０４とが、設けられている。
【００３５】
検証結果記述格納部１０２は、コンポーネント作成時に、コンポーネントの動作の正しさを検証した結果の記述である検証結果記述を格納する部分である。検証結果記述は、あるプログラムにコンポーネントを使用した際にこのプログラムのプログラム仕様を満たすか検証するための検証情報である。
【００３６】
モデル記述格納部１０３は、コンポーネントの動作を抽象化した動作モデルを記述するモデル記述を格納する部分である。また、モデル記述は、あるプログラムにコンポーネントを使用した際にこのプログラムのプログラム仕様を満たすか検証するための検証情報である。
【００３７】
実装格納部１０４は、実際にターゲットマシン上で動作させることができるデータである実装を格納する部分である。
【００３８】
また、コンポーネント生成装置１００には、コンポーネントを生成するための基本情報や、検証結果記述、モデル記述、実装などを取得するための情報を入力する基本情報入力部１０５が設けられている。基本情報入力部１０５は、キーボードなどの一般的な入力手段である。
【００３９】
また、コンポーネント生成装置１００には、コンポーネントを生成する結合部１０６が設けられている。結合部１０６は、基本情報入力部１０５から入力された情報に対応する検証結果記述、モデル記述、実装を抽出し、結合することによりコンポーネントを生成する。結合部１０６は、生成したコンポーネントを伝送部１０７に送る。
【００４０】
伝送部１０７は、送られてきたコンポーネントを、ネットワーク４０を介してプログラム検証生成装置３００に伝送する。
【００４１】
プログラム仕様生成装置２００は、コンポーネント生成装置１００が生成したコンポーネントを用いたプログラムの仕様（プログラム仕様）を生成し、伝送する装置である。
【００４２】
プログラム仕様生成装置２００には、プログラムの満たすべき仕様であるプログラム仕様を生成するための情報を格納するプログラム仕様情報格納部２０１が設けられている。プログラム仕様情報格納部２０１は、具体的には、ハードディスクドライブに代表される蓄積媒体である。
【００４３】
プログラム仕様情報格納部２０１には、プログラム要求仕様格納部２０２と、入出力モデル格納部２０３と、が設けられている。
【００４４】
プログラム要求仕様格納部２０２は、プログラムの満たすべき仕様として、プログラムに必要なコンポーネント間の接続関係およびプログラムが満たすべき要求仕様を記載したプログラム要求仕様を格納している。
【００４５】
入出力モデル格納部２０３は、プログラムが満たすべき仕様として、プログラムの入出力関係を記述した入出力モデルを格納している。
【００４６】
また、プログラム仕様生成装置２００には、プログラム仕様を生成するための基本情報や、プログラム要求仕様や入出力モデルを取得するための情報を入力する基本情報入力部２０４が設けられている。基本情報入力部２０４は、キーボードなどの一般的な入力手段である。
【００４７】
また、プログラム仕様生成装置２００には、プログラム仕様を生成する結合部２０５が設けられている。結合部２０５は、基本情報入力部２０４から入力された情報と、この情報に対応するプログラム要求仕様および入出力モデルを抽出し、結合することによりプログラム仕様を生成する。結合部２０５は、生成したプログラム仕様を伝送部２０６に送る。
【００４８】
伝送部２０６は、プログラム仕様生成装置２００が生成したプログラム仕様をプログラム検証生成装置３００に伝送する。
【００４９】
プログラム検証生成装置３００は、プログラム仕様生成装置２００が生成したプログラム仕様に基づいて、コンポーネント生成装置１００が生成したコンポーネントを選択し、コンポーネントがプログラム仕様のプログラム要求仕様を満たすか否かを検証し、要求仕様を満たす場合に選択したコンポーネントを用いてプログラムを生成する装置である。
【００５０】
プログラム検証生成装置３００には、プログラム仕様生成装置２００が生成したプログラム仕様およびコンポーネント生成装置１００が生成したコンポーネントを受信する伝送部３０１が設けられている。伝送部３０１は、受信したプログラム仕様をプログラム仕様格納部３０２に、受信したコンポーネントをコンポーネント格納部３０３に送る。
【００５１】
プログラム仕様格納部３０２は、プログラム仕様を格納する手段である。具体的には、ハードディスクドライブに代表される蓄積媒体である。
【００５２】
コンポーネント格納部３０３は、コンポーネントを格納する手段である。具体的には、ハードディスクドライブに代表される蓄積媒体である。
【００５３】
検証実行部３０４は、プログラム仕様格納部３０２からプログラム仕様およびコンポーネント格納部３０３からコンポーネントを取り出し、コンポーネントを組み合わせてプログラムを生成した場合に、生成したプログラムがプログラム仕様を満たすかどうかを検証する手段である。つまり、検証実行部３０４は、コンポーネントがプログラム仕様を満たすか検証する。
【００５４】
具体的には、検証実行部３０４は、２つのステップにより、コンポーネントがプログラム仕様を満たすか確認する。
【００５５】
まず、第１に、検証実行部３０４は、コンポーネントに格納されている検証結果記述を取り出し、検証結果記述に基づいて、コンポーネントがプログラム仕様のプログラム要求仕様を満たすかどうかを検証する（以下、整合性確認と呼ぶ）。
【００５６】
検証結果記述は、コンポーネント生成装置１００において、予め動作の正当性を検証した結果記述である。このため、プログラム仕様のプログラム要求仕様に対応する全ての動作の検証が記述されているとは限らない。つまり、検証結果記述だけでは、プログラム仕様の検証ができない場合がある。
【００５７】
そこで、第２に、検証実行部３０４は、検証結果記述に基づくコンポーネントの検証で検証できなかったプログラム要求仕様に対しては、検証器を用いて検証を行う（以下、検証器による検証と呼ぶ）。
【００５８】
具体的には、まず、検証実行部３０４は、コンポーネントに格納されるモデル記述を取り出し、プログラム要求仕様の入出力モデルに従って繋ぎ合わせ、必要な情報を付加して検証用のデータを生成する。次に、検証実行部３０４は、この検証用のデータを検証器にかけて検証を行う。そして、検証実行部３０４は、検証器を用いた検証結果が、プログラム仕様のプログラム要求仕様を満たすか判断する。
【００５９】
モデル記述は、コンポーネントの入出力部分に関する全ての動作の抽象化モデルであるので、検証器を用いた検証によりコンポーネントの入出力部分に関する動作がプログラム要求仕様を満たすか確実に検証できる。
【００６０】
また、検証実行部３０４が所有する検証器としては、例えば、ＳＰＩＮなどがある。
【００６１】
また、検証実行部３０４は、検証の結果、生成されるプログラムが要求仕様を満たすことが確認された場合には、プログラム生成部３０５にプログラムの生成指示を送信する。
【００６２】
プログラム生成部３０５は、検証実行部３０４からの生成指示により、プログラム仕様格納部３０２からプログラム仕様を取得し、プログラム仕様に従ってコンポーネントを選択、取得し、取得したコンポーネントの実装を組み合わせてプログラムを生成し、プログラム格納部３０６に生成したプログラムを格納する。
【００６３】
検証実行部３０４から生成指示により通知される情報としては、プログラム仕様格納部３０２に格納されるプログラム仕様の名前（ファイル名）、組み合わせるべきコンポーネントの名前（ファイル名）である。これらの情報に基づき、プログラム生成部３０５は、コンポーネントを読み出し、コンポーネント中の実装（実際にターゲットマシン上で動作させることができるデータ）をコンポーネントより取り出す。そして、プログラム生成部３０５は、取り出した実装を、プログラム仕様に基づいて組み合わせてプログラムを生成する。
【００６４】
プログラム格納部３０６は、生成されたプログラムを格納する手段である。具体的には、ハードディスクドライブに代表される蓄積媒体である。
【００６５】
なお、プログラム仕様格納部３０２、コンポーネント格納部３０３、プログラム格納部３０６は同一の媒体であってもよいし、異なっていてもよい。
【００６６】
ネットワーク４０は、有線網（ＡＤＳＬ、ＡＴＭ、ＬＡＮ、ケーブル、ダイアルアップ回線）、無線網（無線ＬＡＮ、ＦＷＡ、携帯電話網）を問わず、また、通信網、放送網（地上波デジタル、衛星デジタル）であってもよい。また、複数の伝送路を具備した形態であってもよい。
【００６７】
なお、実施の形態１では、コンポーネント生成装置１００およびプログラム仕様生成装置２００を別の装置として説明するが、同一の装置であってもよい。
【００６８】
次に、実施の形態１にかかるコンポーネント生成装置１００が生成するコンポーネントについてについて図２を用いて説明する。図２は、実施の形態１にかかるコンポーネントのフォーマットを示す図である。
【００６９】
図２に示すように、実施の形態１にかかるコンポーネント４００は、基本情報４０１、検証結果記述４０２、モデル記述４０３、および実装４０４から構成される。
【００７０】
基本情報４０１には、コンポーネントの、作成日、作成者、ライセンス形態、使用方法といった情報が格納されている。また、基本情報４０１には、上記に加えて、どういったコンポーネントがプログラムの部品であるかを表す識別情報が格納されている。この識別情報は、プログラム仕様作成者およびコンポーネント作成者とも予め知っており、プログラム仕様作成者は、作成したプログラム仕様から実際のプログラムを生成するのにどのコンポーネントを使用するかをこの識別情報を用いて指定する。
【００７１】
検証結果記述４０２には、コンポーネントを作成した際に、実際に検証を行って正しいことが保証されている動作や、その動作を行うために必要な前提条件を記されている。ここに記載される情報は、整合性確認の際に使用される。
【００７２】
モデル記述４０３は、コンポーネントの動作を抽象化した動作モデルを記述するモデル記述を格納する部分である。特に、モデル記述４０３は、コンポーネントの入出力に注目し、コンポーネントの入出力の動作を抽象化したモデルである。ここに格納されるモデル記述４０３は、検証器を用いた検証の際に利用される。
【００７３】
また、本実施の形態では、モデル記述４０３は、Ｐｒｏｍｅｌａで記述されている。このため、モデル記述４０３を結合して、コンポーネントの起動記述とメッセージ定義を追加するだけで、検証実行部３０４の検証器（ＳＰＩＮ）で検証可能なデータを生成することができる。
【００７４】
実装４０４は、実際にターゲットマシン上で動作するデータである。例えば、ＪＡＶＡ（Ｒ）の場合であれば、ＪＡＲファイルやクラスファイルなどであり、Ｃであれば、ライブラリなどである。また、プログラム生成部３０５がプログラムのコンパイル機能を持つ場合には、ソースコードであってもよい。
【００７５】
このように、実施の形態１のコンポーネント４００には、実装４０４だけでなく、整合性確認を行うための検証結果記述４０４や、検証器による検証を行うためのモデル記述が記述されている。
【００７６】
なお、基本情報４０１、検証結果記述４０２、モデル記述４０３は、実装４０４に電子透かしとして格納された形で配布されるものとしてもよい。プログラムに電子透かしを挿入する方法としては、特開２０００−７６０６４号公報などがあり、これらの方法を適用して上記の情報を電子透かしとして挿入することで、実装と実装の付加情報が一体化し、取り扱いの利便性が向上する。
【００７７】
次に、コンポーネントの具体的な例について図３を用いて説明する。図３は、実施の形態１にかかるコンポーネントの記述の例を説明するための図である。
【００７８】
図３に示すコンポーネント５００には、基本情報５０１、検証結果記述５０２、モデル記述５０３、および実装５０４が記述されている。
【００７９】
基本情報５０１には、図中５０１ａに示されるように、コンポーネントの説明文などが記されている。
【００８０】
また、５０１ｂで記される部分には、コンポーネント５００を識別する識別情報が記述されている。識別情報は、コンポーネントの種別を表す識別子であり、後述するプログラム仕様８００において、コンポーネントを指定する際に使用される。
【００８１】
検証結果記述５０２は、“ＰＲＥ：”以降に記述される事前条件５０４、“ＰＯＳＴ：”以降に記載される事後条件５０５により記述される。事前条件５０４は、このコンポーネントを呼び出す際に守られるべき条件であり、事後条件５０５は事前条件５０４が守られた場合に成り立つことが保証される条件である。
【００８２】
なお、各条件に付与されている記号“１：”、“２：”は、事前条件と事後条件の対応を表している。例えば、“１：”を付与された事前条件が守られる場合に、“１：”を付与された事後条件が成り立つことが保証されることを示す。
【００８３】
モデル記述５０３は、上述したように、コンポーネントの実装をモデル化（抽象化）した記述である。この例ではＰｒｏｍｅｌａにより記述されている。
【００８４】
モデル記述５０３により、このコンポーネントの実装では、ＮＴＤＶ＿ＳＴＡＲＴ＿ＲＥＱ、ＮＴＤＶ＿ＳＴＯＰ＿ＲＥＱを受信した際に、それぞれＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ、ＮＥＴ＿ＳＴＯＰ＿ＲＥＱをネットワーク４０に送信することがわかる。なお、この例では、２回連続でＮＴＤＶ＿ＳＴＡＲＴ＿ＲＥＱを受信した場合に、２回連続でＮＴＤＶ＿ＳＴＡＲＴ＿ＲＥＱを送信する実装になっている。
【００８５】
次に、コンポーネントの別の例について図４を用いて説明する。図４は、実施の形態１にかかるコンポーネントのその他の記述例を説明する図である。
【００８６】
図４に示すコンポーネント６００には、基本情報６０１、検証結果記述６０２、モデル記述６０３、および実装６０４が記述されている。
【００８７】
基本情報６０１には、図中６０１ａに示されるように、コンポーネントの説明文が記されている。また、６０１ｂで記される部分には、コンポーネント６００を識別する識別情報が記述されている。識別情報は、コンポーネントの種別を表す識別子であり、後述するプログラム仕様８００において、コンポーネントを指定する際に使用される。
【００８８】
検証結果記述６０２においては、事前条件の記述は存在しない。これは、事前条件なしで事後条件が成り立つことを示している。したがって、検証結果記述６０２から、ＮＴＤＶ＿ＳＴＡＲＴ＿ＲＥＱが続けて２回以上送信されることがないことがわかる。
【００８９】
モデル記述６０３は、実装６０４がＮＴＤＶ＿ＳＴＡＲＴ＿ＲＥＱ、ＮＴＤＶ＿ＳＴＯＰ＿ＲＥＱをそれぞれ２回以上連続して送信しないことを示している。
【００９０】
次に、プログラム仕様生成装置２００が生成するプログラム仕様について図５を用いて説明する。図５は、実施の形態１にかかるプログラム仕様のフォーマットを示す図である。
【００９１】
図５に示すように、実施の形態１にかかるプログラム仕様７００は、基本情報７０１、プログラム要求仕様７０２、および入出力モデル７０３から構成され。
【００９２】
基本情報７０１には、作成日、作成者、ライセンス形態、使用方法といった情報が格納されている。また、基本情報７０１には、プログラム仕様が実際にプログラムを生成するのにどのコンポーネントを使用するか指定する記述がなされている。この指定には、コンポーネントの識別情報が用いられている。
【００９３】
プログラム要求仕様７０２は、プログラムの要求仕様を記述する部分である。具体的には、プログラムを生成するのに必要なコンポーネントとその接続関係、および、プログラムが満たすべき仕様（具体的には例を用いて後述する）を記述する。
【００９４】
入出力モデル７０３は、プログラムが前提とする入出力部分のモデルを記述する。例えば、生成されるプログラムが、ＧＵＩを持ち、ファイルアクセスを行い、他のプロセスや端末と通信をする場合に、それぞれのＧＵＩ、ファイル、プロセス、ネットワークのモデルを記述する必要がある。
【００９５】
このように、実施の形態１にかかるプログラム仕様７００には、プログラムを生成するのに必要なコンポーネントとその接続関係、および、プログラムが満たすべき仕様、プログラムが前提とする入出力部分のモデルを記述されている。
【００９６】
次に、プログラム仕様の具体例について図６を用いて説明する。図６は、実施の形態１にかかるプログラム仕様の記述例を示す図である。
【００９７】
図６に示すプログラム仕様８００は、基本情報８０１、プログラム要求仕様８０２、入出力モデル８０３からなる。
【００９８】
プログラム要求仕様８０２のうち、ＣＯＭＰＯＮＥＮＴ｛…｝８０４は、使用するコンポーネントの識別情報を示す。この例では、ＳＴＡＲＴ＿ＳＴＯＰ＿ＰＲＯＴＯＣＯＬ＿ＧＵＩ（図４に示すコンポーネント（ＧＵＩコンポーネント）６００）、ＳＴＡＲＴ＿ＳＴＯＰ＿ＰＲＯＴＯＣＯＬ＿ＳＴＡＣＫ（図３に示すコンポーネント（プロトコルスタックコンポーネント）５００）という識別情報の付与されたコンポーネントを使用することを示している。
【００９９】
また、ＣＯＮＮＥＣＴＩＯＮ：８０５は、各コンポーネントがどういった接続関係を持つことを示している。この例では、ユーザとＧＵＩ、ＧＵＩとプロトコルスタック（ＮＴＤＶ）、プロトコルスタックとネットワークが接続していることを示す。
【０１００】
また、ＣＯＮＮＥＣＴＩＯＮ：８０５に記述されている、“ＵＳＲ”、“ＮＥＴ”は予め定められたユーザ、ネットワークを示す識別子であるものとし、“ＧＵＩ”、“ＮＴＤＶ”はＣＯＭＰＯＮＥＮＴ８０４により定義されている。
【０１０１】
ＣＯＮＮＥＣＴＩＯＮ：８０５により、モデル記述を用いた検証を行う際に、各モデルを接続することができる。
【０１０２】
Ｖｅｒｉｆ−Ｒｕｌｅ：８０６はプログラムの要求仕様を論理表現により表している。
【０１０３】
この例では、“ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ−＞！ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ  Ｕ  ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ”と記述されているが、”ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ“、”ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ”、“ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ”はそれぞれメッセージの送信を表す。また“−＞”は推移、“！”は否定、“Ｕ”は時相論理のＵｎｔｉｌ（“Ａ  Ｕ  Ｂ”で“Ｂが真となるまでＡは真”という意味となる）を表す。
【０１０４】
したがって、Ｖｅｒｉｆ−Ｒｕｌｅ：８０６全体として、“ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱが送信されたならば、ＮＥＴ＿ＳＴＯＰ＿ＲＥＱが送信されるまでＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱが送信されない”ということを表す。
【０１０５】
また、ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ−＞！ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ  Ｕ  ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱに関しての説明は、同様であるため、説明は省略する。
【０１０６】
また、入出力モデル８０３に関しては、この例では、ユーザのモデル（ＵＳＲ：８０７）と、ネットワークのモデル（ＮＥＴ：８０８）が記述されている。各モデルは、Ｐｒｏｍｅｌａにより記述されている。
【０１０７】
ユーザモデル８０７は、ｄｏ〜ｏｄの間に記載される“：：”記号から始まる一連の命令の組から１つをランダムに選択して繰り返し実行する。図の例では、「“ｔｏＧＵＩ！ＧＵＩ＿ＳＴＡＲＴ＿ＲＥＱ“、“ｔｏＧＵＩ！ＧＵＩ＿ＳＴＯＰ＿ＲＥＱ”のうちのどちらかを実行する」という動作を無限に繰り返すことをあらわしている。
【０１０８】
また、“ｔｏＧＵＩ！ＧＵＩ＿ＳＴＡＲＴ＿ＲＥＱ”は、ｔｏＧＵＩチャンネル（ＧＵＩとメッセージを送受信するチャンネル）にＧＵＩ＿ＳＴＡＲＴ＿ＲＥＱを送信する。ＧＵＩ＿ＳＴＡＲＴ＿ＲＥＱの送信は、ユーザがＳＴＡＲＴボタンの押下に相当するものである。したがって、ユーザモデルは、ＳＴＡＲＴ，ＳＴＯＰボタンをランダムに繰り返し押し続ける動作を表している。
【０１０９】
ネットワークモデル８０８は、“ｔｏＮＥＴ？ｉｎｐｕｔ”によりｔｏＮＥＴチャンネル（プロトコルスタックとデータを送受信するチャンネル）からデータを受信する（受信したデータはｉｎｐｕｔに格納される）。
【０１１０】
そして、“ｉｆ〜ｆｉ”により、受信したデータがＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱで、かつ現在の状態（ｓｔａｔｅ）がＳ＿ＳＴＯＰ（ＮＥＴ＿ＳＴＯＰ＿ＲＥＱを受信した状態）あるときに、状態をＳ＿ＳＴＡＲＴに変化させる。
【０１１１】
また、受信したデータがＮＥＴ＿ＳＴＯＰ＿ＲＥＱで、かつ現在の状態（ｓｔａｔｅ）がＳ＿ＳＴＡＲＴ（ＮＥＴ＿ＳＴＯＰ＿ＲＥＱを受信した状態）あるときに、状態をＳ＿ＳＴＯＰに変化させる。上記のどちらでもない場合には、エラー状態となる。
【０１１２】
したがって、この入出力モデル８０３は、ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ、もしくはＮＥＴ＿ＳＴＯＰ＿ＲＥＱのいずれかを続けて２回送信したときにプロトコルの仕様違反（エラー状態）となることを示している。
【０１１３】
次に、図３、図４に示すコンポーネントと、図６に示すプログラム仕様を用いて実現されるプログラムについて、図７を用いて説明する。図７は、実施の形態１にかかるプログラムの記述例を示す図である。
【０１１４】
図７に示すプログラム９００は、図４に示すＧＵＩコンポーネント６００と、図３に示すプロトコル（スタック）コンポーネント５００により構成され、以下の仕様を持つ。
【０１１５】
図７に示すプログラム９００は、ＧＵＩコンポーネント６００においてＳＴＡＲＴボタン９０１とＳＴＯＰボタン９０２を持ち、ＳＴＡＲＴボタン９０１がクリックされた際には、ネットワークへＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱというメッセージを送信する。また、ＧＵＩコンポーネント６００は、ＳＴＯＰボタン９０２が押されると、ＮＥＴ＿ＳＴＯＰ＿ＲＥＱをネットワークへ送信する。
【０１１６】
また、ＧＵＩコンポーネント６００は、ＳＴＡＲＴボタンが押された際には、プロトコル（スタック）コンポーネント５００にＮＴＤＶ＿ＳＴＡＲＴ＿ＲＥＱメッセージを送信し、ストップボタンが押された際にはＮＴＤＶ＿ＳＴＯＰ＿ＲＥＱメッセージを送信する。
【０１１７】
プロトコル（スタック）コンポーネント５００は、ＮＴＤＶ＿ＳＴＡＲＴ＿ＲＥＱを受信した際にＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱを送信し、ＮＴＤＶ＿ＳＴＯＰ＿ＲＥＱを受信した際にはＮＥＴ＿ＳＴＯＰ＿ＲＥＱを送信する。
【０１１８】
プログラム９００は、基本的には上記の仕様であるが、“ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ、ＮＥＴ＿ＳＴＯＰ＿ＲＥＱは、交互に送信されなければならない”というプロトコルの仕様が上記の仕様に優先されるものとする。例えば、プログラム９００は、ＳＴＡＲＴボタンが２回押された場合でも、ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱメッセージを続けて２回送信してはならない。
【０１１９】
次に、実施の形態１にかかるコンポーネント生成装置１００のコンポーネント生成処理について図８を用いて説明する。図８は、コンポーネント生成装置１００のコンポーネント生成処理のフローチャートである。
【０１２０】
まず、コンポーネント生成装置１００は、基本情報入力部１０５からコンポーネントの基本情報を入力し、結合部１０６に送る（ステップ１０１）。また、基本情報入力部１０５は、実装を抽出するための情報や、検証結果記述を抽出するための情報や、モデル記述を抽出するための情報を入力し、結合部１０６に送る。なお、基本情報入力部１０５には、ユーザ操作により、これらの情報が入力される。
【０１２１】
次に、結合部１０６は、基本情報、実装を抽出するための情報、検証結果記述を抽出するための情報、モデル記述を抽出するための情報を入力する。次に、結合部１０６は、入力した実装を抽出するための情報に対応する実装を実装格納部１０４から取得する（ステップ１０２）。
【０１２２】
次に、結合部１０６は、入力した検証結果記述を抽出するための情報に対応する検証結果記述を検証結果格納部１０２から取得する（ステップ１０３）。
【０１２３】
次に、結合部１０６は、入力したモデル記述を抽出するための情報に対応するモデル記述をモデル記述格納部１０３から取得する（ステップ１０４）。
【０１２４】
次に、結合部１０６は、取得した、基本情報、実装、検証結果記述、モデル記述をひとつのファイルに結合することにより、図２に示す構成のコンポーネント４００を生成する（ステップ１０５）。そして、結合部１０６は、必要があれば、生成したコンポーネント４００を、伝送部１０７を介してプログラム検証生成装置３００に送信する。
【０１２５】
このようにして、コンポーネント生成装置１００は、検証のために必要な情報である検証結果記述やモデル記述を付与したコンポーネント４００を生成する。
【０１２６】
次に、実施の形態１にかかるプログラム仕様生成装置２００のプログラム仕様生成処理について図９を用いて説明する。図９は、プログラム仕様生成装置２００のプログラム仕様生成処理のフローチャートである。
【０１２７】
まず、プログラム仕様生成装置２００は、基本情報入力部２０４からプログラム仕様の基本情報を入力し、結合部２０５に送る。また、基本情報入力部２０４は、プログラム要求仕様を抽出するための情報や、入出力モデルを抽出するための情報を入力し、結合部２０５に送る。なお、基本情報入力部２０４には、ユーザ操作により、これらの情報が入力される。
【０１２８】
次に、結合部２０５は、プログラム仕様の基本情報、プログラム要求仕様を抽出するための情報、入出力モデルを抽出するための情報を入力する（ステップ２０１）。
【０１２９】
次に、結合部２０５は、プログラム要求仕様を抽出するための情報に対応するプログラム要求仕様をプログラム要求仕様格納部２０２から取得する（ステップ２０２）。次に、結合部２０５は、入出力モデルを抽出するための情報に対応する入出力モデルを入出力モデル格納部２０３から取得する（ステップ２０３）。
【０１３０】
次に、結合部２０６は、取得した、プログラム仕様の基本情報、プログラム要求仕様、入出力モデルをひとつのファイルに結合することにより、図５に示す構成のプログラム仕様７００を生成する（ステップ２０４）。そして、結合部２０５は、必要があれば、生成したプログラム仕様７００を、伝送部２０６を介して、プログラム検証生成装置３００に送信する。
【０１３１】
このようにして、プログラム仕様生成装置２００は、検証のために必要な情報であるプログラム要求仕様や入出力モデルを付与したプログラム仕様７００を生成する。
【０１３２】
次に、プログラム検証生成装置３００のプログラム検証およびプログラム生成処理について図１０を用いて説明する。図１０は、プログラム検証生成装置３００の動作のフローチャートである。
【０１３３】
まず、検証実行部３０４が、プログラム仕様格納部３０２よりプログラム仕様７００を読み出す（ステップ３０１）。次に、検証実行部３０４が、プログラム仕様７００のプログラム要求仕様７０２に基づいて、コンポーネント４００を選択する（ステップ３０２）。続いて、検証実行部３０４は、選択したコンポーネント４００から検証結果記述４０２を読み出す（ステップ３０３）。
【０１３４】
次に、検証実行部３０４は、読み出した検証結果記述４０２と、プログラム仕様７００のプログラム要求仕様７０２の整合性を検査し（整合性確認処理）（ステップ３０４）、整合性がとれた場合には（ステップ３０５）、プログラム生成部３０５にプログラム生成を開始する旨の情報を送る。
【０１３５】
なお、検証実行部３０４の、整合性確認処理の詳細については、後述する。
【０１３６】
以上のように、検証実行部３０４は、コンポーネント４００に記述された検証結果記述４０２がプログラム仕様７００に記述されたプログラム要求仕様７０２を満たすか検証することにより、コンポーネント４００がプログラム仕様７００を満たすか検証する。
【０１３７】
そして、これに対して、プログラム生成部３０５が、コンポーネント４００の実装４０４を結合してプログラム生成を開始する（ステップ３０６）。
【０１３８】
一方、検証結果記述を用いて検査した結果、整合がとれない場合には、検証実行部３０４は、現在検証中のコンポーネント４００に、既に検証済みのコンポーネント４００の検証結果記述４０２と矛盾する検証結果記述４０２が存在するかを確認する（ステップ３０７）。ここでいう矛盾する検証結果記述４０２とは、既に検証済みのコンポーネント４００の検証結果記述４０２が成り立つ場合に、同時には、絶対成り立たない検証結果記述４０２のことである。
【０１３９】
そして、検証中のコンポーネント４００に矛盾する検証結果記述４０２が存在する場合には、検証中のコンポーネント４００はプログラム要求仕様７００を満たさないことになるので、他のコンポーネント４００を検索し（ステップ３０８）、他のコンポーネント４００が存在する場合には（ステップ３０９）、ステップ３０３に戻る。
【０１４０】
一方、検証中のコンポーネント４００に矛盾する検証結果記述４０２が存在しない場合には、単にプログラム要求仕様７００に対応する検証結果記述４０２がない場合が考えられ、検証結果記述４０２を用いた検証だけでは、不十分な可能性がある。よって、検証実行部３０４は、検証器を用いた検証に移行する。
【０１４１】
まず、検証実行部３０４は、コンポーネント４００からモデル記述４０３を読み出す。次に、検証実行部３０４は、プログラム仕様７００から入出力モデル７０３を読み出す（ステップ３１０）。
【０１４２】
次に、モデル記述４０３はＰｒｏｍｅｌａで記述されているため、検証実行部３０４は、モデル記述４０３を入出力モデル７０３に従って結合し、コンポーネント４００の起動記述（ｉｎｉｔ関数およびｒｕｎステートメントの記述）とメッセージ定義を追加することにより、検証器（ＳＰＩＮ）で検証可能なデータを生成する。そして、検証実行部３０４は、検証器を用いて、生成した検証可能なデータを検証し、検証結果がプログラム仕様７００のプログラム要求仕様７０２を満たすか否かを検証する（ステップ３１１）。
【０１４３】
ステップ３１１において、検証結果がプログラム要求仕様７０２を満たさないと検証した場合には（ステップ３１２）、検証実行部３０４は、検証中のコンポーネント４００がプログラム仕様７００を満たさないと最終的に判断し、ステップ３０８に移行し、他のコンポーネント４００に対する検証を行う。
【０１４４】
一方、検証結果がプログラム要求仕様７０２を満たすと検証した場合には（ステップ３１２）、検証実行部３０４は、プログラム生成部３０５において、プログラム生成を行って（ステップ３０６）、プログラム生成されたプログラムを格納する（ステップ３１３）。
【０１４５】
以上のように、検証実行部３０４は、コンポーネント４００のモデル記述４０３およびプログラム仕様７００の入出力モデル７０３を用いることで、検証器を用いた検証を行う。
【０１４６】
また、モデル記述４０３には、コンポーネント４００の入出力部分における全ての動作を抽象化した記述がなされている。よって、検証器を用いた検証により、コンポーネント４００の入出力部分に関する仕様が、プログラム仕様７００を満たすか確実に検証できる。つまり、検証器を用いた検証により、検証記述結果４０２により検証できなかった動作に関しても確実に検証できる。
【０１４７】
次に、プログラム検証生成装置３００の整合性確認処理（ステップ３０４の処理）について、図１１を用いて詳細に説明する。図１１は、プログラム検証生成装置３００の整合性確認処理のフローチャートである。
【０１４８】
まず、プログラム検証生成装置３００の検証実行部３０４は、事前条件のない事後条件を全てのコンポーネント４００から検索する（ステップ４０１）。ここで、検証実行部３０４は、検索により発見された事後条件をＰ［ｉ］（１＜＝ｉ＜＝Ｎ）に格納する。
【０１４９】
続いて、検証実行部３０４は、全てのＰ［ｉ］に対して、整合性確認処理を行う。
【０１５０】
まず、検証実行部３０４は、変数ｉに０を代入する（ステップ４０２）。次に、検証実行部３０４は、変数ｉを１インクリメントする（ステップ４０３）。
【０１５１】
次に、検証実行部３０４は、現在の変数ｉがＮ以下であるか、つまり、全てのＰ［ｉ］に対して処理が終わったか判断する（ステップ４０４）。
【０１５２】
次に、検証実行部３０４は、Ｐ［ｉ］を引数として整合性調査処理を呼び出す（ステップ４０５）。
【０１５３】
なお、検証実行部３０４の整合性調査処理の詳細については、後述する。
【０１５４】
検証実行部３０４は、整合性調査処理の結果として、要求仕様を全て満たした（整合性がとれた）か、否かを示す返り値を返す。
【０１５５】
そして、検証実行部３０４は、整合性がとれた場合には（ステップ４０６）、処理終了する。一方、検証実行部３０４は、整合性がとれていない場合には、ステップ４０３に移行し、次の事後条件を選択して（ステップ４０３）、再度整合性調査処理を行う（ステップ４０５）。
【０１５６】
そして、検証実行部３０４は、全ての事後条件Ｐ［ｉ］を用いても整合性がとれなかった場合には（ステップ４０６）、プログラムを生成せずに処理を終了する。
【０１５７】
次に、プログラム検証生成装置３００の整合性調査処理（ステップ４０５）について図１２を用いて詳細に説明する。図１２は、プログラム検証生成装置３００の整合性調査処理のフローチャートである。
【０１５８】
まず、検証実行部３０４が、引数として渡された事後条件と、プログラム仕様７００のプログラム要求仕様７０２が一致するかどうかを検証し、一致する場合には一致したプログラム要求仕様７０２にマークをする（ステップ５０１）。
【０１５９】
次に、マークされていないプログラム要求仕様７０２がない場合には（ステップ５０２）、検証実行部３０４は、プログラム要求仕様７０２を満たしたものとして、整合性がとれたという返り値を返して処理を終了する（ステップ５０３）。
【０１６０】
一方、マークされていないプログラム要求仕様７０２が存在する場合には、検証実行部３０４は、引数として渡された事後条件Ｐ［ｉ］を持つコンポーネント４００と接続されているコンポーネント４００を検索し、検索されたコンポーネント４００ごとに以下の処理を行う（検索により発見されたコンポーネント４００をＣ［ｊ］（１＜＝ｊ＜＝Ｍ）とする）（ステップ５０４）。
【０１６１】
まず、検証実行部３０４は、変数ｊに０を代入する（ステップ５０５）。次に、検証実行部３０４は、変数ｊを１インクリメントする（ステップ５０６）。
【０１６２】
次に、検証実行部３０４は、現在の変数ｊがＭ以下であるか、つまり、全てのＣ［ｊ］に対して処理が終わったか判断する（ステップ５０７）。
【０１６３】
次に、検証実行部３０４は、コンポーネントＣ［ｊ］中の事前条件を調べ、事後条件Ｐ［ｉ］と一致する事前条件をマークする（ステップ５０８）。
【０１６４】
続いて、検証実行部３０４は、コンポーネントＣ［ｊ］中の事後条件Ｐ［ｉ］を調べ、Ｃ［ｊ］に対応する事前条件Ｐ［ｉ］が全てマークされているものを検索する（検索された事後条件をＰ’［ｋ］（１＜＝ｋ＜＝Ｌ）とする）（ステップ５０９）。
【０１６５】
次に、検証実行部３０４は、発見された事後条件Ｐ’［ｋ］ごとに以下の処理を行う。検証実行部３０４は、以下の処理を行って、整合性がとれておらず、かつｊ＜Ｍであれば、ステップ５０８以降の処理を繰り返す。
【０１６６】
まず、検証実行部３０４は、変数ｋに０を代入する（ステップ５１０）。次に、検証実行部３０４は、変数ｋを１インクリメントする（ステップ５１１）。
【０１６７】
次に、検証実行部３０４は、現在の変数ｋがＬ以下であるか、つまり、全てのＰ’［ｋ］に対して処理が終わったか判断する（ステップ５１２）。
【０１６８】
次に、検証実行部３０４は、事後条件Ｐ’［ｋ］を引数として整合調査処理の再帰呼び出しを行う（ステップ５１３）。
【０１６９】
再帰呼び出しの結果、返り値として整合性がとれたという結果を受信すれば（ステップ５１４）、検証実行部３０４は、整合性がとれたことを返り値として返して処理を終了し（ステップ５１５）、整合性がとれておらず、かつｋ＜Ｌであればステップ５１１以降を繰り返す。
【０１７０】
このように、検証実行部３０４は、全ての成立する事後条件を洗い出し、要求仕様を満たすかどうかを検証することができる。
【０１７１】
以上のように、検証実行部３０４は、コンポーネント４００に記述された検証結果記述４０２と、プログラム仕様７００に記述されたプログラム要求仕様７０２とを比較することにより、コンポーネント４００がプログラム仕様７００を満たすか検証できる。
【０１７２】
また、検証結果記述は、コンポーネント４００の代表的な動作に対する検証を行ったものであり、コンポーネント４００の全ての動作に対して検証を行ったものではない。よって、検証結果記述を用いて検証することにより、代表的な動作がプログラム仕様を満たすか検証できる。つまり、検証結果記述を用いた検証を行うことにより、処理コストの少ない検証を行うことができる。
【０１７３】
次に、図３、図４、図６において説明した例に対する、プログラム検証生成装置３００のプログラム検証について説明する。
【０１７４】
まず、検証実行部３０４は、プログラム仕様格納部３０２からプログラム仕様８００を取得し（ステップ３０１）、プログラム仕様８００に記述されているコンポーネント５００、６００をコンポーネント格納部３０３から取得する（ステップ３０２）。次に、検証実行部３０４は、コンポーネント５００、６００から検証結果記述５０２、６０２を取得する（ステップ３０３）。
【０１７５】
次に、検証実行部３０４は、プログラム要求仕様８００中のＶｅｒｉｆ−Ｒｕｌｅ：８０６に記載される“ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ−＞！ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ  Ｕ  ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ”と“ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ−＞！ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ  Ｕ  ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ”が成り立つかどうかを検証することになる（ステップ３０４）。以下に動作を示す。
【０１７６】
なお、以下の見出しに付与される数字（たとえば、“Ａ−０”の”−０“の部分）は、整合性調査処理の再帰呼び出しの深さを示している。すなわち、整合性調査処理が呼び出されると、インクリメントされ、呼び出しから復帰すると、デクリメントされる。
【０１７７】
Ａ−０）まず、検証実行部３０４は、図３、図４に記すコンポーネント５００、６００において、事前条件のない事後条件を検索する（ステップ４０１）。事前条件のない事後条件は、ＧＵＩコンポーネント６００の“ＮＴＤＶ＿ＳＴＡＲＴ＿ＲＥＱ−＞！ＮＴＤＶ＿ＳＴＡＲＴ＿ＲＥＱ  Ｕ  ＮＴＤＶ＿ＳＴＯＰ＿ＲＥＱ”のみである。よって、検証結果実行部３０４は、これを引数として整合性調査処理を呼び出す（ステップ４０５）。
【０１７８】
Ｂ−１）続いて、検証実行部３０４は、上記の事後条件と一致するプログラム仕様８００のプログラム要求仕様８０２を検索する（ステップ５０１）。しかし、一致するプログラム要求仕様８０２は存在しない。
【０１７９】
よって、検証実行部３０４は、マークされていない要求仕様があるので（ステップ５０２）、終了せずに次の処理へ進む。
【０１８０】
Ｃ−１）続いて、検証実行部３０４は、ＧＵＩコンポーネント６００と呼び出し関係のあるプロトコル（スタック）コンポーネント５００の事前条件を調べると（ステップ５０３）、“１：”の事前条件と一致することがわかるので、“１：”の事前条件にマークする（ステップ５０８）。
【０１８１】
Ｄ−１）続いて、検証実行部３０４は、プロトコル（スタック）コンポーネント５００の事後条件のうち、対応する事前条件がマークされているものを検索する（ステップ５０９）。発見されるのは、“ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ−＞！ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ  Ｕ  ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ”であるので、検証実行部３０４は、これを引数として整合性調査処理を呼び出す（ステップ５１３）。
【０１８２】
Ｅ−２）Ｄ−１）で指定された事後条件（“ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ−＞！ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ  Ｕ  ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ”）をプログラム要求仕様８０２と比較すると、一致するプログラム要求仕様８０２があるので、検証実行部３０４は、そのプログラム要求仕様８０２をマークする（ステップ５０１）。まだマークされていない要求仕様があるので（ステップ５０２）、検証実行部３０４は、処理を終了せず次の処理に進む。
【０１８３】
Ｆ−２）次に、検証実行部３０４は、プロトコル（スタック）コンポーネント５００と接続関係のあるコンポーネントを検索すると、発見されるのはＧＵＩコンポーネント６００のみである（ステップ５０４）。よって、検証実行部３０４は、ＧＵＩコンポーネント６００の事前条件をチェックするが、事前条件がないので事前条件はマークしない（ステップ５０８）。次に、マークされた事前条件がないので、Ｌ＝０となり、検証実行部３０４は、ステップ５１３を呼び出さない。
【０１８４】
また、他にプロトコル（スタック）コンポーネント５００と接続する他のコンポーネントは存在しないので、検証実行部３０４は、整合性がとれていないという返り値とともに処理を終了する（ステップ５１６）。
【０１８５】
Ｇ−１）次に、検証実行部３０４は、呼び出し元（ステップ５１３）に戻って処理を続けるが、マークされない要求仕様が残るため（“ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ−＞！ＮＥＴ＿ＳＴＯＰ＿ＲＥＱ  Ｕ  ＮＥＴ＿ＳＴＡＲＴ＿ＲＥＱ“が残る）、整合性がとれないという返り値とともに整合性調査処理を終了する（ステップ５１６）。
【０１８６】
Ｈ−０）次に、検証実行部３０４は、ステップ４０２に戻るが、整合性がとれていないため（ステップ４０６）、プログラムは生成されずに処理を終了する。
【０１８７】
このように、この例では、予めコンポーネント制作者によって用意された検証結果記述を用いた整合性確認動作では、整合性が確認できない（ステップ３０５）。
【０１８８】
また、矛盾する検証結果記述も無いので（ステップ３０７）、次に、検証実行部３０４の検証器による検証を行うことになることになる。
【０１８９】
まず、検証実行部３０４は、コンポーネント５００、６００に記述されたモデル記述５０３、６０３と、プログラム仕様８００に記述された入出力モデル８０３を取得する（ステップ３１０）。
【０１９０】
次に、検証実行部３０４は、コンポーネント５００、６００のモデル記述５０３、６０３を、プログラム仕様８００の入出力モデル８０３に従って結合して、各コンポーネントの起動記述（ｉｎｉｔ関数およびｒｕｎステートメントの記述）とメッセージ定義を追加することにより、検証器（ＳＰＩＮ）で検証可能なデータを生成する。そして、検証実行部３０４は、検証器を用いて、生成した検証可能なデータを検証した検証結果が、プログラム仕様８００のプログラム要求仕様８０２を満たすか否かを判断する（ステップ３１１）。
【０１９１】
この検証を行った結果、検証結果が、プログラム仕様８００のプログラム要求仕様８０２を満たすことが確認された場合には（ステップ３１２）、検証実行部３０４は、プログラム生成部３０５にプログラムの生成指示を送信する。そして、プログラム生成部３０５がコンポーネント４００の実装４０４をプログラム仕様７００に基づいて結合することにより、プログラムを生成し（ステップ３０６）、プログラム格納部３０６に格納する（ステップ３１３）。
【０１９２】
一方、検証結果が、プログラム仕様８００のプログラム要求仕様８０２を満たさないことが確認できない場合には（ステップ３１２）、検証実行部３０４は、他のコンポーネントを検索して（ステップ３０８、３０９）、もう一度検証作業を行う（ステップ３０３、３０４）。
【０１９３】
以上説明したように、実施の形態１によれば、コンポーネントに検証結果記述やモデル記述をし、プログラム仕様にプログラム要求仕様や入出力モデルを記述することにより、コンポーネントを結合して実際にプログラムを生成しなくても、検証結果記述、モデル記述、プログラム要求仕様、および入出力モデルを用いることによりプログラムの動作の検証をできる。つまり、コンポーネントを結合してプログラムを生成する装置であるプログラム検証生成装置３００において、実際にコンポーネント結合してプログラム生成し、生成したプログラムを動作させなくてもプログラムの動作の正当性を検証できる。
【０１９４】
また、実施の形態１によれば、まず、整合性確認により、コンポーネントがプログラム仕様を満たすかどうかを検証し、必要なら、次に、検証器を用いた検証により、コンポーネントがプログラム仕様を満たすかどうかを検証するという、２段階の検証ができる。これにより、まず、処理コストの軽い整合性確認により、検証を行い、必要があれば、次に、確実性の高い検証器を用いた検証により検証を行うことができる。この結果、検証を、高速に、かつ確実に行うことができる。
【０１９５】
実施の形態１によれば、プログラム全体で満たせばよいプログラム要求仕様を、予め決まったコンポーネントに割り振る必要がなくなる。つまり、プログラム要求仕様を異なるコンポーネントに振り分けることができる。例えば、プログラム要求がＡ，Ｂ，Ｃという内容である場合に、Ａを満たすコンポーネントとＢを満たすコンポーネントとＣを満たすコンポーネントを用いてプログラムを生成しても良いし、ＡとＢを満たすコンポーネントとＣを満たすコンポーネントを用いてプログラムを生成しても良い。つまり、多くの実装を持つ高価なコンポーネントを用いても、少ない実装を持つ安価なコンポーネントを多く用いプログラムを生成しても良い。このように、プログラム要求仕様をどのコンポーネントにより満足させるか予め決めなくて良いので、コンポーネントの設計、実装の自由度を向上することができる。
【０１９６】
なお、コンポーネント生成装置１００、プログラム仕様生成装置２００、プログラム検証生成装置３００の動作をプログラムにし、記憶媒体に格納し、汎用のコンピュータが記憶媒体からプログラムをダウンロードして実行する形態であっても良い。
【０１９７】
（実施の形態２）
続いて、本発明の実施の形態２について説明する。実施の形態２におけるプログラム検証生成装置は、プログラムの実行部を保有し、プログラムを動作させることができる。また、実施の形態２におけるプログラム検証生成装置は、データ伝送可能な伝送路に接続しており、動作させているプログラムを構成するコンポーネントに更新があったことを知らせる変更通知を伝送路から受信し、変更通知に基づいてコンポーネントを取得、蓄積し、検証、プログラム合成を行って現在動作しているプログラムを新しいプログラムと入れ替える。
【０１９８】
以下、実施の形態２にかかるプログラム検証生成装置について、図１３を用いて具体的に説明する。図１３は、実施の形態２にかかるプログラム検証生成装置を示す図である。
【０１９９】
図１３のプログラム検証生成装置１３００は、図１のプログラム検証生成装置３００に、変更通知受信部１００１、コンポーネント取得部１００２、プログラム実行部１００３を追加したものである。
【０２００】
変更通知受信部１００１は、伝送路４００より変更通知を受信して、変更通知に基づいて、コンポーネント取得部１００２に更新されたプログラムを取得するよう指示する手段である。
【０２０１】
なお、変更通知はコンポーネントを開発した開発元（コンポーネント生成装置１００）、もしくはプログラム仕様を配布した配布元（プログラム仕様生成装置２００）より送信される。
【０２０２】
変更通知には、更新されたコンポーネントの名前、バージョン番号、更新されたコンポーネントの取得先を示す情報（ＵＲＬなど）が含まれている。
【０２０３】
コンポーネント取得部１００２は、伝送路に接続し、変更通知受信部１００１のコンポーネント取得指示に基づいて、更新されたコンポーネントを取得してコンポーネント格納部３０３に保存する手段である。
【０２０４】
プログラム実行部１００３は、生成されたプログラムを実行する手段である。また、プログラムが更新された際には、現行プログラムを終了して新しいプログラムを実行する。
【０２０５】
なお、現行プログラムの終了、新しいプログラムの実行のタイミングは端末の電源ＯＮ／ＯＦＦ時や再起動時、プログラムの終了、起動時であってもよい。
【０２０６】
次に、プログラム検証生成装置１３００の動作について説明する。
【０２０７】
まず、プログラム検証生成装置１３００は、変更通知受信部１００１において、動作させているプログラムを構成するコンポーネントに更新があったことを知らせる変更通知を受信する。
【０２０８】
次に、プログラム検証生成装置１３００は、コンポーネント取得部１００２において、変更通知に基づいて新たなコンポーネントを取得し、コンポ−ネント格納部３０３に蓄積する。
【０２０９】
次に、プログラム検証生成装置１３００は、検証実行部３０４において、プログラム仕様格納部３０２に蓄積されているプログラム仕様に、コンポーネント格納部３０３に新たに蓄積したコンポ−ネントが適合するか検証する。
【０２１０】
なお、検証実行部３０４の検証処理は、実施の形態１と同様なので詳細な説明を省略する。
【０２１１】
次に、プログラム検証生成装置１３００は、プログラム生成部３０５において、プログラム合成を行って新たなプログラムを生成する。
【０２１２】
次に、プログラム検証生成装置１３００は、プログラム格納部３０６に蓄積されている、現在動作しているプログラムを新しいプログラムと入れ替える。
【０２１３】
そして、プログラム検証生成装置１３００は、プログラム実行部１００３において、新しいプログラムを実行する。
【０２１４】
以上説明したように、実施の形態２によれば、変更通知に基づいてコンポーネントを取得、蓄積し、検証、プログラム合成を行って現在動作しているプログラムを新しいプログラムと入れ替えることができる。この結果、今まで正常に動作していたプログラムが、コンポーネントの更新により動作しなくなるという課題を解決することができる。
【０２１５】
【発明の効果】
以上説明したように、本発明によれば、コンポーネントに記述されている検証情報とプログラム仕様とを比較することにより、コンポーネント結合後に実際にプログラムを動作させる前に、プログラムの検証を行うことができるようになる。
【図面の簡単な説明】
【図１】本発明の実施の形態１にかかるプログラム検証生成システムの構成を説明する図
【図２】実施の形態１にかかるコンポーネントのフォーマットを示す図
【図３】実施の形態１にかかるコンポーネントの記述の例を説明するための図
【図４】実施の形態１にかかるコンポーネントのその他の記述例を説明する図
【図５】実施の形態１にかかるプログラム仕様のフォーマットを示す図
【図６】実施の形態１にかかるプログラム仕様の記述例を示す図
【図７】実施の形態１にかかるプログラムの記述例を示す図
【図８】実施の形態１にかかるコンポーネント生成装置のコンポーネント生成処理のフローチャート
【図９】実施の形態１にかかるプログラム仕様生成装置のプログラム仕様生成処理のフローチャート
【図１０】実施の形態１にかかるプログラム検証生成装置の動作のフローチャート
【図１１】実施の形態１にかかるプログラム検証生成装置の整合性確認のフローチャート
【図１２】実施の形態１にかかるプログラム検証生成装置の整合性調査処理のフローチャート
【図１３】本発明の実施の形態２にかかるプログラム検証生成装置を示す図
【符号の説明】
１０  プログラム検証生成システム
１００  コンポーネント生成装置
１０１  コンポーネント情報格納部
１０２  検証結果記述格納部
１０３  モデル記述格納部
１０４  実装格納部
１０５、２０４  基本情報入力部
１０６、２０５  結合部
１０７、２０６、３０１  伝送部
２００  プログラム仕様生成部
２０１  プログラム仕様情報格納部
２０２  プログラム要求仕様格納部
２０３  入出力モデル格納部
３００  プログラム検証生成装置
３０２  プログラム仕様格納部
３０３  コンポーネント格納部
３０４  検証実行部
３０５  プログラム生成部
３０６  プログラム格納部
１００１  変更通知受信部
１００２  コンポーネント取得部
１００３  プログラム実行部
【図１】
2004326366.tif 000003
【図２】
2004326366.tif 000004
【図３】
2004326366.tif 000005
【図４】
2004326366.tif 000006
【図５】
2004326366.tif 000007
【図６】
2004326366.tif 000008
【図７】
2004326366.tif 000009
【図８】
2004326366.tif 000010
【図９】
2004326366.tif 000011
【図１０】
2004326366.tif 000012
【図１１】
2004326366.tif 000013
【図１２】
2004326366.tif 000014
【図１３】
2004326366.tif 000015