"システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報を受け付ける検証対象指定部と、前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する検証対象判断部と、前記検証対象判断部によって検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを、前記モデル情報に基づき生成する検証コード変換部と、前記検証コードに基づいてモデル検査を実行するモデル検査実行部とを有するモデル検査装置。前記検証対象判断部によって検証対象であると判断された前記制約条件に対応する時相論理式を生成する時相論理式変換部をさらに備え、また、前記検証コード変換部に代えて、前記モデル情報に含まれている全ての前記制約条件について前記モデル検査を実行する手順を示す検証コードを生成する検証コード生成部を備え、前記モデル検査実行部は、前記時相論理式変換部により生成された前記時相論理式と、前記検証コード生成部により生成された前記検証コードとに基づいて、前記モデル検査を実行する請求項1記載のモデル検査装置。前記検証コード変換部は、前記モデル情報に含まれているにも拘わらず、前記検証対象判断部によって検証対象であると判断されなかった前記制約条件に対応する部分を含まない前記検証コードを生成する請求項1記載のモデル検査装置。システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報をコンピュータで受け付け、前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かをコンピュータが判断し、検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードをコンピュータが前記モデル情報に基づき生成し、前記検証コードに基づいてコンピュータがモデル検査を実行するモデル検査方法。前記検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す前記検証コードを生成することに代えて、前記モデル情報に含まれている全ての前記制約条件について前記モデル検査を実行する手順を示す検証コードを生成し、検証対象であると判断された前記制約条件に対応する時相論理式をさらに生成し、前記時相論理式および前記検証コードに基づいて、前記モデル検査を実行する請求項4記載のモデル検査方法。コンピュータに、システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報を受け付ける機能と、前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する機能と、検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを前記モデル情報に基づき生成する機能と、前記検証コードに基づいてモデル検査を実行する機能とを持たせるコンピュータプログラム。コンピュータに、前記検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す前記検証コードを生成する機能に代えて、前記モデル情報に含まれている全ての前記制約条件について前記モデル検査を実行する手順を示す検証コードを生成する機能を持たせ、さらに、検証対象であると判断された前記制約条件に対応する時相論理式を生成する機能と、前記時相論理式および前記検証コードに基づいて、前記モデル検査を実行する機能とを持たせる請求項6記載のコンピュータプログラム。特許文献1等に示されているモデル検査を実行する装置モデル検査装置がモデル検査を行う場合には、例えば図12に示すようなフローで動作する。ところで、モデル検査を行うに際し、ユーザは、次に述べるモデル情報を作成しモデル検査装置に入力する。例えば、図13に示されるように、モデル情報D11は、処理毎の情報処理情報P1,Pnnは1以上の整数を有する。各処理情報P1,Pnは、処理の識別子d1と、処理が参照する変数名d2と、処理が満たすべき制約条件事前条件、事後条件、不変条件d3と、処理の動作仕様d4とを含んでいる。モデル検査装置は、上記のようなモデル情報D11が入力されている状態で、モデル検査を開始する。まず、モデル検査装置は、モデル情報D11を基に、検証コードを生成する図12のステップS1。その検証コードは、モデル情報D11に含まれている全ての制約条件事前条件、事後条件、不変条件を検証する検証コードソースコードである。検証コードを生成した後に、モデル検査装置は、その検証コードを利用して、モデル検査を実行するステップS2。そして、モデル検査装置は、その検査結果を出力するステップS3。これにより、ユーザは、検査結果を確認できる。上記のようなモデル検査装置には次のような問題がある。つまり、前述したように、モデル検査装置が生成する検証コードは、モデル情報D11に含まれている全ての制約条件事前条件、事後条件、不変条件を検証する検証コードである。モデル検査装置は、その検証コードに基づいてモデル検査検証を行うことから、モデル情報D11に含まれている全ての制約条件事前条件、事後条件、不変条件を検証する。モデル情報D11に含まれる処理情報事前条件、事後条件、不変条件の数は、システムやソフトウェアの複雑化巨大化によって、増大する傾向にある。このため、モデル検査装置が、モデル情報D11に含まれている全ての制約条件事前条件、事後条件、不変条件を検証すると、モデル検査に多くの時間が掛かる。また、検査結果の情報量も増加することから、ユーザが検査結果を確認する時間が長くなる。このようなことから、モデル検査に関わる作業の効率化のために、ユーザが、モデル情報D11に含まれる制約条件事前条件、事後条件、不変条件の中から、特定の性質の成否に関わる一部の制約条件について検証したいという要望を持つ場合がある。しかしながら、上記モデル検査装置は、前述したように、モデル情報D11に含まれる全ての制約条件事前条件、事後条件、不変条件を検証する検証コードに基づいてモデル検査を行うために、モデル情報D11に含まれている一部の制約条件について検証できない。このため、上記特定の制約条件事前条件、事後条件、不変条件について検証したい場合には、ユーザが、その特定の制約条件を検証させる別のモデル情報D11を作成しモデル情報D11を変更し、当該モデル情報D11をモデル検査装置に入力しなければならない。この作業は、検証対象の事前条件、事後条件、不変条件を変更する度に、行わなければならず、ユーザにとって、面倒かつ手間が掛かり、モデル検査に関わる時間の増加を招いてしまう。本発明はそのような問題を解決するために考え出された。すなわち、本発明の主な目的は、モデル情報に含まれている一部の制約条件事前条件、事後条件、不変条件を検証するモデル検査が可能なモデル検査装置、モデル検査方法およびコンピュータプログラムを提供することにある。本発明のモデル検査装置は、システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報を受け付ける検証対象指定部と、前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する検証対象判断部と、前記検証対象判断部によって検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを、前記モデル情報に基づき生成する検証コード変換部と、前記検証コードに基づいてモデル検査を実行するモデル検査実行部とを有する。本発明のモデル検査方法は、システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報をコンピュータで受け付け、前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かをコンピュータが判断し、検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードをコンピュータが前記モデル情報に基づき生成し、前記検証コードに基づいてコンピュータがモデル検査を実行する。本発明のコンピュータプログラムは、コンピュータに、システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報を受け付ける機能と、前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する機能と、検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを前記モデル情報に基づき生成する機能と、前記検証コードに基づいてモデル検査を実行する機能とを持たせる。なお、本発明の前記目的は、本発明のモデル検査装置に対応する本発明のモデル検査方法によっても、また、本発明のモデル検査方法をコンピュータによって実現するコンピュータプログラムによっても、達成される。本発明によれば、モデル情報に含まれている一部の制約条件事前条件、事後条件、不変条件を検証するモデル検査が可能となる。以下に、本発明に係る実施形態を図面を参照して説明する。第1実施形態図1は、本発明に係る第1実施形態のモデル検査装置の構成を簡略的に示すブロック図である。図1に示されるように、第1実施形態のモデル検査装置1は、モデル情報入力部11と、検証対象指定部12と、検証コード生成部13と、モデル検査実行部14と、検証結果出力部15とを有する。検証コード生成部13は、検証対象判断部16と、検証コード変換部17とを有する。なお、この第1実施形態では、モデル検査装置1は、制御装置例えばCPUCentralProcessingUnit2を備えている。当該制御装置2は、データやコンピュータプログラムプログラムを格納する記憶装置6から、モデル検査に関わるプログラムを読み出し当該プログラムに従って動作することにより、上記のような各構成部機能11~17を備える。モデル情報入力部11は、図13に示されるようなモデル情報D11を受け付ける機能を備えている。モデル情報D11は、システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理毎の情報処理情報P1,Pnnは1以上の整数を含んでいる。各処理情報P1,Pnは、処理の識別子d1と、処理が参照する変数名d2と、処理が満たすべき制約条件ここでは、事前条件、事後条件、不変条件d3と、処理の動作仕様d4とを含んでいる。このようなモデル情報D11は、ユーザによって作成され、入力装置情報を入力する例えばキーボードやマウスやタッチパネルなど4を利用してユーザによりモデル検査装置1に入力される。検証対象指定部12は、モデル情報入力部11で受け付けたモデル情報D11に含まれている制約条件事前条件、事後条件、不変条件の中から、ユーザーにより入力装置4を利用して指定された検証対象である制約条件の情報指定情報を受け付ける機能を備えている。モデル検査実行部14は、後述する検証コード生成部13で生成された検証コードに基づいて、モデル検査を実行する機能を備えている。検証結果出力部15は、モデル検査実行部14が実行したモデル検査の結果を出力する機能を備えている。その検査結果は例えば出力装置例えばディスプレイやプリンタなど5に出力される。出力装置5は、そのモデル検査の結果を画面表示したり、プリントアウトする。これにより、ユーザは、モデル検査の結果を確認できる。検証コード生成部13の検証対象判断部16は、検証対象指定部12で受け付けた指定情報に基づいて、モデル情報D11に含まれている事前条件、事後条件、不変条件のそれぞれに関し、検証コードに反映するか否か換言すれば、検証対象とするか否かを判断する機能を備えている。検証コード生成部13の検証コード変換部17は、検証対象判断部16の判断結果を利用し、モデル情報D11を、モデル検査実行部14が実行可能な検証コードに変換する機能を備えている。その検証コードは、検証する処理の内容と、その処理の検証内容とを定義している。この第1実施形態では、検証コード変換部17が生成する検証コードは、検証対象と判断された制約条件事前条件、事後条件、不変条件についてのモデル検査を実行する手順を示す検証コードである。以下に、モデル検査装置1の動作例を図2を利用して説明する。なお、図2は、モデル検査装置1が実行するモデル検査動作処理の一例を示すフローチャートであり、当該フローチャートは、モデル検査装置1の制御装置2が実行するコンピュータプログラムソフトウェアの処理手順を表す。モデル検査装置1が図2に示す動作を開始する際には、ユーザにより作成されたモデル情報D11がモデル情報入力部11で受け付けられ、また、ユーザにより指定された検証対象を示す指定情報が検証対象指定部12で受け付けられた状態である。この状態において、モデル検査装置1の検証対象判断部16制御装置2は、モデル情報D11に含まれている制約条件事前条件、事後条件、不変条件のそれぞれに関し、ユーザーからの指定情報に基づいて、検証コードに反映するか否かを判断する図2のステップS101。その後、検証コード変換部17制御装置2は、検証対象判断部16の判断結果に基づいて、次に述べるようにモデル情報D11を検証コードに変換する。すなわち、検証コード変換部17は、空の検証コードD12を生成するステップS102。次に、検証コード変換部17は、モデル情報D11に含まれる処理情報P1~Pnの中に未チェックの処理情報が有るか否かを判断するステップS103。そして、検証コード変換部17は、未抽出の処理情報が有ると判断した場合には、その未抽出の処理情報の一つここでは、処理情報Pnと記すをモデル情報D11から抽出するステップS104。次に、検証コード変換部17は、抽出した処理情報Pnの動作仕様d4に基づいた検証コードD12_Pnを生成するステップS105。その検証コードD12_Pnは、処理情報Pnに基づいた処理と同様の動作を実行させるコードである。そして、検証コード変換部17は、抽出した処理情報Pnに含まれている制約条件事前条件、事後条件、不変条件のそれぞれについて、検証対象判断部16の判断結果に基づき、検証対象と判断された条件であるか否かを判断するステップS106。検証対象と判断された条件である場合には、検証コード変換部17は、その検証対象と判断された条件Cnに基づいた検証コードD12_Cnを生成するステップS107。そして、検証コード変換部17は、その検証コードD12_Cnを検証コードD12_Pnに挿入するステップS108。その挿入位置は、検証コードの生成手法により異なるが、例えば、事前条件であれば処理に関する部分の直前であり、事後条件であれば処理に関する部分の直後であり、不変条件であれば処理に関する部分内である。次に、検証コード変換部17は、検証コードD12_Pnを検証コードD12にマージするステップS109。前記ステップS106において、抽出した処理情報Pnに含まれている何れの制約条件事前条件、事後条件、不変条件も検証対象と判断されなかった場合には、検証コード変換部17は、前記ステップS109において、条件無し検証コードD12_Cnが挿入されていない検証コードD12_Pnを検証コードD12にマージする。その後、検証コード変換部17は、前記ステップS103以降の動作を繰り返す。そして、ステップS103において、モデル情報D11の中に未抽出の処理情報が無いと判断した場合には、検証コード変換部17は、検証コードD12をモデル検査実行部14に出力する。これにより、モデル検査実行部14制御装置2は、その検証コードD12に基づいてモデル検査を実行するステップS110。然る後に、モデル検査実行部14は、検証結果を生成し、その検査結果を検証結果出力部15に出力する。検証結果出力部15制御装置2は、その検証結果を、出力装置5に適合する形式の情報に変換して出力装置5に出力するステップS111。これにより、モデル検査の結果が出力装置5によって出力されて、ユーザーは、モデル検査の結果を確認できる。この第1実施形態のモデル検査装置1は、上記のような検証対象判断部16と検証コード変換部17を有する検証コード生成部13、および、検証対象指定部12を備えることにより、次のような効果を得ることができる。すなわち、モデル検査装置1は、モデル検査を行う検証コードを生成する際に、モデル情報D11に含まれている制約条件事前条件、事後条件、不変条件のそれぞれに関し、ユーザーからの指定情報に基づいて、検証対象であるか否かを判断する。そして、モデル検査装置1は、検証対象であると判断された条件だけを反映した検証コードを生成する。モデル検査装置1は、その検証コードに基づいてモデル検査を実行するので、ユーザが要望指定する検証対象である制約条件事前条件、事後条件、不変条件のみについてモデル検査を行うことができる。つまり、モデル検査装置1は、モデル情報D11に含まれている全ての制約条件事前条件、事後条件、不変条件についてのモデル検査はもちろんのこと、モデル情報D11に含まれている一部の制約条件事前条件、事後条件、不変条件についてのモデル検査をも実行することが可能となる。これにより、モデル検査装置1は、ユーザが要望する検証対象の制約条件についてのモデル検査の結果だけを出力することが可能となる。このため、ユーザは、要望しない制約条件の検査結果をもチェックしなければならないという無駄を無くすことができる。これにより、ユーザによる検査結果確認の効率化を図ることができる。また、この第1実施形態では、検証対象の制約条件事前条件、事後条件、不変条件が変更になった場合に、その検証対象の制約条件がモデル情報D11に含まれていれば、ユーザは、そのモデル情報D11の制約条件の中から、検証対象の制約条件を指定するだけでよいなる。つまり、この第1実施形態のモデル検査装置1は、検証対象の制約条件事前条件、事後条件、不変条件が変更になる度にモデル情報D11を作成変更するというユーザの手間を軽減することができる。第2実施形態次に、本発明に係る第2実施形態を説明する。なお、この第2実施形態の説明において、第1実施形態と同様な構成部分には同一符号を付し、その共通部分の重複説明は省略する。この第2実施形態では、第1実施形態のモデル検査装置1にモデル検査ツールとしてSPINSimplePromelaInterpreterと呼ばれるコンピュータプログラムを用いる場合の具体例を示す。つまり、この第2実施形態では、モデル検査実行部14は、SPINに従ってモデル検査を実行する。SPINには複数のバージョンがあり、何れのバージョンを採用してもよいが、この第2実施形態では、例えば、バージョン4.2.9を採用する場合について説明する。この第2実施形態では、図3に示されるように、モデル情報D11に含まれる各処理情報メソッド情報P1,Pnの識別子d1、変数名d2、制約条件事前条件、事後条件、不変条件d3は、クラス図Fcの態様を採る。図4はクラス図Fcの一例を示している。なお、この第2実施形態では、処理をメソッドともいう。各メソッド情報P1,Pnの動作仕様d4は、アクティビティ図Faの態様を採る。図5はアクティビティ図Faの一例を示している。モデル情報入力部11は、上記のようなモデル情報D11を受け付ける。検証対象指定部12は、例えば表示装置図示せずの画面ディスプレイに、モデル情報D11に含まれている全ての制約条件事前条件、事後条件、不変条件のリストを表示させる指示を出力する機能を備える。そのリストの一例として、ドロップダウンリストがある。検証対象指定部12は、その表示されたリスト中から入力装置4を利用して指定選択された検査対象の制約条件の情報を、指定情報として受け取る。検証コード生成部13は、モデル検査ツールSPINの入力言語であるPromelaで記述された検証コードD12Promelaコードを生成する。具体的には、検証コード生成部13は、例えば次のように検証コードD12を生成する。すなわち、検証コード生成部13は、モデル情報D11におけるクラス図Fcで定義されている各クラスをそれぞれPromelaプロセスとして宣言する。また、検証コード生成部13は、各メソッド処理の動作仕様d4を各Promelaプロセスの動作として定義し、そのPromelaプロセスの動作にはそれぞれ各メソッドの識別子d1を変換したラベルを付ける。さらに、検証コード生成部13は、検証対象指定部12による指定情報に基づいて、検証対象と判断された制約条件事前条件、事後条件、不変条件d3を検証する検証コードD12_Cnを生成する。さらに、検証コード生成部13は、その検証コードD12_Cnを検証コードD12_Pnに挿入する。この挿入位置は、例えば、事前条件であればメソッドの最初の文の直前である。事後条件であればメソッドの最後の文の直後である。不変条件であればプロセスの外のグローバルな位置である。さらに、検証コード生成部13は、各メソッドが参照する変数名d2を変換しPromelaのグローバル変数として宣言する。図6はPromelaコード検証コードD12_Pnの一例を示す。この検証コードD12_Pnは、検証コード生成部13が、図3に示すモデル情報D11を、Promelaコードに変換したコードである。この図6に示される検証コードD12_Pnは、メソッドPnにおいて、事前条件も事後条件も不変条件も検証するコードである。これに対して、この第2実施形態では、例えば事前条件を反映しない検証対象としない場合には、検証コード生成部13によって、図6における事前条件を検証する文始と事前条件を検証する文終で囲まれている部分Zが生成挿入されない。検証結果出力部15は、モデル検査実行部14SPINによるモデル検査の結果を示す情報を、出力装置5に出力する機能を有する。さらに、この第2実施形態では、検証結果出力部15は、検証対象である制約条件事前条件、事後条件、不変条件が満たされない場合にその満たされないことを示す反例をシーケンス図で表示させる情報を出力装置5に出力する機能を備えている。図7はそのシーケンス図の一例を示している。この図7の例では、事前条件preconditionが満たさないことを表している。この第2実施形態のモデル検査装置1において、上記以外の構成は第1実施形態と同様である。また、第2実施形態のモデル検査装置1も、第1実施形態で述べた動作例図2のフローチャートに示される動作例と同様に動作する。この第2実施形態のモデル検査装置1も、第1実施形態と同様に、検証対象判断部16と検証コード変換部17を有する検証コード生成部13、および、検証対象指定部12を備えているので、第1実施形態と同様の効果を得ることができる。なお、この第2実施形態では、第1実施形態のモデル検査装置1にモデル検査ツールとしてSPINを用いる例を示したが、第1実施形態のモデル検査装置1に採用されるモデル検査ツールはSPINに限定されず、第1実施形態のモデル検査装置1にはSPIN以外のモデル検査ツールを採用してもよい。また、検証コード生成部13が生成する検証コードは、図6の示す態様に限定されず、変換手法に応じた態様となる。第3実施形態次に、本発明に係る第3実施形態を説明する。なお、この第3実施形態の説明において、第1や第2の実施形態と同様の構成部分には同一符号を付し、その共通部分の重複説明は省略する。図8は、本発明に係る第3実施形態のモデル検査装置の構成を簡略的に示すブロック図である。この第3実施形態のモデル検査装置3は、第1実施形態のモデル検査装置1の構成に加え、時相論理式生成部32を備えている。この時相論理式生成部32が検証対象判断部35を有しており、検証コード生成部33は検証対象判断部を有していない。時相論理式生成部32は、検証対象判断部35と、時相論理式変換部36とを有している。検証対象判断部35は、モデル情報入力部11で受け付けたモデル情報D11に含まれている制約条件事前条件、事後条件、不変条件のそれぞれに関し、検証対象指定部12による指定情報に基づいて時相論理式に反映変換するか否か換言すれば、検証対象であるか否かを判断する機能を備えている。時相論理式変換部36は、モデル情報D11と、検証対象判断部35の判断結果とに基づいて、時相論理式を生成する機能を備えている。つまり、時相論理式変換部36は、モデル情報D11に含まれる制約条件事前条件、事後条件、不変条件のそれぞれに関し、検証対象判断部35により反映する検証対象であると判断された条件を、当該条件が満たされるか否かを検証する時相論理式に変換する。検証コード生成部33は、モデル情報D11に基づいて、モデル検査実行部34が実行可能な検証コードを生成する機能を備えている。この第3実施形態では、検証コード生成部33は、モデル情報D11に含まれている全ての制約条件事前条件、事後条件、不変条件を反映する検証コードを生成する。モデル検査実行部34は、検証コード生成部33で生成された検証コードと、時相論理式生成部32により生成された時相論理式に基づいて、モデル検査を実行する機能を備えている。次に、モデル検査装置3の動作例を図9を利用して説明する。なお、図9は、モデル検査装置3が実行するモデル検査動作処理の一例を示すフローチャートであり、当該フローチャートは、モデル検査装置3の制御装置2が実行するコンピュータプログラムソフトウェアの処理手順を表す。モデル検査装置3が図9に示す動作を開始する際には、ユーザにより作成されたモデル情報D11がモデル情報入力部11で受け付けられ、また、ユーザにより指定された検証対象を示す指定情報が検証対象指定部12で受け付けられた状態である。この状態において、モデル検査装置3の検証コード生成部33制御装置2は、モデル情報D11に基づいて検証コードD31を生成する。つまり、検証コード生成部33は、図9に示すステップS301~S305の動作を行う。それら各ステップS301~S305は、それぞれ、図2に示すステップS102~S105,S109と同様の動作である。この第3実施形態では、検証コード生成部33は、図2に示すステップS106~S108の動作を行わない。図9に示すステップS301~S305の動作によって検証コードD31が生成された以降に、検証対象判断部35制御装置2が、モデル情報D11に含まれている制約条件事前条件、事後条件、不変条件のそれぞれに関し、検証対象指定部12による指定情報に基づいて、時相論理式に変換するか否かを判断するステップS306。そして、時相論理式変換部36制御装置2が、検証対象判断部35の検査結果に基づき、変換すると判断された検証対象である制約条件事前条件、事後条件、不変条件を時相論理式D32に変換するステップS307。その後、モデル検査実行部34は、検証コードD31において時相論理式D32が満たされるか否かを検証するモデル検査を実行するステップS308。然る後に、モデル検査実行部34は、検証結果を生成し、その検査結果を検証結果出力部15に出力する。検証結果出力部15制御装置2は、その検証結果を、出力装置5に適合する形式の情報に変換して出力装置5に出力するステップS309。これにより、モデル検査の結果が出力装置5によって出力されて、ユーザーは、モデル検査の結果を確認できる。この第3実施形態のモデル検査装置3は、検証対象判断部35を有する時相論理式生成部32、および、検証対象指定部12を備えているので、第1や第2の実施形態と同様の効果を得ることができる。つまり、検証コードおよび時相論理式を利用してモデル検査を実行するモデル検査装置3において、ユーザが要望指定する検証対象の制約条件のみの時相論理式を生成することができる。このため、モデル検査装置3は、モデル情報D11に含まれている全ての制約条件ではなく、一部の制約条件についてモデル検査を実行できる。これにより、モデル検査装置3は、ユーザによる検査結果確認の効率化を図ることができる効果や、検証対象の制約条件事前条件、事後条件、不変条件が変更になる度にモデル情報D11を作成変更するというユーザの手間を軽減できる効果を得ることができる。第4実施形態以下に、本発明に係る第4実施形態を説明する。なお、この第4実施形態の説明において、第1~第3の実施形態と同様な構成部分には同一符号を付し、その共通部分の重複説明は省略する。第4実施形態は、第3実施形態のモデル検査装置3にモデル検査ツールとしてSPINコンピュータプログラムを用いる場合の具体例を示す。時相論理式生成部32は、例えば図10に示されるような時相論理式を生成する。図10の例では、一つの処理メソッドにおいて、事前条件も事後条件も不変条件も時相論理式に変換されている。これに対して、この第3実施形態では、時相論理式生成部32は、検証対象判断部35によって変換しないと判断された制約条件に関する時相論理式を生成しない。例えば、事後条件を検証しない場合には、図10に示すB部分の時相論理式が生成されない。検証コード生成部33は、モデル情報D11に含まれている全ての制約条件事前条件、事後条件、不変条件を反映した検証コードD31を生成する。これ以外については、検証コード生成部33は、第2実施形態で示した検証コード生成部13とほぼ同様に検証コードD31を生成する。つまり、検証コード生成部33は、図3に示すモデル情報D11におけるクラス図Fcで定義されている各クラスをそれぞれPromelaプロセスとして宣言する。また、検証コード生成部33は、各メソッド処理の動作仕様d4を各Promelaプロセスの動作として定義し、そのPromelaプロセスの動作にはそれぞれ各メソッドの識別子d1を変換したラベルを付ける。さらに、検証コード生成部33は、制約条件事前条件、事後条件、不変条件d3が満たされているか否かを表す変数を宣言し、当該変数の値を変更するコードを生成する。さらに、検証コード生成部33は、そのコードを検証コードD31_Pnに挿入する。この挿入位置は、例えば、事前条件であればメソッドの最初の文の直前である。事後条件であればメソッドの最後の文の直後である。不変条件であればプロセスの外のグローバルな位置である。さらに、検証コード生成部33は、各メソッドが参照する変数名d2を変換しPromelaのグローバル変数として宣言する。このようにして、検証コード生成部33は、検証コードD31を生成する。この第4実施形態のモデル検査装置3は、第3実施形態と同様の構成を備えているので、第3実施形態と同様の効果を得ることができる。その他の実施形態本発明は第1~第4の各実施形態に限定されるものではなく、様々な実施の形態を採り得る。例えば、図11は、本発明に係るその他の実施形態であるモデル検査装置の構成を簡略的に示すブロック図である。このモデル検査装置20は、検証対象指定部21と、検証対象判断部22と、検証コード変換部23と、モデル検査実行部24とを有している。検証対象指定部21は、モデル検査で用いるモデル情報に含まれる制約条件である事前条件、事後条件、および、不変条件の中から、検証対象として指定された制約条件を示す指定情報を受け付ける機能を備えている。前述したように、事前条件とは、システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を開始する際に満たされるべき条件である。事後条件とは、前記処理が終了した際に満たされるべき条件である。不変条件とは、前記処理の実行中に満たされるべき条件である。検証対象判断部22は、前記モデル情報に含まれる前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する機能を備えている。検証コード変換部23は、前記検証対象判断部22によって検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを、前記モデル情報に基づき生成する機能を備えている。モデル検査実行部24は、前記検証コードに基づいてモデル検査を実行する機能を備えている。このモデル検査装置20においても、前記各実施形態と同様に、検証対象判断部22を備え、当該検証対象判断部22によって、モデル情報に含まれている前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、検証対象とするか否かを判断できる構成を備えている。そして、モデル検査装置20は、その検証対象と判断された制約条件に関するモデル検査を行うので、前記各実施形態と同様の効果を得ることができる。なお、このモデル検査装置20は、例えばコンピュータにより構成される。当該モデル検査装置20コンピュータは、記憶装置26に格納されているコンピュータプログラム27を読み出し、当該コンピュータプログラム27に従って動作する。そのコンピュータプログラム27は、コンピュータに、上記のような各構成部21~24の機能を持たせるプログラムである。このコンピュータプログラム27に従ってモデル検査装置20が動作することによって、モデル検査装置20は上記機能を持つことができる。なお、モデル情報に含まれている処理情報には、制約条件として、事前条件と事後条件と不変条件の全てが必ず含まれるとは限らない。"