(57)【要約】【課題】  モデル情報に含まれている一部の制約条件（事前条件、事後条件、不変条件）を検証するモデル検査を可能にする。【解決手段】  モデル検査装置２０は、検証対象指定部２１と、検証対象判断部２２と、検証コード変換部２３と、モデル検査実行部２４とを有している。検証対象指定部２１は、モデル検査で用いるモデル情報に含まれる制約条件（事前条件、事後条件、不変条件）の中から、検証対象として指定された制約条件を示す指定情報を受け付ける。検証対象判断部２２は、前記モデル情報に含まれる制約条件（事前条件、事後条件、不変条件）について、前記指定情報に基づいて、検証対象とするか否かを判断する。検証コード変換部２３は、検証対象であると判断された前記制約条件と、前記モデル情報に基づき、検証コードを生成する。モデル検査実行部２４は、前記検証コードに基づいてモデル検査を実行する。【選択図】      図１１
2013045269.tif 000002
【特許請求の範囲】
【請求項１】
システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報を受け付ける検証対象指定部と、
前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する検証対象判断部と、
前記検証対象判断部によって検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを、前記モデル情報に基づき生成する検証コード変換部と、
前記検証コードに基づいてモデル検査を実行するモデル検査実行部と
を有するモデル検査装置。
【請求項２】
前記検証対象判断部によって検証対象であると判断された前記制約条件に対応する時相論理式を生成する時相論理式変換部をさらに備え、また、前記検証コード変換部に代えて、前記モデル情報に含まれている全ての前記制約条件について前記モデル検査を実行する手順を示す検証コードを生成する検証コード生成部を備え、
前記モデル検査実行部は、前記時相論理式変換部により生成された前記時相論理式と、前記検証コード生成部により生成された前記検証コードとに基づいて、前記モデル検査を実行する請求項１記載のモデル検査装置。
【請求項３】
前記検証コード変換部は、前記モデル情報に含まれているにも拘わらず、前記検証対象判断部によって検証対象であると判断されなかった前記制約条件に対応する部分を含まない前記検証コードを生成する請求項１記載のモデル検査装置。
【請求項４】
システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報をコンピュータで受け付け、
前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かをコンピュータが判断し、
検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードをコンピュータが前記モデル情報に基づき生成し、
前記検証コードに基づいてコンピュータがモデル検査を実行するモデル検査方法。
【請求項５】
前記検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す前記検証コードを生成することに代えて、前記モデル情報に含まれている全ての前記制約条件について前記モデル検査を実行する手順を示す検証コードを生成し、
検証対象であると判断された前記制約条件に対応する時相論理式をさらに生成し、
前記時相論理式および前記検証コードに基づいて、前記モデル検査を実行する請求項４記載のモデル検査方法。
【請求項６】
コンピュータに、
システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報を受け付ける機能と、
前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する機能と、
検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを前記モデル情報に基づき生成する機能と、
前記検証コードに基づいてモデル検査を実行する機能と
を持たせるコンピュータプログラム。
【請求項７】
コンピュータに、
前記検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す前記検証コードを生成する機能に代えて、前記モデル情報に含まれている全ての前記制約条件について前記モデル検査を実行する手順を示す検証コードを生成する機能を持たせ、さらに、
検証対象であると判断された前記制約条件に対応する時相論理式を生成する機能と、
前記時相論理式および前記検証コードに基づいて、前記モデル検査を実行する機能と
を持たせる請求項６記載のコンピュータプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、システムやソフトウェアを検証するモデル検査装置、モデル検査方法およびコンピュータプログラムに関する。
【背景技術】
【０００２】
近年、システムやソフトウェアの複雑化・巨大化が進んでいる。このため、システムやソフトウェアの検証が難しくなっている。それに対する解決手段の一つとしてモデル検査がある。モデル検査とは、検証対象を状態遷移系としてモデル化し、それを網羅的に探索し、検証対象が仕様を満たすか否かを検証する技術である。モデル検査は、システムやソフトウェアの設計段階から適用できるため、検証対象が仕様を満たすか否かを設計段階で検証できる。このことから、モデル検査は、システムやソフトウェアの信頼性を向上させる技術として注目されている。
【０００３】
一方、システムやソフトウェアの仕様を定義する手法として、次のような事前条件、事後条件、不変条件を定義する手法がある。事前条件とは、システムが行う処理、あるいはソフトウェアに基づいてコンピュータが実行する処理の開始時に満たされるべき条件を示す。事後条件とは、処理の終了時に満たされるべき条件を示す。不変条件とは、処理の実行中に常に満たされるべき条件を示す。これらの条件を定義することで、システムやソフトウェアの仕様を定義し、また、システムやソフトウェアに不具合があった場合にその原因を容易に判明しやすくする。
【０００４】
システムによる処理、あるいは、ソフトウェアに基づいた処理が事前条件、事後条件、不変条件をそれぞれ満たすか否かを検証するために、前述したモデル検査を用いる場合がある。例えば、特許文献１は、次のようなシステムの検証手法を開示している。つまり、特許文献１に示される検証手法では、検証対象のシステムが行うアクションの制約条件を事前条件および事後条件として定義し、当該システムにおいて、それら条件が満たされるか否かをモデル検査により検証している。
【０００５】
特許文献２は、ソースコード（ソフトウェア）の検証にモデル検査を利用する場合の技術を開示している。特許文献３は、システム開発のテスト工程においてモデル検査を利用する技術を開示している。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２０１０−２０５５５号公報
【特許文献２】特開２００９−２１１５０３号公報
【特許文献３】特開２０１０−１０２６５０号公報
【発明の概要】
【発明が解決しようとする課題】
【０００７】
特許文献１等に示されているモデル検査を実行する装置（モデル検査装置）がモデル検査を行う場合には、例えば図１２に示すようなフローで動作する。ところで、モデル検査を行うに際し、ユーザは、次に述べるモデル情報を作成しモデル検査装置に入力する。例えば、図１３に示されるように、モデル情報Ｄ１１は、処理毎の情報（処理情報）Ｐ1，・・・Ｐn（ｎは１以上の整数）を有する。各処理情報Ｐ1，・・・Ｐnは、処理の識別子ｄ１と、処理が参照する変数名ｄ２と、処理が満たすべき制約条件（事前条件、事後条件、不変条件）ｄ３と、処理の動作仕様ｄ４とを含んでいる。
【０００８】
モデル検査装置は、上記のようなモデル情報Ｄ１１が入力されている状態で、モデル検査を開始する。まず、モデル検査装置は、モデル情報Ｄ１１を基に、検証コードを生成する（図１２のステップＳ１）。その検証コードは、モデル情報Ｄ１１に含まれている全ての制約条件（事前条件、事後条件、不変条件）を検証する検証コード（ソースコード）である。
【０００９】
検証コードを生成した後に、モデル検査装置は、その検証コードを利用して、モデル検査を実行する（ステップＳ２）。そして、モデル検査装置は、その検査結果を出力する（ステップＳ３）。これにより、ユーザは、検査結果を確認できる。
【００１０】
上記のようなモデル検査装置には次のような問題がある。つまり、前述したように、モデル検査装置が生成する検証コードは、モデル情報Ｄ１１に含まれている全ての制約条件（事前条件、事後条件、不変条件）を検証する検証コードである。モデル検査装置は、その検証コードに基づいてモデル検査（検証）を行うことから、モデル情報Ｄ１１に含まれている全ての制約条件（事前条件、事後条件、不変条件）を検証する。モデル情報Ｄ１１に含まれる処理情報（事前条件、事後条件、不変条件）の数は、システムやソフトウェアの複雑化・巨大化によって、増大する傾向にある。このため、モデル検査装置が、モデル情報Ｄ１１に含まれている全ての制約条件（事前条件、事後条件、不変条件）を検証すると、モデル検査に多くの時間が掛かる。また、検査結果の情報量も増加することから、ユーザが検査結果を確認する時間が長くなる。
【００１１】
このようなことから、モデル検査に関わる作業の効率化のために、ユーザが、モデル情報Ｄ１１に含まれる制約条件（事前条件、事後条件、不変条件）の中から、特定の性質の成否に関わる一部の制約条件について検証したいという要望を持つ場合がある。しかしながら、上記モデル検査装置は、前述したように、モデル情報Ｄ１１に含まれる全ての制約条件（事前条件、事後条件、不変条件）を検証する検証コードに基づいてモデル検査を行うために、モデル情報Ｄ１１に含まれている一部の制約条件について検証できない。
【００１２】
このため、上記特定の制約条件（事前条件、事後条件、不変条件）について検証したい場合には、ユーザが、その特定の制約条件を検証させる別のモデル情報Ｄ１１を作成し（モデル情報Ｄ１１を変更し）、当該モデル情報Ｄ１１をモデル検査装置に入力しなければならない。この作業は、検証対象の事前条件、事後条件、不変条件を変更する度に、行わなければならず、ユーザにとって、面倒かつ手間が掛かり、モデル検査に関わる時間の増加を招いてしまう。
【００１３】
本発明はそのような問題を解決するために考え出された。すなわち、本発明の主な目的は、モデル情報に含まれている一部の制約条件（事前条件、事後条件、不変条件）を検証するモデル検査が可能なモデル検査装置、モデル検査方法およびコンピュータプログラムを提供することにある。
【課題を解決するための手段】
【００１４】
本発明のモデル検査装置は、
システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報を受け付ける検証対象指定部と、
前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する検証対象判断部と、
前記検証対象判断部によって検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを、前記モデル情報に基づき生成する検証コード変換部と、
前記検証コードに基づいてモデル検査を実行するモデル検査実行部と
を有する。
【００１５】
本発明のモデル検査方法は、
システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報をコンピュータで受け付け、
前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かをコンピュータが判断し、
検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードをコンピュータが前記モデル情報に基づき生成し、
前記検証コードに基づいてコンピュータがモデル検査を実行する。
【００１６】
本発明のコンピュータプログラムは、
コンピュータに、
システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を検証するモデル検査で用いるモデル情報に含まれる制約条件であって前記処理を開始する際に満たされるべき事前条件、前記処理を終了した際に満たされるべき事後条件、および、前記処理の実行中に満たされるべき不変条件の中から、検証対象として指定された前記制約条件を示す指定情報を受け付ける機能と、
前記モデル情報に含まれる前記制約条件である前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する機能と、
検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを前記モデル情報に基づき生成する機能と、
前記検証コードに基づいてモデル検査を実行する機能と
を持たせる。
【００１７】
なお、本発明の前記目的は、本発明のモデル検査装置に対応する本発明のモデル検査方法によっても、また、本発明のモデル検査方法をコンピュータによって実現するコンピュータプログラムによっても、達成される。
【発明の効果】
【００１８】
本発明によれば、モデル情報に含まれている一部の制約条件（事前条件、事後条件、不変条件）を検証するモデル検査が可能となる。
【図面の簡単な説明】
【００１９】
【図１】本発明に係る第１実施形態のモデル検査装置の構成を簡略的に示すブロック図である。
【図２】本発明に係る第１実施形態のモデル検査装置の動作例を示すフローチャートである。
【図３】本発明に係る第２実施形態のモデル検査装置が受け付けるモデル情報の一例を説明する図である。
【図４】モデル情報に含まれるクラス図を模式的に示す図である。
【図５】モデル情報に含まれるアクティビティ図を模式的に示す図である。
【図６】検証コードであるPromela（Process Meta Language）コードの一例を表す図である。
【図７】モデル検査装置から出力される反例の一例を示す図である。
【図８】本発明に係る第３実施形態のモデル検査装置の構成を簡略的に示すブロック図である。
【図９】本発明に係る第３実施形態のモデル検査装置の動作例を示すフローチャートである。
【図１０】時相論理式の一例を表す図である。
【図１１】本発明に係るその他の実施形態であるモデル検査装置の構成を簡略的に示すブロック図である。
【図１２】特許文献１等に示されるモデル検査のフローを説明するフローチャートである。
【図１３】モデル情報を説明する図である。
【発明を実施するための形態】
【００２０】
以下に、本発明に係る実施形態を図面を参照して説明する。
【００２１】
（第１実施形態）
図１は、本発明に係る第１実施形態のモデル検査装置の構成を簡略的に示すブロック図である。図１に示されるように、第１実施形態のモデル検査装置１は、モデル情報入力部１１と、検証対象指定部１２と、検証コード生成部１３と、モデル検査実行部１４と、検証結果出力部１５とを有する。検証コード生成部１３は、検証対象判断部１６と、検証コード変換部１７とを有する。なお、この第１実施形態では、モデル検査装置１は、制御装置（例えばＣＰＵ（Central Processing Unit））２を備えている。当該制御装置２は、データやコンピュータプログラム（プログラム）を格納する記憶装置６から、モデル検査に関わるプログラムを読み出し当該プログラムに従って動作することにより、上記のような各構成部（機能）１１〜１７を備える。
【００２２】
モデル情報入力部１１は、図１３に示されるようなモデル情報Ｄ１１を受け付ける機能を備えている。モデル情報Ｄ１１は、システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理毎の情報（処理情報）Ｐ1，・・・Ｐn（ｎは１以上の整数）を含んでいる。各処理情報Ｐ1，・・・Ｐnは、処理の識別子ｄ１と、処理が参照する変数名ｄ２と、処理が満たすべき制約条件（ここでは、事前条件、事後条件、不変条件）ｄ３と、処理の動作仕様ｄ４とを含んでいる。このようなモデル情報Ｄ１１は、ユーザによって作成され、入力装置（情報を入力する例えばキーボードやマウスやタッチパネルなど）４を利用してユーザによりモデル検査装置１に入力される。
【００２３】
検証対象指定部１２は、モデル情報入力部１１で受け付けたモデル情報Ｄ１１に含まれている制約条件（事前条件、事後条件、不変条件）の中から、ユーザーにより入力装置４を利用して指定された検証対象である制約条件の情報（指定情報）を受け付ける機能を備えている。
【００２４】
モデル検査実行部１４は、後述する検証コード生成部１３で生成された検証コードに基づいて、モデル検査を実行する機能を備えている。
【００２５】
検証結果出力部１５は、モデル検査実行部１４が実行したモデル検査の結果を出力する機能を備えている。その検査結果は例えば出力装置（例えばディスプレイやプリンタなど）５に出力される。出力装置５は、そのモデル検査の結果を画面表示したり、プリントアウトする。これにより、ユーザは、モデル検査の結果を確認できる。
【００２６】
検証コード生成部１３の検証対象判断部１６は、検証対象指定部１２で受け付けた指定情報に基づいて、モデル情報Ｄ１１に含まれている事前条件、事後条件、不変条件のそれぞれに関し、検証コードに反映するか否か（換言すれば、検証対象とするか否か）を判断する機能を備えている。
【００２７】
検証コード生成部１３の検証コード変換部１７は、検証対象判断部１６の判断結果を利用し、モデル情報Ｄ１１を、モデル検査実行部１４が実行可能な検証コードに変換する機能を備えている。その検証コードは、検証する処理の内容と、その処理の検証内容とを定義している。この第１実施形態では、検証コード変換部１７が生成する検証コードは、検証対象と判断された制約条件（事前条件、事後条件、不変条件）についてのモデル検査を実行する手順を示す検証コードである。
【００２８】
以下に、モデル検査装置１の動作例を図２を利用して説明する。なお、図２は、モデル検査装置１が実行するモデル検査動作（処理）の一例を示すフローチャートであり、当該フローチャートは、モデル検査装置１の制御装置２が実行するコンピュータプログラム（ソフトウェア）の処理手順を表す。
【００２９】
モデル検査装置１が図２に示す動作を開始する際には、ユーザにより作成されたモデル情報Ｄ１１がモデル情報入力部１１で受け付けられ、また、ユーザにより指定された検証対象を示す指定情報が検証対象指定部１２で受け付けられた状態である。この状態において、モデル検査装置１の検証対象判断部１６（制御装置２）は、モデル情報Ｄ１１に含まれている制約条件（事前条件、事後条件、不変条件）のそれぞれに関し、ユーザーからの指定情報に基づいて、検証コードに反映するか否かを判断する（図２のステップＳ１０１）。
【００３０】
その後、検証コード変換部１７（制御装置２）は、検証対象判断部１６の判断結果に基づいて、次に述べるようにモデル情報Ｄ１１を検証コードに変換する。すなわち、検証コード変換部１７は、空の検証コードＤ１２を生成する（ステップＳ１０２）。次に、検証コード変換部１７は、モデル情報Ｄ１１に含まれる処理情報Ｐ1〜Ｐnの中に未チェックの処理情報が有るか否かを判断する（ステップＳ１０３）。そして、検証コード変換部１７は、未抽出の処理情報が有ると判断した場合には、その未抽出の処理情報の一つ（ここでは、処理情報Ｐnと記す）をモデル情報Ｄ１１から抽出する（ステップＳ１０４）。次に、検証コード変換部１７は、抽出した処理情報Ｐnの動作仕様ｄ４に基づいた検証コードＤ１２＿Ｐnを生成する（ステップＳ１０５）。その検証コードＤ１２＿Ｐnは、処理情報Ｐnに基づいた処理と同様の動作を実行させるコードである。
【００３１】
そして、検証コード変換部１７は、抽出した処理情報Ｐnに含まれている制約条件（事前条件、事後条件、不変条件）のそれぞれについて、検証対象判断部１６の判断結果に基づき、検証対象と判断された条件であるか否かを判断する（ステップＳ１０６）。検証対象と判断された条件である場合には、検証コード変換部１７は、その検証対象と判断された条件Ｃnに基づいた検証コードＤ１２＿Ｃnを生成する（ステップＳ１０７）。そして、検証コード変換部１７は、その検証コードＤ１２＿Ｃnを検証コードＤ１２＿Ｐnに挿入する（ステップＳ１０８）。その挿入位置は、検証コードの生成手法により異なるが、例えば、事前条件であれば処理に関する部分の直前であり、事後条件であれば処理に関する部分の直後であり、不変条件であれば処理に関する部分内である。
【００３２】
次に、検証コード変換部１７は、検証コードＤ１２＿Ｐnを検証コードＤ１２にマージする（ステップＳ１０９）。前記ステップＳ１０６において、抽出した処理情報Ｐnに含まれている何れの制約条件（事前条件、事後条件、不変条件）も検証対象と判断されなかった場合には、検証コード変換部１７は、前記ステップＳ１０９において、条件無し（検証コードＤ１２＿Ｃnが挿入されていない）検証コードＤ１２＿Ｐnを検証コードＤ１２にマージする。
【００３３】
その後、検証コード変換部１７は、前記ステップＳ１０３以降の動作を繰り返す。そして、ステップＳ１０３において、モデル情報Ｄ１１の中に未抽出の処理情報が無いと判断した場合には、検証コード変換部１７は、検証コードＤ１２をモデル検査実行部１４に出力する。これにより、モデル検査実行部１４（制御装置２）は、その検証コードＤ１２に基づいてモデル検査を実行する（ステップＳ１１０）。
【００３４】
然る後に、モデル検査実行部１４は、検証結果を生成し、その検査結果を検証結果出力部１５に出力する。検証結果出力部１５（制御装置２）は、その検証結果を、出力装置５に適合する形式の情報に変換して出力装置５に出力する（ステップＳ１１１）。これにより、モデル検査の結果が出力装置５によって出力されて、ユーザーは、モデル検査の結果を確認できる。
【００３５】
この第１実施形態のモデル検査装置１は、上記のような検証対象判断部１６と検証コード変換部１７を有する検証コード生成部１３、および、検証対象指定部１２を備えることにより、次のような効果を得ることができる。すなわち、モデル検査装置１は、モデル検査を行う検証コードを生成する際に、モデル情報Ｄ１１に含まれている制約条件（事前条件、事後条件、不変条件）のそれぞれに関し、ユーザーからの指定情報に基づいて、検証対象であるか否かを判断する。そして、モデル検査装置１は、検証対象であると判断された条件だけを反映した検証コードを生成する。モデル検査装置１は、その検証コードに基づいてモデル検査を実行するので、ユーザが要望（指定）する検証対象である制約条件（事前条件、事後条件、不変条件）のみについてモデル検査を行うことができる。つまり、モデル検査装置１は、モデル情報Ｄ１１に含まれている全ての制約条件（事前条件、事後条件、不変条件）についてのモデル検査はもちろんのこと、モデル情報Ｄ１１に含まれている一部の制約条件（事前条件、事後条件、不変条件）についてのモデル検査をも実行することが可能となる。これにより、モデル検査装置１は、ユーザが要望する検証対象の制約条件についてのモデル検査の結果だけを出力することが可能となる。このため、ユーザは、要望しない制約条件の検査結果をもチェックしなければならないという無駄を無くすことができる。これにより、ユーザによる検査結果確認の効率化を図ることができる。
【００３６】
また、この第１実施形態では、検証対象の制約条件（事前条件、事後条件、不変条件）が変更になった場合に、その検証対象の制約条件がモデル情報Ｄ１１に含まれていれば、ユーザは、そのモデル情報Ｄ１１の制約条件の中から、検証対象の制約条件を指定するだけでよいなる。つまり、この第１実施形態のモデル検査装置１は、検証対象の制約条件（事前条件、事後条件、不変条件）が変更になる度にモデル情報Ｄ１１を作成（変更）するというユーザの手間を軽減することができる。
【００３７】
（第２実施形態）
次に、本発明に係る第２実施形態を説明する。なお、この第２実施形態の説明において、第１実施形態と同様な構成部分には同一符号を付し、その共通部分の重複説明は省略する。
【００３８】
この第２実施形態では、第１実施形態のモデル検査装置１にモデル検査ツールとしてＳＰＩＮ（Simple Promela Interpreter）と呼ばれるコンピュータプログラムを用いる場合の具体例を示す。つまり、この第２実施形態では、モデル検査実行部１４は、ＳＰＩＮに従ってモデル検査を実行する。ＳＰＩＮには複数のバージョンがあり、何れのバージョンを採用してもよいが、この第２実施形態では、例えば、バージョン４．２．９を採用する場合について説明する。
【００３９】
この第２実施形態では、図３に示されるように、モデル情報Ｄ１１に含まれる各処理情報（メソッド情報）Ｐ1，・・・Ｐnの識別子ｄ１、変数名ｄ２、制約条件（事前条件、事後条件、不変条件）ｄ３は、クラス図Ｆcの態様を採る。図４はクラス図Ｆcの一例を示している。なお、この第２実施形態では、処理をメソッドともいう。
【００４０】
各メソッド情報Ｐ1，・・・Ｐnの動作仕様ｄ４は、アクティビティ図Ｆaの態様を採る。図５はアクティビティ図Ｆaの一例を示している。
【００４１】
モデル情報入力部１１は、上記のようなモデル情報Ｄ１１を受け付ける。
【００４２】
検証対象指定部１２は、例えば表示装置（図示せず）の画面（ディスプレイ）に、モデル情報Ｄ１１に含まれている全ての制約条件（事前条件、事後条件、不変条件）のリストを表示させる指示を出力する機能を備える。そのリストの一例として、ドロップダウンリストがある。
【００４３】
検証対象指定部１２は、その表示されたリスト中から入力装置４を利用して指定（選択）された検査対象の制約条件の情報を、指定情報として受け取る。
【００４４】
検証コード生成部１３は、モデル検査ツールＳＰＩＮの入力言語であるPromelaで記述された検証コードＤ１２（Promelaコード）を生成する。具体的には、検証コード生成部１３は、例えば次のように検証コードＤ１２を生成する。
【００４５】
すなわち、検証コード生成部１３は、モデル情報Ｄ１１におけるクラス図Ｆcで定義されている各クラスをそれぞれPromelaプロセスとして宣言する。また、検証コード生成部１３は、各メソッド（処理）の動作仕様ｄ４を各Promelaプロセスの動作として定義し、そのPromelaプロセスの動作にはそれぞれ各メソッドの識別子ｄ１を変換したラベルを付ける。さらに、検証コード生成部１３は、検証対象指定部１２による指定情報に基づいて、検証対象と判断された制約条件（事前条件、事後条件、不変条件）ｄ３を検証する検証コードＤ１２＿Ｃnを生成する。
【００４６】
さらに、検証コード生成部１３は、その検証コードＤ１２＿Ｃnを検証コードＤ１２＿Ｐnに挿入する。この挿入位置は、例えば、事前条件であればメソッドの最初の文の直前である。事後条件であればメソッドの最後の文の直後である。不変条件であればプロセスの外のグローバルな位置である。さらに、検証コード生成部１３は、各メソッドが参照する変数名ｄ２を変換しPromelaのグローバル変数として宣言する。図６はPromelaコード（検証コードＤ１２＿Ｐn）の一例を示す。この検証コードＤ１２＿Ｐnは、検証コード生成部１３が、図３に示すモデル情報Ｄ１１を、Promelaコードに変換したコードである。
【００４７】
この図６に示される検証コードＤ１２＿Ｐnは、メソッドＰnにおいて、事前条件も事後条件も不変条件も検証するコードである。これに対して、この第２実施形態では、例えば事前条件を反映しない（検証対象としない）場合には、検証コード生成部１３によって、図６における「事前条件を検証する文（始）」と「事前条件を検証する文（終）」で囲まれている部分Ｚが生成（挿入）されない。
【００４８】
検証結果出力部１５は、モデル検査実行部１４（ＳＰＩＮ）によるモデル検査の結果を示す情報を、出力装置５に出力する機能を有する。さらに、この第２実施形態では、検証結果出力部１５は、検証対象である制約条件（事前条件、事後条件、不変条件）が満たされない場合にその満たされないことを示す反例をシーケンス図で表示させる情報を出力装置５に出力する機能を備えている。図７はそのシーケンス図の一例を示している。この図７の例では、事前条件（precondition）が満たさないことを表している。
【００４９】
この第２実施形態のモデル検査装置１において、上記以外の構成は第１実施形態と同様である。また、第２実施形態のモデル検査装置１も、第１実施形態で述べた動作例（図２のフローチャートに示される動作例）と同様に動作する。
【００５０】
この第２実施形態のモデル検査装置１も、第１実施形態と同様に、検証対象判断部１６と検証コード変換部１７を有する検証コード生成部１３、および、検証対象指定部１２を備えているので、第１実施形態と同様の効果を得ることができる。
【００５１】
なお、この第２実施形態では、第１実施形態のモデル検査装置１にモデル検査ツールとしてＳＰＩＮを用いる例を示したが、第１実施形態のモデル検査装置１に採用されるモデル検査ツールはＳＰＩＮに限定されず、第１実施形態のモデル検査装置１にはＳＰＩＮ以外のモデル検査ツールを採用してもよい。
【００５２】
また、検証コード生成部１３が生成する検証コードは、図６の示す態様に限定されず、変換手法に応じた態様となる。
【００５３】
（第３実施形態）
次に、本発明に係る第３実施形態を説明する。なお、この第３実施形態の説明において、第１や第２の実施形態と同様の構成部分には同一符号を付し、その共通部分の重複説明は省略する。
【００５４】
図８は、本発明に係る第３実施形態のモデル検査装置の構成を簡略的に示すブロック図である。この第３実施形態のモデル検査装置３は、第１実施形態のモデル検査装置１の構成に加え、時相論理式生成部３２を備えている。この時相論理式生成部３２が検証対象判断部３５を有しており、検証コード生成部３３は検証対象判断部を有していない。
【００５５】
時相論理式生成部３２は、検証対象判断部３５と、時相論理式変換部３６とを有している。検証対象判断部３５は、モデル情報入力部１１で受け付けたモデル情報Ｄ１１に含まれている制約条件（事前条件、事後条件、不変条件）のそれぞれに関し、検証対象指定部１２による指定情報に基づいて時相論理式に反映（変換）するか否か（換言すれば、検証対象であるか否か）を判断する機能を備えている。
【００５６】
時相論理式変換部３６は、モデル情報Ｄ１１と、検証対象判断部３５の判断結果とに基づいて、時相論理式を生成する機能を備えている。つまり、時相論理式変換部３６は、モデル情報Ｄ１１に含まれる制約条件（事前条件、事後条件、不変条件）のそれぞれに関し、検証対象判断部３５により反映する（検証対象である）と判断された条件を、当該条件が満たされるか否かを検証する時相論理式に変換する。
【００５７】
検証コード生成部３３は、モデル情報Ｄ１１に基づいて、モデル検査実行部３４が実行可能な検証コードを生成する機能を備えている。この第３実施形態では、検証コード生成部３３は、モデル情報Ｄ１１に含まれている全ての制約条件（事前条件、事後条件、不変条件）を反映する検証コードを生成する。
【００５８】
モデル検査実行部３４は、検証コード生成部３３で生成された検証コードと、時相論理式生成部３２により生成された時相論理式に基づいて、モデル検査を実行する機能を備えている。
【００５９】
次に、モデル検査装置３の動作例を図９を利用して説明する。なお、図９は、モデル検査装置３が実行するモデル検査動作（処理）の一例を示すフローチャートであり、当該フローチャートは、モデル検査装置３の制御装置２が実行するコンピュータプログラム（ソフトウェア）の処理手順を表す。
【００６０】
モデル検査装置３が図９に示す動作を開始する際には、ユーザにより作成されたモデル情報Ｄ１１がモデル情報入力部１１で受け付けられ、また、ユーザにより指定された検証対象を示す指定情報が検証対象指定部１２で受け付けられた状態である。この状態において、モデル検査装置３の検証コード生成部３３（制御装置２）は、モデル情報Ｄ１１に基づいて検証コードＤ３１を生成する。つまり、検証コード生成部３３は、図９に示すステップＳ３０１〜Ｓ３０５の動作を行う。それら各ステップＳ３０１〜Ｓ３０５は、それぞれ、図２に示すステップＳ１０２〜Ｓ１０５，Ｓ１０９と同様の動作である。この第３実施形態では、検証コード生成部３３は、図２に示すステップＳ１０６〜Ｓ１０８の動作を行わない。
【００６１】
図９に示すステップＳ３０１〜Ｓ３０５の動作によって検証コードＤ３１が生成された以降に、検証対象判断部３５（制御装置２）が、モデル情報Ｄ１１に含まれている制約条件（事前条件、事後条件、不変条件）のそれぞれに関し、検証対象指定部１２による指定情報に基づいて、時相論理式に変換するか否かを判断する（ステップＳ３０６）。そして、時相論理式変換部３６（制御装置２）が、検証対象判断部３５の検査結果に基づき、変換すると判断された検証対象である制約条件（事前条件、事後条件、不変条件）を時相論理式Ｄ３２に変換する（ステップＳ３０７）。
【００６２】
その後、モデル検査実行部３４は、検証コードＤ３１において時相論理式Ｄ３２が満たされるか否かを検証するモデル検査を実行する（ステップＳ３０８）。然る後に、モデル検査実行部３４は、検証結果を生成し、その検査結果を検証結果出力部１５に出力する。検証結果出力部１５（制御装置２）は、その検証結果を、出力装置５に適合する形式の情報に変換して出力装置５に出力する（ステップＳ３０９）。これにより、モデル検査の結果が出力装置５によって出力されて、ユーザーは、モデル検査の結果を確認できる。
【００６３】
この第３実施形態のモデル検査装置３は、検証対象判断部３５を有する時相論理式生成部３２、および、検証対象指定部１２を備えているので、第１や第２の実施形態と同様の効果を得ることができる。つまり、検証コードおよび時相論理式を利用してモデル検査を実行するモデル検査装置３において、ユーザが要望（指定）する検証対象の制約条件のみの時相論理式を生成することができる。このため、モデル検査装置３は、モデル情報Ｄ１１に含まれている全ての制約条件ではなく、一部の制約条件についてモデル検査を実行できる。これにより、モデル検査装置３は、ユーザによる検査結果確認の効率化を図ることができる効果や、検証対象の制約条件（事前条件、事後条件、不変条件）が変更になる度にモデル情報Ｄ１１を作成（変更）するというユーザの手間を軽減できる効果を得ることができる。
【００６４】
（第４実施形態）
以下に、本発明に係る第４実施形態を説明する。なお、この第４実施形態の説明において、第１〜第３の実施形態と同様な構成部分には同一符号を付し、その共通部分の重複説明は省略する。
【００６５】
第４実施形態は、第３実施形態のモデル検査装置３にモデル検査ツールとしてＳＰＩＮ（コンピュータプログラム）を用いる場合の具体例を示す。
【００６６】
時相論理式生成部３２は、例えば図１０に示されるような時相論理式を生成する。図１０の例では、一つの処理（メソッド）において、事前条件も事後条件も不変条件も時相論理式に変換されている。これに対して、この第３実施形態では、時相論理式生成部３２は、検証対象判断部３５によって変換しないと判断された制約条件に関する時相論理式を生成しない。例えば、事後条件を検証しない場合には、図１０に示すＢ部分の時相論理式が生成されない。
【００６７】
検証コード生成部３３は、モデル情報Ｄ１１に含まれている全ての制約条件（事前条件、事後条件、不変条件）を反映した検証コードＤ３１を生成する。これ以外については、検証コード生成部３３は、第２実施形態で示した検証コード生成部１３とほぼ同様に検証コードＤ３１を生成する。つまり、検証コード生成部３３は、図３に示すモデル情報Ｄ１１におけるクラス図Ｆcで定義されている各クラスをそれぞれPromelaプロセスとして宣言する。また、検証コード生成部３３は、各メソッド（処理）の動作仕様ｄ４を各Promelaプロセスの動作として定義し、そのPromelaプロセスの動作にはそれぞれ各メソッドの識別子ｄ１を変換したラベルを付ける。さらに、検証コード生成部３３は、制約条件（事前条件、事後条件、不変条件）ｄ３が満たされているか否かを表す変数を宣言し、当該変数の値を変更するコードを生成する。
【００６８】
さらに、検証コード生成部３３は、そのコードを検証コードＤ３１＿Ｐnに挿入する。この挿入位置は、例えば、事前条件であればメソッドの最初の文の直前である。事後条件であればメソッドの最後の文の直後である。不変条件であればプロセスの外のグローバルな位置である。さらに、検証コード生成部３３は、各メソッドが参照する変数名ｄ２を変換しPromelaのグローバル変数として宣言する。このようにして、検証コード生成部３３は、検証コードＤ３１を生成する。
【００６９】
この第４実施形態のモデル検査装置３は、第３実施形態と同様の構成を備えているので、第３実施形態と同様の効果を得ることができる。
【００７０】
（その他の実施形態）
本発明は第１〜第４の各実施形態に限定されるものではなく、様々な実施の形態を採り得る。例えば、図１１は、本発明に係るその他の実施形態であるモデル検査装置の構成を簡略的に示すブロック図である。このモデル検査装置２０は、検証対象指定部２１と、検証対象判断部２２と、検証コード変換部２３と、モデル検査実行部２４とを有している。
【００７１】
検証対象指定部２１は、モデル検査で用いるモデル情報に含まれる制約条件である事前条件、事後条件、および、不変条件の中から、検証対象として指定された制約条件を示す指定情報を受け付ける機能を備えている。前述したように、事前条件とは、システムが行う処理、あるいは、ソフトウェアに基づいてコンピュータが実行する処理を開始する際に満たされるべき条件である。事後条件とは、前記処理が終了した際に満たされるべき条件である。不変条件とは、前記処理の実行中に満たされるべき条件である。
【００７２】
検証対象判断部２２は、前記モデル情報に含まれる前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、前記指定情報に基づいて、検証対象とするか否かを判断する機能を備えている。
【００７３】
検証コード変換部２３は、前記検証対象判断部２２によって検証対象であると判断された前記制約条件について前記モデル検査を実行する手順を示す検証コードを、前記モデル情報に基づき生成する機能を備えている。
【００７４】
モデル検査実行部２４は、前記検証コードに基づいてモデル検査を実行する機能を備えている。
【００７５】
このモデル検査装置２０においても、前記各実施形態と同様に、検証対象判断部２２を備え、当該検証対象判断部２２によって、モデル情報に含まれている前記事前条件と前記事後条件と前記不変条件とのそれぞれについて、検証対象とするか否かを判断できる構成を備えている。そして、モデル検査装置２０は、その検証対象と判断された制約条件に関するモデル検査を行うので、前記各実施形態と同様の効果を得ることができる。
【００７６】
なお、このモデル検査装置２０は、例えばコンピュータにより構成される。当該モデル検査装置２０（コンピュータ）は、記憶装置２６に格納されているコンピュータプログラム２７を読み出し、当該コンピュータプログラム２７に従って動作する。そのコンピュータプログラム２７は、コンピュータに、上記のような各構成部２１〜２４の機能を持たせるプログラムである。このコンピュータプログラム２７に従ってモデル検査装置２０が動作することによって、モデル検査装置２０は上記機能を持つことができる。
【００７７】
なお、モデル情報に含まれている処理情報には、制約条件として、事前条件と事後条件と不変条件の全てが必ず含まれるとは限らない。
【産業上の利用可能性】
【００７８】
本発明は、システム開発やソフトウェア開発における設計の妥当性を検証するツールとして有効である。
【符号の説明】
【００７９】
１，３，２０  モデル検査装置
１２，２１  検証対象指定部
１４，２４，３４  モデル検査実行部
１６，２２，３５  検証対象判断部
１７，２３  検証コード変換部
３６  時相論理式変換部
【図１】
2013045269.tif 000003
【図２】
2013045269.tif 000004
【図３】
2013045269.tif 000005
【図４】
2013045269.tif 000006
【図５】
2013045269.tif 000007
【図６】
2013045269.tif 000008
【図７】
2013045269.tif 000009
【図８】
2013045269.tif 000010
【図９】
2013045269.tif 000011
【図１０】
2013045269.tif 000012
【図１１】
2013045269.tif 000013
【図１２】
2013045269.tif 000014
【図１３】
2013045269.tif 000015