外部機器から情報を取得する外部情報取得手段と、プログラムを実行する演算処理装置と、を有し、前記外部情報取得手段が取得した情報をもとに演算を行う演算プログラムと、要求仕様を仕様記述言語で記述した形式仕様記述から生成された監視プログラムと、が、前記演算処理装置上で実行され、前記演算プログラムは、演算に伴う状態の変化を前記監視プログラムに通知し、前記監視プログラムは、前記演算プログラムからの通知をトリガとして、前記演算プログラムの処理が、要求仕様の定義に従っているか否かを検証することを特徴とする、自己診断機能を備えたコンピュータ。プログラムの監視を行うための監視プログラムと、監視対象のプログラムである演算プログラムと、を生成可能なソフトウェア作成装置であって、該ソフトウェア作成装置は、プログラムの動作をモデル記述言語で記述したモデル情報から、演算プログラムを生成する演算プログラム生成手段と、要求仕様を仕様記述言語で記述した形式仕様記述から監視プログラムを生成する監視プログラム生成手段と、前記演算プログラムと、監視プログラムを実行用コンピュータに記録するプログラム書き込み手段と、を有し、前記演算プログラムは、演算に伴う状態の変化を前記監視プログラムに通知し、前記監視プログラムは、前記演算プログラムからの通知をトリガとして、前記演算プログラムの処理上に、要求仕様に定義されていない状態が発生していないか検証可能であることを特徴とする、ソフトウェア作成装置。利用者が監視に用いる形式仕様記述を選択するための選択手段をさらに有し、前記監視プログラム生成手段は、前記形式仕様記述から前記監視プログラムを生成する際、選択された前記形式仕様記述を用いて前記監視プログラムを生成することを特徴とする、請求項2に記載のソフトウェア作成装置。プログラムの監視を行うための監視プログラムを生成する監視プログラム生成手段と、監視対象のプログラムである演算プログラムを生成する演算プログラム生成手段と、を有するソフトウェア作成装置が行うソフトウェア作成方法であって、演算に伴う状態の変化を前記監視プログラムに通知する前記演算プログラムを、プログラムの動作をモデル記述言語で記述したモデル情報から生成するステップと、前記演算プログラムからの通知をトリガとして、前記演算プログラムの処理が要求仕様に従っているか否かを検証する前記監視プログラムを、要求仕様を仕様記述言語で記述した形式仕様記述から生成するステップと、を含むことを特徴とする、ソフトウェア作成方法。前述の自己診断機能は、車載コンピュータに接続されたセンサが正常に動作していることや、車載コンピュータの処理が正常に行えていることを、専用に設計されたプログラムが監視する。しかし、コストの問題により、車載コンピュータが有する全ての機能を監視することは一般的ではなく、監視できない機能が少なからず存在するという問題がある。また、設計段階で、自己診断機能のプログラム自体にバグが混入する恐れがあるため、従来技術では、車載コンピュータの完全な自己診断を行うことができないという問題がある。本発明は上記の問題点を考慮してなされたものであり、実行されるプログラムが要求仕様に従っているか効率よく監視を行うことができる、自己診断機能を備えたコンピュータ、ソフトウェア作成方法、およびソフトウェア作成装置を提供することを目的とする。本発明に係る自己診断機能を備えたコンピュータ、ソフトウェア作成方法、およびソフトウェア作成装置では、上記目的を以下の手段により実現する。組込みソフトウェアの開発においては、モデルベース開発、および形式手法が用いられる場合がある。モデルベース開発とは、統一モデリング言語等のモデル記述言語によって、コンピュータ上にソフトウェアの仕様を表現した仮想的なモデルソフトウェアモデルを作り、モデルを検証しながら開発プロセスを進めるという開発手法である。また、形式手法とは、ソフトウェア開発における要求、仕様、設計の各段階を、論理的な矛盾がないように数学的に検証する手法のことである。開発に形式手法を用いた場合、ソフトウェアが行うべき論理的な振る舞いである要求仕様を、形式仕様記述と呼ばれる数式で記述しておき、これをソフトウェアの検証に用いる。以降、形式仕様記述で表されたソフトウェア仕様のことを、形式仕様と称する。本発明では、この形式仕様から、プログラムを監視するためのソフトウェアモデルを自動生成する。また、生成したソフトウェアモデルからプログラムを自動生成して、監視対象のプログラムと同時に実行し監視させることで、任意の機能についての正確な自己診断機能を実現する。本発明に係るコンピュータは、外部に接続されたセンサやスイッチ等から情報を取得する外部情報取得手段と、プログラムが実行される演算処理装置と、を有し、前記情報取得手段が取得した情報をもとに演算を行う演算プログラムと、仕様記述言語で記述された形式仕様記述から生成した監視プログラムと、が、前記演算処理装置上で実行され、前記演算プログラムは、演算に伴う状態の変化を前記監視プログラムに通知し、前記監視プログラムは、前記演算プログラムからの通知をトリガとして、前記演算プログラムの処理上に、要求仕様に定義されていない状態が発生していないか検証することを特徴とする。組み込みソフトウェア開発において、モデルと形式手法を用いる場合、開発者は形式仕様を満たすようにソフトウェアモデルを設計し、ソフトウェアモデルから実行コードを生成する。そこで本発明では、形式仕様記述を、監視対象のソフトウェアモデルと同等のモデルに変換して監視プログラムを生成し、監視の用途に用いる。この監視を行うプログラムは、数理的に正しい形式仕様記述から自動生成されるため、ソフトウェアの実行結果が仕様通りであるかを判断することができる。これにより、開発者が自己診断機能のコーディングを行った場合と比較して、人為的なバグが混入する可能性が無くなるという利点がある。また、本発明に係るソフトウェア作成装置は、プログラムの監視を行うための監視プログラムと、監視対象のプログラムである演算プログラムと、を生成可能なソフトウェア作成装置であって、該ソフトウェア作成装置は、プログラムの動作をモデル記述言語で記述したモデル情報から、演算プログラムを生成する演算プログラム生成手段と、仕様記述言語で記述された形式仕様記述から監視プログラムを生成する監視プログラム生成手段と、前記演算プログラムと、監視プログラムを実行用コンピュータに記録するプログラム書き込み手段と、を有し、前記演算プログラムは、演算に伴う状態の変化を前記監視プログラムに通知し、前記監視プログラムは、前記演算プログラムからの通知をトリガとして、前記演算プログラムの処理上に、要求仕様に定義されていない状態が発生していないか検証可能であることを特徴とする。このように構成することにより、前記自己診断機能を持つプログラムを作成し、実行用コンピュータに書き込むことができるソフトウェア作成装置を提供することができる。また、前記ソフトウェア作成装置においては、前記形式仕様記述から前記監視プログラムを生成する際、監視に用いる形式仕様記述を選択できることを特徴としてもよい。本発明における自己診断機能を備えたコンピュータは、監視対象のプログラムが持っている全ての機能に対して監視を実行すると、オーバーヘッドが大きくなり、オーバーヘッドを減らすと監視できる機能が少なくなるという問題がある。そこで、ソフトウェア作成装置が監視プログラムを生成する際に、監視に用いる形式仕様記述を選択可能にすることで、この問題に対応することができる。本発明によれば、実行されるプログラムが要求仕様に従っているか効率よく監視を行うことができる、自己診断機能を備えたコンピュータ、ソフトウェア作成装置、およびソフトウェア作成方法を提供することができる。形式手法を用いてソフトウェアの開発を行う場合、ソフトウェアが満たすべき要求を記述した形式仕様記述が、ソフトウェアの最も基本的な設計図となる。通常、形式仕様は、LTLLinearTemporalLogic、CTLComputationalTreeLogic等の仕様記述言語にて記述される。また、形式手法を取り入れたモデルベース開発を行う場合、開発者が、MATLAB登録商標、Simulink登録商標等の開発ツール以降、開発環境と称するを用いて、形式仕様を満たすソフトウェアモデルを作成する。作成したソフトウェアモデルに誤りがないことを検証するためには、モデルベーステストが用いられる。モデルベーステストとは、必要なテストをモデルレベルで実施するものであり、例えば、事前にテスト対象のパスを定義した試験用モデルを作成して、開発対象のモデルと対比させる方法や、実行結果を形式仕様と対比させて正しいことを確認していく方法など、いくつかの手法がある。これらの手法の一つに、テスト対象のプログラムを監視するオブザーバモデルを作成する方法がある。オブザーバモデルとは、監視対象プログラムの入出力状態や変数などが、仕様通りとなっているか検証するための監視プログラムをモデルで表したものである。監視対象のプログラムは、この監視プログラムに対して、入出力状態や変数の更新といった状態変化のイベントを通知し、これを受けた監視プログラムが、当該状態変化が正しいか確認を行う。開発環境は、実環境を模した仮想環境であるため、監視対象のソフトウェアモデルから、監視対象プログラムをエミュレートすることができ、オブザーバモデルから、監視プログラムをエミュレートすることができる。そのため、開発環境において、モデル同士を組み合わせることで、監視対象プログラムの動作をテストすることができる。一方、非特許文献1には、仕様記述言語であるLTLにて記述された形式仕様を、有限オートマトンに変換する技術が開示されている。開発環境は、オートマトンで記述された情報を取り込み、モデル化することができるため、ソフトウェアの振る舞いが記録されている形式仕様をモデルに変換し、開発環境に組み込むことができる。これにより、前記オブザーバモデルを作成した場合と同等の効果が得られる。形式仕様は、全ての要求仕様が定義されているため、プログラムがある実行経路を辿った場合、それが仕様に定義されているものであるかを確認することができる。検証が済んだソフトウェアモデルからは、非特許文献2および非特許文献3の技術を用いることにより、プログラム言語で記述されたコードを生成することができる。このコードをマイコンや車載コンピュータなどに書き込むことにより、実際の製品が作られる。通常、ソフトウェアの開発工程においては、テストを実施した後は、試験用のモデルを除去したうえでコードを生成する。一方、本発明においては、設計したソフトウェアモデルと、形式仕様から生成したオブザーバモデルを組み合わせた状態のままでコードの生成を行う。開発環境上では、事前に想定された実行経路しか検証をすることができないが、ソフトウェアモデルと、形式仕様から生成したモデルを組み合わせた状態でコードを生成し、車載コンピュータなどの実環境に移すことで、プログラムが取り得る全ての実行経路について検証を行うことができるようになる。以降、形式仕様から生成したオブザーバモデルからコードを出力して、実行形式にしたものをランタイムオブザーバと称する。出力されたランタイムオブザーバは、監視対象である演算プログラムと同時に実行され、演算に伴う状態の変化、つまり演算プログラムが有している変数や、入出力状態の変化を検出し、処理が仕様の定義に従っているかチェックを行う。万一、仕様に従っていない動作を検出した場合は、その旨を運転者に通知するとともに、詳細な情報を記録し、もしくは外部に送信することができる。必要があれば、システムの運用モードを変更、もしくは停止させることによって安全を担保してもよい。第1の実施形態第1の実施形態に係るコンピュータ、またはソフトウェア作成装置について、図1と図2を用いて詳細な説明をする。図1は、ソフトウェア作成装置におけるオブザーバモデルとシステムモデルとの関係を表す図であり、図2は、本発明におけるソフトウェア作成装置の構成を表した図である。形式仕様11が、仕様記述言語で記述されたソフトウェアの要求仕様である。形式仕様には、ソフトウェアが満たすべき振る舞いが記録されており、たとえば出力がオフの状態でスイッチを押したら必ずオンに遷移する。出力がオンの状態でスイッチを押したら必ずオフに遷移するといった記述がされている。形式仕様11は、要求仕様記憶部51に記録されており、開発者はこの仕様を元に実際のソフトウェアモデルである全体システムモデル13をソフトウェアモデル作成部53にて作成する。オブザーバモデル12は、非特許文献1の技術により、形式仕様11を有限オートマトンに変換したものである。変換はオブザーバモデル生成部52によって実行される。オブザーバモデル12は、開発環境に直接導入できる形式となっている。形式仕様11から変換されたオブザーバモデル12には、全ての要求仕様が定義されているため、オブザーバモデル12を用いることによって、たとえば出力がオフの状態でスイッチを押した結果、状態がオフであれば異常といった判断をすることができる。一方で、全体システムモデル13の一部を構成するシステムモデル14も同様に、有限オートマトンで表現できるソフトウェアモデルである。これは、開発者が実装を行ったものであり、数理的定義であるオブザーバモデル12とは異なり、開発対象のシステムの処理や挙動が詳細に記録されている。たとえば変数Xが0の状態で外部入力Aから信号が入力されたら、外部出力Bから出力を行い、変数Xを1にするといったように、仕様を実現するための具体的手段が記録されたものである。開発環境では、システムモデル14と、オブザーバモデル12の双方の動作をエミュレートし、外部との入出力、たとえばエンジンの挙動をソフトウェアでシミュレートすることで、監視対象プログラムが仕様通りに動作することをモデルレベルで検証することが可能である。モデルの検証は、モデル検証部54にて行うことができる。通常の開発においては、システムモデル14に係る機能を生成しようとした場合、システムモデル14のみからコードを生成するが、本実施形態では、システムモデル14と、オブザーバモデル12を組み合わせた状態のまま、コードの出力を行う。両者を組み合わせたモデルを、オブザーバ連結モデル10と称する。オブザーバ連結モデル10は、開発環境における通常のソフトウェアモデルであるため、非特許文献2および非特許文献3に記載の技術により、C言語やハードウェア記述言語などのプログラム17に変換することができる。コードの出力はコード生成部55が行い、ソフトウェアモデルを入力すると、出力としてソースコードを得ることができる。図3は、開発環境によって生成されたプログラムの構成を表す図である。システムモデル14からは、演算プログラムである監視対象システム15が、オブザーバモデル12からは、監視プログラムであるランタイムオブザーバ16が生成される。なお、監視対象システム15と、ランタイムオブザーバ16は、同時に実行するという条件を満たせば、一つのモジュールに格納されていてもよいし、複数のモジュールに分かれていてもよい。また、一つのプロセスであってもよいし、複数のプロセスに分かれて実行されてもよい。出力されたコードは、コード書込部56にて、実環境で動作するコンピュータが有する記憶装置37ROMに書き込まれる。本発明を車載コンピュータに適用する場合、実環境で動作するコンピュータとは主にエレクトロニックコントロールユニットECUを指す。本実施形態では、車載コンピュータを例に説明する。図4は、第1の実施形態に係るソフトウェア開発手順を表したフロー図である。開発者は、形式仕様をオブザーバモデルに変換しS10、形式仕様を元にソフトウェアモデルを設計するS11。ステップS10とステップS11の手順は、どちらかを先に行ってもよいし、並列して行ってもよい。作成されたモデルは検証S12されたのち、プログラムコードに変換されるS13。最終的に、生成されたコードを対象のコンピュータに書き込むS14ことでソフトウェア開発が完了する。このうち、ステップS10とS13が開発環境による自動生成処理である。次に、プログラムをコンピュータに書き込んだ後の動作を説明する。図5は、監視対象システム15およびランタイムオブザーバ16が実行される車載コンピュータと、その周辺装置を表した図である。車載コンピュータ34は、演算処理装置36および記憶装置37を有している。監視対象システム15およびランタイムオブザーバ16は、記憶装置37に格納されており、演算処理装置36にて実行される。監視対象システム15は、入出力および変数の状態が変化するごとに、ランタイムオブザーバ16にイベントを通知する。これにより、ランタイムオブザーバ16は、イベントをトリガとして、監視対象システム15が有する入出力および変数の状態が、要求仕様から外れていないかを確認することができる。監視方法を具体的な例で説明する。図6は、第1の実施形態に係るプログラムの構成を詳細化した図である。車載コンピュータ34は、センサ41から信号を取得する外部情報取得手段、およびアクチュエータ42へ信号を出力する外部情報出力手段を有している。ここで、監視対象システム15が満たすべき要求仕様として変数AおよびBがともに1であるとき、センサ41からの入力が0であれば、アクチュエータ42への出力は1というものがあった場合、ランタイムオブザーバ16は、センサ41からの入力状態、アクチュエータ42への出力状態、変数Aおよび変数Bを監視する。システム15は、ランタイムオブザーバ16に対して、入出力状態、および変数の内容が変化した場合、通知を行う。そして、ランタイムオブザーバ16が、前記の仕様を満たさない状態、たとえば変数AおよびBがともに1、センサ41からの入力が0、アクチュエータ42への出力が0という状態を検出した場合、仕様外の動作であると判定する。ランタイムオブザーバが、仕様から外れた動作を検出した場合、コンピュータはその異常の度合いに応じて、対処を行う必要がある。例えば、車両を制御するオペレーティングシステムに不具合を検出した場合、システムを、運転に必要最低限な構成であるセーフモードに移行することが考えられる。運転の継続が不可能な不具合である場合、運転者に警告を与え、車両停止後にシステムをシャットダウンすることが考えられる。また、比較的安全と考えられる事象であった場合、運転者に通知のみを行ったうえで運転を継続してもよい。仕様から外れた動作を検出した場合、車載コンピュータ34は、LEDやLCDなどの状態ディスプレイ32を通じて、運転者に異常が発生した旨を通知する。また、車載コンピュータの内部記憶装置35に、関連する情報をログとして記録する。不具合発生時の情報がメンテナンス時に役立つためである。記録する情報は、プログラムのメモリダンプや、各種レジスタの状態などが考えられる。また、これらのログ情報は、内部記憶装置35に記録されるほか、外部通信装置31を通して管理センター38に通知してもよい。また、発生した事象が重大であり、運行に影響を与えると判断した場合は、車載コンピュータ34は、システム制御部33に対して信号を発し、システムの一部を制限したモードセーフモードに移行してもよい。本実施形態によれば、数理的に正しい形式仕様を用いてランタイムオブザーバを生成し、プログラムを監視するため、処理において仕様から外れた状態が発生した場合、必ず検出することができるという利点がある。また、通常のモデルベーステストでは、考えられるケースを事前に定義して試験仕様を作らなくてはならないが、本発明では、エンドユーザが利用する実環境でプログラムを動作させながら監視を行うことができるため、テストで検出することができない予想外の不具合についても検出し、開発にフィードバックすることができるという利点がある。また、仕様から外れた動作を検出した場合、運転者に通知するとともに、システムの状態を変更することで、安全を担保することができるという利点があり、事象発生時の詳細情報を記録、もしくは送信することにより、迅速なシステムの復旧が可能になるという利点がある。また、本実施形態にて例示したプログラム監視の内容は、プログラムの変数と外部入出力の内容のみをチェックする簡単なものであるが、形式仕様記述で表現できるソフトウェア仕様であれば、複雑なものであっても適用することができる。例えば、次の読み込み時にセンサAから1が入力された場合、今後どこかの時点で出力Bから1が出力されることが保証されるが、次の読み込み時にセンサAから0が入力された場合、今後出力Bから1が出力されるかは保証されない。といったものや、センサAから1が入力されるまで、出力Cからは0が出力され続けるが、センサAからの入力が1となる状態が一度でもあった場合、出力Cからは1が出力され、メインスイッチを切らない限り保持し続けるといった仕様も形式仕様記述にて表現することができる。第1の実施形態においては、生成されたプログラムを車載コンピュータに書き込み、実際に自動車に搭載する例を挙げたが、実環境ではなく、仮想環境を用いて動作させてもよい。例えば、車載コンピュータに、エンジンをシミュレートするためのエンジンシミュレータを接続し、実際の自動車を模した環境でソフトウェアの試験を行ってもよい。また、第1の実施形態においては、形式仕様記述からオブザーバモデルを作成し、オブザーバモデルからコードを生成したが、形式仕様記述から直接コードを生成してもよい。第2の実施形態図7は、第2の実施形態に係る回路を表した図である。第1の実施形態では、ランタイムオブザーバと、監視対象のプログラムは同一コンピュータの演算処理装置上にて動作するが、本実施形態では、ランタイムオブザーバと、監視対象のプログラムは共に独立したハードウェア上にて動作する。本実施形態では第1の実施形態と同様に、ソフトウェア作成装置において、ソフトウェアモデルと、形式仕様から生成したオブザーバモデルを組み合わせた状態でコードの生成を行うが、コードはハードウェア記述言語で記述され、出力結果は集積回路等のデジタル回路に書き込まれる。このとき、演算プログラムと、監視プログラムは同一の集積回路に書き込んでもよいし、別個の集積回路に書き込んでもよい。図7は、演算プログラムが書き込まれた集積回路と、監視プログラムが書き込まれた集積回路が別個となっている例である。監視対象回路18は、監視対象となるプログラムが実行される回路であり、第1の実施形態における車載コンピュータ内の監視対象システム15が置き換わるものである。また、ランタイムオブザーバ回路19は、監視を行うプログラムが書き込まれた回路であり、第1の実施形態における車載コンピュータ内のランタイムオブザーバ16が置き換わるものである。本実施形態では、ランタイムオブザーバ回路19は、監視対象となる回路の入力信号および出力信号を監視し、入力信号の状態に変化があった場合、出力信号の状態確認を行う。出力信号に、仕様を外れた状態を検出した場合、異常信号線20を通して外部への異常通報を行う。異常通報がされた場合、コンピュータは、第1の実施形態と同様の対応をとることができる。なお、システム制御部33は、システムの一部を制限したモードに移行する代わりに、異常が発生した回路をバイパス、もしくは切り離してもよい。本実施形態のように構成することで、コンピュータ上ではなく、集積回路上で直接動作するプログラムにも、本発明を適用することができる。第1の実施形態が、同一のコンピュータ上で動作するのに対し、本実施形態ではランタイムオブザーバを別個の集積回路に書き込んでいるため、監視対象システムが動作する回路と、監視を行うランタイムオブザーバが動作する回路を分離して設計することができるという利点を有している。第3の実施形態第3の実施形態について、図8を参照しながら説明する。第1の実施形態では、ソフトウェアモデルにオブザーバモデルを付加してコードを生成するため、プログラム上のオーバーヘッドが増大し、コンピュータのリソースを消費するという欠点がある。これを補うため、オブザーバモデルの生成時に、開発者が監視に用いる形式仕様記述を選択できるようにするのが本実施形態である。形式仕様は、複数の数式で構成される。本実施形態では、燃料系、駆動系、安全装置系の各系統に対応する形式仕様記述があった場合を例として挙げる。通常、3種類全てに対応するランタイムオブザーバを生成するところ、オーバーヘッドの関係から許容される系統が2つまでという制限があった場合、たとえば開発者は、オブザーバモデル生成部52に対して、駆動系と安全装置系の2種類に対応する形式仕様記述のみを指定することができる。図8は、本実施形態におけるオブザーバモデルとシステムモデルを示した図である。駆動系および安全装置系の形式仕様記述のみを選択し、オブザーバモデル12を作成した場合、ランタイムオブザーバ16は、駆動系および安全装置系のみを監視するよう構成される。一方、監視対象となるシステムモデルには、駆動系システムのモデル27、安全装置系システムのモデル28、燃料系システムのモデル29がある。駆動系システムのモデル27、安全装置系システムのモデル28に対しては、図9に示したように、ランタイムオブザーバが生成されるため、開発者が診断のためのモデルを作成する必要はない。一方、燃料系システムのモデル29について監視を行う場合は、開発者が別途診断のためのブロック30を作成してもよい。この場合、燃料系の監視プログラムは、従来通りのダイアグノーシス機能26として生成され、監視対象システム15に組み込まれる。本実施形態のように構成することで、信頼性の高いランタイムオブザーバには、安全のために最低限必要なもののみを搭載し、その他の、故障しても直ちに安全に影響しない機能については、従来通りに開発者が設計した診断機能ダイアグノーシスで対応するといった運用が可能になる。これにより、オーバーヘッドと安全性というトレードオフ関係の両立が可能となる。第3の実施形態では、燃料系、駆動系、安全装置系のそれぞれの系統について、系統単位で監視の適用/非適用を指定したが、それぞれの形式仕様記述は複数の条件式から成っているため、条件式ごとに適用の有無を指定することができる。なお、各実施形態の説明は本発明を説明する上での例示にすぎず、本発明を上記の実施形態に限定して解釈すべきではない。例えば、複数の実施形態を組み合わせてもよいし、仕様外の動作を検出した場合、第1の実施形態にて例示していない方法によって通知を行ってもよい。