(57)【要約】【課題】入力モデルの作成を容易にして、モデル検証技術を熟知しない一般の設計者でもモデル検証を行えるようにする。【解決手段】検証装置２０において、ドメイン特化モデル（検証対象）生成部２４は、「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」に基づいて、特定のシステムの仕様をＵＭＬで記述したＵＭＬモデル１３（検証対象）から、当該システムの仕様をドメイン特化モデル文法に従って記述したドメイン特化モデル（検証対象）を生成する。モデル検証コード生成部２７は、「ドメイン特化モデルＴｏモデル検証コードマッピングルール」に基づいて、ドメイン特化モデル（検証対象）から、当該システムの仕様を記述したモデル検証コードを生成する。モデル検証実行部３０は、モデル検証コードを入力としてＳｐｉｎを実行し、当該システムの仕様の反例を示すデータを検証結果（反例）として取得する。【選択図】図１
2011180632.tif 000002
【特許請求の範囲】
【請求項１】
検証対象のシステムの仕様を記述したモデル検証コードを用いて特定のシステムの仕様を検証する検証装置であって、
任意のシステムの仕様を記述するために共通で用いられる汎用モデリング言語の要素と前記特定のシステムの仕様を記述するために用いられるドメイン特化モデリング言語の要素との対応関係を示す第１マッピング情報と、前記ドメイン特化モデリング言語の要素と前記モデル検証コードを構成する要素との対応関係を示す第２マッピング情報とを予め記憶装置に記憶するデータベースと、
前記特定のシステムの仕様を前記汎用モデリング言語で記述した第１汎用モデルデータの入力を入力装置で受け付け、前記データベースにより記憶された第１マッピング情報に基づいて、当該第１汎用モデルデータから、前記特定のシステムの仕様を前記ドメイン特化モデリング言語で記述した第１ドメイン特化モデルデータを処理装置で生成する第１ドメイン特化モデル生成部と、
前記データベースにより記憶された第２マッピング情報に基づいて、前記第１ドメイン特化モデル生成部により生成された第１ドメイン特化モデルデータから、前記特定のシステムの仕様を記述したモデル検証コードを処理装置で生成するモデル検証コード生成部と、
前記モデル検証コード生成部により生成されたモデル検証コードを用いて前記特定のシステムの仕様を処理装置で検証し、検証結果を示す検証結果データを取得するモデル検証実行部とを備えることを特徴とする検証装置。
【請求項２】
前記モデル検証実行部は、前記モデル検証コードに記述されたシステムの仕様の反例を検出するモデル検証ツールを処理装置で実行し、当該反例を示すデータを前記検証結果データとして取得することを特徴とする請求項１に記載の検証装置。
【請求項３】
前記データベースは、さらに、前記検証結果データを構成する要素と前記ドメイン特化モデリング言語の要素との対応関係を示す第３マッピング情報を予め記憶装置に記憶し、
前記検証装置は、さらに、
前記データベースにより記憶された第３マッピング情報に基づいて、前記モデル検証実行部により取得された検証結果データから、前記モデル検証ツールにより検出された反例を前記ドメイン特化モデリング言語で記述した第２ドメイン特化モデルデータを処理装置で生成する第２ドメイン特化モデル生成部と、
前記データベースにより記憶された第１マッピング情報に基づいて、前記第２ドメイン特化モデル生成部により生成された第２ドメイン特化モデルデータから、前記モデル検証ツールにより検出された反例を前記汎用モデリング言語で記述した第２汎用モデルデータを処理装置で生成する汎用モデル生成部とを備えることを特徴とする請求項２に記載の検証装置。
【請求項４】
前記モデル検証ツールは、Ｓｐｉｎであることを特徴とする請求項２又は３に記載の検証装置。
【請求項５】
前記汎用モデリング言語は、ＵＭＬ（Ｕｎｉｆｉｅｄ・Ｍｏｄｅｌｉｎｇ・Ｌａｎｇｕａｇｅ）であることを特徴とする請求項１から４までのいずれかに記載の検証装置。
【請求項６】
検証対象のシステムの仕様を記述したモデル検証コードを用いて特定のシステムの仕様を検証する検証方法であって、
任意のシステムの仕様を記述するために共通で用いられる汎用モデリング言語の要素と前記特定のシステムの仕様を記述するために用いられるドメイン特化モデリング言語の要素との対応関係を示す第１マッピング情報と、前記ドメイン特化モデリング言語の要素と前記モデル検証コードを構成する要素との対応関係を示す第２マッピング情報とを予め記憶装置に記憶するデータベースを備えるコンピュータが、前記特定のシステムの仕様を前記汎用モデリング言語で記述した第１汎用モデルデータの入力を入力装置で受け付け、前記データベースにより記憶された第１マッピング情報に基づいて、当該第１汎用モデルデータから、前記特定のシステムの仕様を前記ドメイン特化モデリング言語で記述した第１ドメイン特化モデルデータを処理装置で生成し、
前記コンピュータが、前記データベースにより記憶された第２マッピング情報に基づいて、生成した第１ドメイン特化モデルデータから、前記特定のシステムの仕様を記述したモデル検証コードを処理装置で生成し、
前記コンピュータが、生成したモデル検証コードを用いて前記特定のシステムの仕様を処理装置で検証し、検証結果を示す検証結果データを取得することを特徴とする検証方法。
【請求項７】
検証対象のシステムの仕様を記述したモデル検証コードを用いて特定のシステムの仕様を検証する検証プログラムであって、
任意のシステムの仕様を記述するために共通で用いられる汎用モデリング言語の要素と前記特定のシステムの仕様を記述するために用いられるドメイン特化モデリング言語の要素との対応関係を示す第１マッピング情報と、前記ドメイン特化モデリング言語の要素と前記モデル検証コードを構成する要素との対応関係を示す第２マッピング情報とを予め記憶装置に記憶するデータベースを備えるコンピュータにより実行され、
前記特定のシステムの仕様を前記汎用モデリング言語で記述した第１汎用モデルデータの入力を入力装置で受け付け、前記データベースにより記憶された第１マッピング情報に基づいて、当該第１汎用モデルデータから、前記特定のシステムの仕様を前記ドメイン特化モデリング言語で記述した第１ドメイン特化モデルデータを処理装置で生成する第１ドメイン特化モデル生成処理と、
前記データベースにより記憶された第２マッピング情報に基づいて、前記第１ドメイン特化モデル生成処理により生成された第１ドメイン特化モデルデータから、前記特定のシステムの仕様を記述したモデル検証コードを処理装置で生成するモデル検証コード生成処理と、
前記モデル検証コード生成処理により生成されたモデル検証コードを用いて前記特定のシステムの仕様を処理装置で検証し、検証結果を示す検証結果データを取得するモデル検証実行処理とを前記コンピュータに実行させることを特徴とする検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、検証装置及び検証方法及び検証プログラムに関するものである。本発明は、特に、設計モデル検証方式に関するものである。
【背景技術】
【０００２】
従来、Ｓｐｉｎ等のモデル検証ツール（「モデル検査ツール」ともいう）による設計仕様の検証では、設計者がモデル検証ツールの記述文法に従って振舞いの仕様をコード化することで、モデル検証を行っている。しかし、ツール独自の記述文法を理解して厳密にコード化するのは、一般の設計者にとっては非常に困難である。そのため、独自の図形式（独自モデル）により振舞いを記述することで、記述容易性を向上させる技術がある（例えば、特許文献１参照）。また、ＵＭＬ（Ｕｎｉｆｉｅｄ・Ｍｏｄｅｌｉｎｇ・Ｌａｎｇｕａｇｅ）モデルからツールの記述文法に則ったモデル検証コードを生成する技術がある（例えば、非特許文献１参照）。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２００８−３０５０７９号公報
【非特許文献】
【０００４】
【非特許文献１】吉岡信和、青木利晃、田原康之著、「ＳＰＩＮによる設計モデル検証」、近代科学社、２００８年９月３０日、ｐｐ．２１８〜２２３
【発明の概要】
【発明が解決しようとする課題】
【０００５】
従来、モデル検証ツールによる設計仕様の検証において、一般の設計者がモデル検証ツールに依存した記述文法に従い、振舞いの仕様をコード化することは困難であるため、上記の独自モデルやＵＭＬモデルを利用した技術によって、コード（「モデル検証コード」ともいう）を生成し、このコードをモデル検証ツールに入力してモデル検証を実行させている。しかし、上記の独自モデルを利用した技術では、独自の図形式の仕様を理解する必要があるため、導入の際、設計者のイニシャルコストが大きいという課題があった。また、上記のＵＭＬモデルを利用した技術では、ＵＭＬが汎用的過ぎるため、ある特定分野においてサブセット化できる共通的な記述をその都度最初から記述しなければならなく、冗長であるという課題があった。
【０００６】
また、モデル検証ツールにより検証結果として出力される反例（例えば、デッドロック）のモデルは、モデル検証コードレベルのデータやモデル検証ツールの内部用データを含んでいるため、出力される反例のモデル要素と入力モデル（上記の独自モデルやＵＭＬモデル）の要素が対応しておらず、出力モデルの意味解析が困難であるという課題があった。
【０００７】
これらの課題を乗り越えるにはモデル検証に関する知識や経験が必要とされるため、開発現場へのモデル検証技術の導入は、難しいのが現状である。
【０００８】
本発明は、例えば、入力モデルの作成又は出力される反例モデルの意味解析を容易にして、モデル検証技術を熟知しない一般の設計者でもモデル検証を行えるようにすることを目的とする。
【課題を解決するための手段】
【０００９】
本発明の一の態様に係る検証装置は、
検証対象のシステムの仕様を記述したモデル検証コードを用いて特定のシステムの仕様を検証する検証装置であって、
任意のシステムの仕様を記述するために共通で用いられる汎用モデリング言語の要素と前記特定のシステムの仕様を記述するために用いられるドメイン特化モデリング言語の要素との対応関係を示す第１マッピング情報と、前記ドメイン特化モデリング言語の要素と前記モデル検証コードを構成する要素との対応関係を示す第２マッピング情報とを予め記憶装置に記憶するデータベースと、
前記特定のシステムの仕様を前記汎用モデリング言語で記述した第１汎用モデルデータの入力を入力装置で受け付け、前記データベースにより記憶された第１マッピング情報に基づいて、当該第１汎用モデルデータから、前記特定のシステムの仕様を前記ドメイン特化モデリング言語で記述した第１ドメイン特化モデルデータを処理装置で生成する第１ドメイン特化モデル生成部と、
前記データベースにより記憶された第２マッピング情報に基づいて、前記第１ドメイン特化モデル生成部により生成された第１ドメイン特化モデルデータから、前記特定のシステムの仕様を記述したモデル検証コードを処理装置で生成するモデル検証コード生成部と、
前記モデル検証コード生成部により生成されたモデル検証コードを用いて前記特定のシステムの仕様を処理装置で検証し、検証結果を示す検証結果データを取得するモデル検証実行部とを備えることを特徴とする。
【発明の効果】
【００１０】
本発明の一の態様において、検証装置の第１ドメイン特化モデル生成部は、特定のシステムの仕様を汎用モデリング言語で記述した第１汎用モデルデータの入力を受け付け、第１マッピング情報に基づいて、当該第１汎用モデルデータから、上記特定のシステムの仕様をドメイン特化モデリング言語で記述した第１ドメイン特化モデルデータを生成する。検証装置のモデル検証コード生成部は、第２マッピング情報に基づいて、当該第１ドメイン特化モデルデータから、上記特定のシステムの仕様を記述したモデル検証コードを生成する。検証装置のモデル検証実行部は、当該モデル検証コードを用いて上記特定のシステムの仕様を検証し、検証結果を示す検証結果データを取得する。これにより、入力モデルの作成が容易になるため、モデル検証技術を熟知しない一般の設計者でもモデル検証を行えるようになる。
【図面の簡単な説明】
【００１１】
【図１】実施の形態１に係る設計モデル検証方式の構成図である。
【図２】実施の形態１に係るドメイン特化モデルのメタモデルを示す図である。
【図３】実施の形態１に係るドメイン特化モデル文法と各マッピングルールの関係を示す図である。
【図４】実施の形態１に係る「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」の（ａ）スキーマ、（ｂ）テーブルデータの一例を示す表である。
【図５】実施の形態１に係る「ドメイン特化モデルＴｏモデル検証コードマッピングルール」の（ａ）スキーマ、（ｂ）テーブルデータの一例を示す表である。
【図６】実施の形態１に係る「検証結果Ｔｏドメイン特化モデルマッピングルール」の（ａ）スキーマ、（ｂ）テーブルデータの一例を示す表である。
【図７】実施の形態１に係る「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」の（ａ）スキーマ、（ｂ）テーブルデータの一例を示す表である。
【図８】実施の形態１に係る検証装置のハードウェア構成の一例を示す図である。
【図９】実施の形態１に係るドメイン特化モデル文法の例を示すクラス図である。
【図１０】実施の形態１に係るドメイン特化モデル文法の例を示すコンポジット構造図である。
【図１１】実施の形態１に係る「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」の例を示す表である。
【図１２】実施の形態１に係る「ドメイン特化モデルＴｏモデル検証コードマッピングルール」の例を示す表である。
【図１３】実施の形態１に係る「検証結果Ｔｏドメイン特化モデルマッピングルール」の例を示す表である。
【図１４】実施の形態１に係る「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」の例を示す表である。
【図１５】実施の形態１に係る検証装置全体の動作を示すフローチャートである。
【図１６】実施の形態１に係るＵＭＬモデル（検証対象）の例を示すクラス図である。
【図１７】実施の形態１に係るＵＭＬモデル（検証対象）の例を示すアクティビティ図である。
【図１８】実施の形態１に係るＵＭＬモデル（検証対象）の例を示すアクティビティ図である。
【図１９】図１５のステップＳ１０１の詳細な処理を示すフローチャートである。
【図２０】実施の形態１に係る１段階目のドメイン特化モデル（検証対象）の一例を示す図である。
【図２１】実施の形態１に係る１段階目のドメイン特化モデル（検証対象）の一例を示す図である。
【図２２】実施の形態１に係る２段階目のドメイン特化モデル（検証対象）の一例を示す図である。
【図２３】実施の形態１に係る２段階目のドメイン特化モデル（検証対象）の一例を示す図である。
【図２４】実施の形態１に係るモデル検証コードの一例を示す図である。
【図２５】実施の形態１に係る検証結果（反例）の一例を示す図である。
【図２６】図１５のステップＳ１０４の詳細な処理を示すフローチャートである。
【図２７】実施の形態１に係る１段階目のドメイン特化モデル（反例）の一例を示す図である。
【図２８】実施の形態１に係る２段階目のドメイン特化モデル（反例）の一例を示す図である。
【図２９】実施の形態１に係るＵＭＬモデル（反例）の一例を示す図である。
【発明を実施するための形態】
【００１２】
以下、本発明の実施の形態について、図を用いて説明する。
【００１３】
実施の形態１．
図１は、本実施の形態に係る、入力モデルの作成と出力された反例結果の解析を容易にする設計モデル検証方式１０の構成図である。
【００１４】
図１において、ＳＥ１１（システムエンジニア）はシステム開発の設計者である。ドメインエンジニア１２はドメイン特化モデル文法と４種類のマッピングルールの作成者であり、ＵＭＬ文法とドメイン、モデル検証コード記述文法の有識者である。
【００１５】
ＵＭＬモデル１３（検証対象）は、検証したい仕様をドメイン特化モデル文法に則り、ＳＥ１１がモデル化したもので、検証装置２０の入力となる。ＵＭＬモデル１３（検証対象）は、特定のシステムの仕様を汎用モデリング言語（「仕様記述言語」ともいう）で記述した第１汎用モデルデータの一例である。なお、汎用モデリング言語は、任意のシステムの仕様を記述するために共通で用いられる言語である。本実施の形態では、汎用モデリング言語の一例としてＵＭＬを用いるが、他の汎用モデリング言語を用いても構わない。
【００１６】
検証装置２０は、ＵＭＬ文法のＤＢ２１（データベース）、ドメイン特化モデル文法のＤＢ２２、モデル検証コード記述文法のＤＢ２３、ドメイン特化モデル（検証対象）生成部２４、「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」のＤＢ２５、ドメイン特化モデル（検証対象）のＤＢ２６、モデル検証コード生成部２７、「ドメイン特化モデルＴｏモデル検証コードマッピングルール」のＤＢ２８、モデル検証コードのＤＢ２９、モデル検証実行部３０、検証結果（反例）のＤＢ３１、ドメイン特化モデル（反例）生成部３２、「検証結果Ｔｏドメイン特化モデルマッピングルール」のＤＢ３３、ドメイン特化モデル（反例）のＤＢ３４、ＵＭＬモデル（反例）生成部３５、「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」のＤＢ３６を備える。
【００１７】
また、図示していないが、検証装置２０は、処理装置、記憶装置、入力装置、出力装置等のハードウェアを備える。ハードウェアは検証装置２０の各部によって利用される。例えば、処理装置は、検証装置２０の各部でデータや情報の演算、加工、読み取り、書き込み等を行うために利用される。記憶装置は、そのデータや情報を記憶するために、入力装置は、そのデータや情報を入力するために、出力装置は、そのデータや情報を出力するために利用される。記憶装置は、特に、それぞれのＤＢ２１，２２，２３，２５，２６，２８，２９，３１，３３，３４，３６でデータを格納するために利用される。
【００１８】
検証装置２０は、ＳＥ１１によって定義された検証対象のＵＭＬモデル１３が入力されると、以下のように各部を動作させて反例のＵＭＬモデル１４を出力する。
【００１９】
まず、ドメイン特化モデル（検証対象）生成部２４が、ＵＭＬモデルとドメイン特化モデルのマッピングルールである「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」を用いてＵＭＬモデル１３（検証対象）をドメイン特化モデル（検証対象）へ変換する。ドメイン特化モデル（検証対象）は、第１汎用モデルデータに記述された特定のシステムの仕様をドメイン特化モデリング言語（「ドメイン固有モデリング言語」ともいう）で記述した第１ドメイン特化モデルデータの一例である。なお、ドメイン特化モデリング言語は、前述した汎用モデリング言語と異なり、特定のシステムの仕様を記述するために用いられる言語である。
【００２０】
次に、モデル検証コード生成部２７が、ドメイン特化モデルとモデル検証コードのマッピングルールである「ドメイン特化モデルＴｏモデル検証コードマッピングルール」を用いてドメイン特化モデル（検証対象）をモデル検証コードへ変換する。モデル検証コードは、第１ドメイン特化モデルデータに記述された特定のシステムの仕様を、モデル検証ツール（例えば、Ｓｐｉｎ）が解釈可能な言語（例えば、Ｐｒｏｍｅｌａ）で記述したものである。モデル検証ツールは、モデル検証コードが入力されると、モデル検証コードに記述された検証対象のシステムの仕様を検証し、その仕様の反例を検出して出力するプログラムである。
【００２１】
次に、モデル検証実行部３０が、生成されたモデル検証コードを入力としてモデル検証を行うことにより検証結果（反例）を出力する。このとき、モデル検証実行部３０によってモデル検証ツールが実行され、検証結果（反例）を示す検証結果データが取得される。
【００２２】
次に、ドメイン特化モデル（反例）生成部３２が、検証結果とドメイン特化モデルのマッピングルールである「検証結果Ｔｏドメイン特化モデルマッピングルール」を用いて検証結果（反例）をドメイン特化モデル（反例）へ変換する。ドメイン特化モデル（反例）は、モデル検証ツールにより検出された反例をドメイン特化モデリング言語で記述した第２ドメイン特化モデルデータの一例である。
【００２３】
最後に、ＵＭＬモデル（反例）生成部３５が、ドメイン特化モデルとＵＭＬモデルのマッピングルールである「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」を用いてドメイン特化モデル（反例）をＵＭＬモデル１４（反例）へ変換する。ＵＭＬモデル１４（反例）は、モデル検証ツールにより検出された反例を汎用モデリング言語で記述した第２汎用モデルデータの一例である。
【００２４】
ＵＭＬ文法のＤＢ２１は、ＵＭＬの記述仕様を定義したデータ（ＵＭＬメタモデル）を格納するＤＢである。ＵＭＬメタモデル（ＵＭＬ文法）は、ＯＭＧ（Ｏｂｊｅｃｔ・Ｍａｎａｇｅｍｅｎｔ・Ｇｒｏｕｐ）が策定したものである。
【００２５】
ドメイン特化モデル文法のＤＢ２２は、各ドメインのドメイン特化モデル（「ドメイン固有モデル」ともいう）の記述仕様（メタモデル）を格納するＤＢである。ドメイン特化モデルのメタモデル（ドメイン特化モデル文法）はＵＭＬメタモデル（ＵＭＬ文法）を拡張したものであり、ドメインエンジニア１２が予め定義しておくものである。ここで、図２にドメイン特化モデルのメタモデルを示す。図２において、ドメイン特化モデルのメタモデルのＳＥ記述構成要素とＳＥ記述振舞い要素はＳＥ１１が入力のモデル（検証対象）を定義する際の要素を意味する。暗黙的構成要素と暗黙的振舞い要素はドメイン特化モデル（検証対象）生成部２４とドメイン特化モデル（反例）生成部３２においてドメイン特化モデルへの変換を行う際にドメイン特化モデルに追加する要素であり、ＳＥ１１が入力モデルを定義する際には使用しない要素である。つまり、暗黙的構成要素と暗黙的振舞い要素はドメインにてサブセット化される要素であり、ＵＭＬで定義する必要のない要素である。これらのＳＥ記述構成要素、ＳＥ記述振舞い要素、暗黙的構成要素、暗黙的振舞い要素は、ドメイン特化モデル（検証対象）で使われる要素である。動作要素は、ドメイン特化モデル（反例）で使われる要素である。ドメイン特化モデル（反例）では、他に、ＳＥ記述構成要素、ＳＥ記述振舞い要素、暗黙的構成要素、暗黙的振舞い要素が使われる。なお、ドメイン特化モデル（反例）生成部３２が検証結果をドメイン特化モデル（反例）に変換する際、「検証結果Ｔｏドメイン特化モデルマッピングルール」の参照による変換だけではドメイン特化モデル（反例）のモデル要素が不足し、出力モデルの要素が入力モデルの要素と対応しない。そのため、ドメイン特化モデル（反例）生成部３２は、ドメイン特化モデル文法においてドメイン特化モデルのメタモデルの検証トレースに相当する関連と、不足する要素との関連から、別の要素との関連を辿ることで、不足する要素を特定し、補足するようにしている。
【００２６】
ドメイン特化モデル文法を定義する際に、ドメインエンジニア１２は併せて、４種類のマッピングルール（「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」、「ドメイン特化モデルＴｏモデル検証コードマッピングルール」、「検証結果Ｔｏドメイン特化モデルマッピングルール」、「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」）も定義する。ここで、図３にドメイン特化モデル文法と各マッピングルールの関係を示す。図３において、「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」と「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」は、ＵＭＬ文法の要素とドメイン特化モデル文法の要素との対応を定義したマッピングルールである。「ドメイン特化モデルＴｏモデル検証コードマッピングルール」と「検証結果Ｔｏドメイン特化モデルマッピングルール」は、ドメイン特化モデル文法の要素とモデル検証コード記述文法の要素との対応を定義したマッピングルールである。
【００２７】
上記４種類のマッピングルールのうち、「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」と「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」は、汎用モデリング言語の要素とドメイン特化モデリング言語の要素との対応関係を示す第１マッピング情報の一例である。「ドメイン特化モデルＴｏモデル検証コードマッピングルール」は、ドメイン特化モデリング言語の要素とモデル検証コードを構成する要素との対応関係を示す第２マッピング情報の一例である。「検証結果Ｔｏドメイン特化モデルマッピングルール」は、検証結果データを構成する要素とドメイン特化モデリング言語の要素との対応関係を示す第３マッピング情報の一例である。各マッピングルールは、ＤＢ２５，２８，３３，３６によって予め記憶装置に記憶される。
【００２８】
モデル検証コード記述文法のＤＢ２３は、モデル検証ツールが解釈可能なプログラムの記述文法と検証結果の仕様を定義したものを格納するＤＢである。モデル検証を行うには、この記述文法に則って検証対象となるモデル（仕様）をコード化し、モデル検証実行部３０に入力する。
【００２９】
ドメイン特化モデル（検証対象）生成部２４は、入力されたＵＭＬモデル１３（検証対象）のドメインに対応する「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」のマッピングルールとドメイン特化モデル文法を参照し、ＵＭＬモデル１３（検証対象）をドメイン特化モデル（検証対象）に変換する。ドメイン特化モデル（検証対象）生成部２４は、第１ドメイン特化モデル生成部の一例である。
【００３０】
「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」のＤＢ２５は、ＵＭＬモデルとドメイン特化モデルのマッピングルールを格納したＤＢである。ここで、図４の（ａ）に「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」のスキーマを示す。「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」のＤＢ２５には、例えば図４の（ｂ）に示すようなテーブルデータが格納される。このマッピングルールは、ドメインエンジニア１２がＵＭＬ文法とドメイン特化モデル文法を参照して、予め定義して格納しておく。
【００３１】
ドメイン特化モデル（検証対象）のＤＢ２６は、ドメイン特化モデル（検証対象）生成部２４により生成される検証対象のドメイン特化モデルを、モデル検証コード生成部２７がロードするまで一時的に格納するＤＢである。
【００３２】
モデル検証コード生成部２７は、ドメイン特化モデル（検証対象）のドメインに対応する「ドメイン特化モデルＴｏモデル検証コードマッピングルール」のマッピングルールを参照し、ドメイン特化モデル（検証対象）をモデル検証コードに変換する。
【００３３】
「ドメイン特化モデルＴｏモデル検証コードマッピングルール」のＤＢ２８は、ドメイン特化モデル（検証対象）とモデル検証コードのマッピングルールを格納したＤＢである。ここで、図５の（ａ）に「ドメイン特化モデルＴｏモデル検証コードマッピングルール」のスキーマを示す。「ドメイン特化モデルＴｏモデル検証コードマッピングルール」のＤＢ２８には、例えば図５の（ｂ）に示すようなテーブルデータが格納される。このマッピングルールは、ドメインエンジニア１２がドメイン特化モデル文法とモデル検証コード記述文法を参照して、予め定義して格納しておく。
【００３４】
モデル検証コードのＤＢ２９は、モデル検証コード生成部２７により生成されるモデル検証コードを、モデル検証実行部３０がロードするまで一時的に格納するＤＢである。なお、モデル検証コードとは、モデル検証ツールが解釈可能なコードにより記述されたプログラムである。
【００３５】
モデル検証実行部３０は、Ｓｐｉｎ等、既存のモデル検証ツールのコマンドを実行する部分であり、モデル検証コードのＤＢ２９よりロードしたモデル検証コードを入力として、検証結果（反例）を出力する。
【００３６】
検証結果（反例）のＤＢ３１は、モデル検証実行部３０から出力される検証結果（反例）を、ドメイン特化モデル（反例）生成部３２がロードするまで一時的に格納するＤＢである。
【００３７】
ドメイン特化モデル（反例）生成部３２は、検証結果（反例）のドメインに対応する「検証結果Ｔｏドメイン特化モデルマッピングルール」のマッピングルールとドメイン特化モデル文法を参照し、検証結果（反例）をドメイン特化モデル（反例）に変換する。ドメイン特化モデル（反例）生成部３２は、第２ドメイン特化モデル生成部の一例である。
【００３８】
「検証結果Ｔｏドメイン特化モデルマッピングルール」のＤＢ３３は、検証結果とドメイン特化モデルのマッピングルールを格納したＤＢである。ここで、図６の（ａ）に「検証結果Ｔｏドメイン特化モデルマッピングルール」のスキーマを示す。「検証結果Ｔｏドメイン特化モデルマッピングルール」のＤＢ３３には、例えば図６の（ｂ）に示すようなテーブルデータが格納される。このマッピングルールは、ドメインエンジニア１２がモデル検証コード記述文法とドメイン特化モデル文法を参照して、予め定義して格納しておく。
【００３９】
ドメイン特化モデル（反例）のＤＢ３４は、ドメイン特化モデル（反例）生成部３２により生成されるドメイン特化モデル（反例）を、ＵＭＬモデル（反例）生成部３５がロードするまで一時的に格納するＤＢである。
【００４０】
ＵＭＬモデル（反例）生成部３５は、ドメイン特化モデル（反例）のドメインに対応する「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」のマッピングルールを参照し、ドメイン特化モデル（反例）をＵＭＬモデル１４（反例）に変換する。ＵＭＬモデル（反例）生成部３５は、汎用モデル生成部の一例である。
【００４１】
「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」のＤＢ３６は、ドメイン特化モデルとＵＭＬモデルのマッピングルールを格納したＤＢである。ここで、図７の（ａ）に「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」のスキーマを示す。「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」のＤＢ３６には、例えば図７の（ｂ）に示すようなテーブルデータが格納される。このマッピングルールは、ドメインエンジニア１２がドメイン特化モデル文法とＵＭＬ文法を参照して、予め定義して格納しておく。
【００４２】
ＵＭＬモデル１４（反例）は、ＵＭＬモデル（反例）生成部３５により生成される反例のＵＭＬモデルである。
【００４３】
このように、本実施の形態に係る設計モデル検証方式１０では、ドメイン特化モデル文法をベースにしてＳＥ１１が記述したＵＭＬモデル１３（検証対象）と検証したい性質を定義した制約を入力として反例のＵＭＬモデル１４を生成する。
【００４４】
図８は、検証装置２０のハードウェア構成の一例を示す図である。
【００４５】
図８において、検証装置２０は、コンピュータであり、ＬＣＤ９０１（Ｌｉｑｕｉｄ・Ｃｒｙｓｔａｌ・Ｄｉｓｐｌａｙ）、キーボード９０２（Ｋ／Ｂ）、マウス９０３、ＦＤＤ９０４（Ｆｌｅｘｉｂｌｅ・Ｄｉｓｋ・Ｄｒｉｖｅ）、ＣＤＤ９０５（Ｃｏｍｐａｃｔ・Ｄｉｓｃ・Ｄｒｉｖｅ）、プリンタ９０６といったハードウェアデバイスを備えている。これらのハードウェアデバイスはケーブルや信号線で接続されている。ＬＣＤ９０１の代わりに、ＣＲＴ（Ｃａｔｈｏｄｅ・Ｒａｙ・Ｔｕｂｅ）、あるいは、その他の表示装置が用いられてもよい。マウス９０３の代わりに、タッチパネル、タッチパッド、トラックボール、ペンタブレット、あるいは、その他のポインティングデバイスが用いられてもよい。
【００４６】
検証装置２０は、プログラムを実行するＣＰＵ９１１（Ｃｅｎｔｒａｌ・Ｐｒｏｃｅｓｓｉｎｇ・Ｕｎｉｔ）を備えている。ＣＰＵ９１１は、処理装置の一例である。ＣＰＵ９１１は、バス９１２を介してＲＯＭ９１３（Ｒｅａｄ・Ｏｎｌｙ・Ｍｅｍｏｒｙ）、ＲＡＭ９１４（Ｒａｎｄｏｍ・Ａｃｃｅｓｓ・Ｍｅｍｏｒｙ）、通信ボード９１５、ＬＣＤ９０１、キーボード９０２、マウス９０３、ＦＤＤ９０４、ＣＤＤ９０５、プリンタ９０６、ＨＤＤ９２０（Ｈａｒｄ・Ｄｉｓｋ・Ｄｒｉｖｅ）と接続され、これらのハードウェアデバイスを制御する。ＨＤＤ９２０の代わりに、フラッシュメモリ、光ディスク装置、メモリカードリーダライタ又はその他の記憶媒体が用いられてもよい。
【００４７】
ＲＡＭ９１４は、揮発性メモリの一例である。ＲＯＭ９１３、ＦＤＤ９０４、ＣＤＤ９０５、ＨＤＤ９２０は、不揮発性メモリの一例である。これらは、記憶装置の一例である。通信ボード９１５、キーボード９０２、マウス９０３、ＦＤＤ９０４、ＣＤＤ９０５は、入力装置の一例である。また、通信ボード９１５、ＬＣＤ９０１、プリンタ９０６は、出力装置の一例である。
【００４８】
通信ボード９１５は、ＬＡＮ（Ｌｏｃａｌ・Ａｒｅａ・Ｎｅｔｗｏｒｋ）等に接続されている。通信ボード９１５は、ＬＡＮに限らず、ＩＰ−ＶＰＮ（Ｉｎｔｅｒｎｅｔ・Ｐｒｏｔｏｃｏｌ・Ｖｉｒｔｕａｌ・Ｐｒｉｖａｔｅ・Ｎｅｔｗｏｒｋ）、広域ＬＡＮ、ＡＴＭ（Ａｓｙｎｃｈｒｏｎｏｕｓ・Ｔｒａｎｓｆｅｒ・Ｍｏｄｅ）ネットワークといったＷＡＮ（Ｗｉｄｅ・Ａｒｅａ・Ｎｅｔｗｏｒｋ）、あるいは、インターネットに接続されていても構わない。ＬＡＮ、ＷＡＮ、インターネットは、ネットワークの一例である。
【００４９】
ＨＤＤ９２０には、オペレーティングシステム９２１（ＯＳ）、ウィンドウシステム９２２、プログラム群９２３、ファイル群９２４が記憶されている。プログラム群９２３のプログラムは、ＣＰＵ９１１、オペレーティングシステム９２１、ウィンドウシステム９２２により実行される。プログラム群９２３には、本実施の形態の説明において「〜部」として説明する機能を実行するプログラムが含まれている。プログラムは、ＣＰＵ９１１により読み出され実行される。ファイル群９２４には、本実施の形態の説明において、「〜データ」、「〜情報」、「〜ＩＤ（識別子）」、「〜フラグ」、「〜結果」として説明するデータや情報や信号値や変数値やパラメータが、「〜ファイル」や「〜データベース」や「〜テーブル」の各項目として含まれている。「〜ファイル」や「〜データベース」や「〜テーブル」は、ＲＡＭ９１４やＨＤＤ９２０等の記憶媒体に記憶される。ＲＡＭ９１４やＨＤＤ９２０等の記憶媒体に記憶されたデータや情報や信号値や変数値やパラメータは、読み書き回路を介してＣＰＵ９１１によりメインメモリやキャッシュメモリに読み出され、抽出、検索、参照、比較、演算、計算、制御、出力、印刷、表示といったＣＰＵ９１１の処理（動作）に用いられる。抽出、検索、参照、比較、演算、計算、制御、出力、印刷、表示といったＣＰＵ９１１の処理中、データや情報や信号値や変数値やパラメータは、メインメモリやキャッシュメモリやバッファメモリに一時的に記憶される。
【００５０】
本実施の形態の説明において用いるブロック図やフローチャートの矢印の部分は主としてデータや信号の入出力を示す。データや信号は、ＲＡＭ９１４等のメモリ、ＦＤＤ９０４のフレキシブルディスク（ＦＤ）、ＣＤＤ９０５のコンパクトディスク（ＣＤ）、ＨＤＤ９２０の磁気ディスク、光ディスク、ＤＶＤ（Ｄｉｇｉｔａｌ・Ｖｅｒｓａｔｉｌｅ・Ｄｉｓｃ）、あるいは、その他の記録媒体に記録される。また、データや信号は、バス９１２、信号線、ケーブル、あるいは、その他の伝送媒体により伝送される。
【００５１】
本実施の形態の説明において「〜部」として説明するものは、「〜回路」、「〜装置」、「〜機器」であってもよく、また、「〜ステップ」、「〜工程」、「〜手順」、「〜処理」であってもよい。即ち、「〜部」として説明するものは、ＲＯＭ９１３に記憶されたファームウェアで実現されていても構わない。あるいは、「〜部」として説明するものは、ソフトウェアのみ、あるいは、素子、デバイス、基板、配線といったハードウェアのみで実現されていても構わない。あるいは、「〜部」として説明するものは、ソフトウェアとハードウェアとの組み合わせ、あるいは、ソフトウェアとハードウェアとファームウェアとの組み合わせで実現されていても構わない。ファームウェアとソフトウェアは、プログラムとして、フレキシブルディスク、コンパクトディスク、磁気ディスク、光ディスク、ＤＶＤ等の記録媒体に記憶される。プログラムはＣＰＵ９１１により読み出され、ＣＰＵ９１１により実行される。即ち、プログラムは、本実施の形態の説明で述べる「〜部」としてコンピュータを機能させるものである。あるいは、プログラムは、本実施の形態の説明で述べる「〜部」の手順や方法をコンピュータに実行させるものである。
【００５２】
以下、検証装置２０の動作（本実施の形態に係る検証方法、本実施の形態に係る検証プログラムの処理手順）について、下記のプリンタ・スキャナの獲得仕様を例にして説明する。なお、本例では、モデル検証ツールとしてＳｐｉｎを用いることを想定しているが、他のモデル検証ツールを用いても構わない。
【００５３】
プリンタ・スキャナの獲得の際の振舞い仕様（獲得仕様）：ユーザＡとユーザＢがプリンタとスキャナの２つの資源を使って作業をする。ユーザＡとユーザＢがプリンタとスキャナを利用する手順は下記の通りとする。なお、一方が獲得しようとした資源を既に他方が獲得している場合は、その資源がリリースされてフリー状態になるまで待つ。
・ユーザＡは、プリンタ→スキャナの順に資源を獲得し、２つの資源を同時に利用した後、プリンタ→スキャナの順に資源を解放する。
・ユーザＢは、スキャナ→プリンタの順に資源を獲得し、２つの資源を同時に利用した後、プリンタ→スキャナの順に資源を解放する。
【００５４】
プリンタ・スキャナの獲得仕様のドメインを“共有資源獲得”とした場合の、共有資源獲得用のドメイン特化モデル文法の例を図９、図１０に示す。ドメイン特化モデル文法のＤＢ２２には、例えば図９のクラス図、図１０のコンポジット構造図で定義されるメタモデルデータが格納される。また、共有資源獲得用のドメイン特化モデル文法に対応する４種類のマッピングルールの例を図１１〜図１４に示す。「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」のＤＢ２５には、例えば図１１に示すようなテーブルデータが格納される。「ドメイン特化モデルＴｏモデル検証コードマッピングルール」のＤＢ２８には、例えば図１２に示すようなテーブルデータが格納される。「検証結果Ｔｏドメイン特化モデルマッピングルール」のＤＢ３３には、例えば図１３に示すようなテーブルデータが格納される。「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」のＤＢ３６には、例えば図１４に示すようなテーブルデータが格納される。各マッピングルールは、定義されたドメイン特化モデル文法とＵＭＬ文法、モデル検証コード記述文法から作成される。
【００５５】
図１５は、検証装置２０全体の動作を示すフローチャートである。
【００５６】
まずＳＥ１１が、検証したい仕様に関わるドメインのドメイン特化モデル文法を参照し、その文法に則ってＵＭＬモデル１３（検証対象）を定義し、ドメイン特化モデル（検証対象）生成部２４に入力する。プリンタ・スキャナの資源獲得仕様の場合のＵＭＬモデル１３（検証対象）を図１６〜図１８に示す。ＳＥ１１は、例えば図１６のクラス図、図１７のユーザＡのアクティビティ図、図１８のユーザＢのアクティビティ図で定義されるＵＭＬモデル１３（検証対象）を入力する。
【００５７】
図１６に示すように、このＵＭＬモデル１３（検証対象）は、要素として、ユーザＡ（ＵｓｅｒＡ）やユーザＢ（ＵｓｅｒＢ）を含んでいる。また、図１７及び図１８に示すように、このＵＭＬモデル１３（検証対象）は、要素として、プリンタ（ｐｒｉｎｔｅｒ）やスキャナ（ｓｃａｎｎｅｒ）を含んでいる。そして、図１７に示すように、このＵＭＬモデル１３（検証対象）では、ユーザＡ（ＵｓｅｒＡ）がプリンタ（ｐｒｉｎｔｅｒ）、スキャナ（ｓｃａｎｎｅｒ）を順番に獲得（ｇｅｔ）した後、プリンタ（ｐｒｉｎｔｅｒ）、スキャナ（ｓｃａｎｎｅｒ）を順番に解放（ｒｅｌｅａｓｅ）することが記述されている。また、図１８に示すように、このＵＭＬモデル１３（検証対象）では、ユーザＢ（ＵｓｅｒＢ）がスキャナ（ｓｃａｎｎｅｒ）、プリンタ（ｐｒｉｎｔｅｒ）を順番に獲得（ｇｅｔ）した後、プリンタ（ｐｒｉｎｔｅｒ）、スキャナ（ｓｃａｎｎｅｒ）を順番に解放（ｒｅｌｅａｓｅ）することが記述されている。
【００５８】
図１５のステップＳ１０１において、ドメイン特化モデル（検証対象）生成部２４は、特定のシステムの仕様としてプリンタ・スキャナの獲得仕様をＵＭＬで記述したＵＭＬモデル１３（検証対象）の入力を入力装置で受け付ける。ドメイン特化モデル（検証対象）生成部２４は、ＤＢ２５により記憶された「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」に基づいて、そのＵＭＬモデル１３（検証対象）から、プリンタ・スキャナの獲得仕様をドメイン特化モデリング言語で（即ち、ＤＢ２２により記憶されたドメイン特化モデル文法に従って）記述したドメイン特化モデル（検証対象）を処理装置で生成する。そして、ドメイン特化モデル（検証対象）生成部２４は、生成したドメイン特化モデル（検証対象）をＤＢ２６に記憶する。
【００５９】
ここで、ステップＳ１０１の詳細な処理を図１９に示す。
【００６０】
図１９において、ドメイン特化モデル（検証対象）生成部２４は、入力されたＵＭＬモデル１３（検証対象）の要素を抽出して、対応するドメインの「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」を参照して、ＵＭＬモデル１３（検証対象）を１段階目のドメイン特化モデル（検証対象）に変換する（ステップＳ２０１）。図２０は、図１１に示した「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」に従って、図１６及び図１７に示したユーザＡのＵＭＬモデル１３（検証対象）から生成されるユーザＡの１段階目のドメイン特化モデル（検証対象）の一例である。同様に、図２１は、図１１に示した「ＵＭＬモデルＴｏドメイン特化モデルマッピングルール」に従って、図１６及び図１８に示したユーザＢのＵＭＬモデル１３（検証対象）から生成されるユーザＢの１段階目のドメイン特化モデル（検証対象）の一例である。図２０及び図２１に示すように、１段階目のドメイン特化モデル（検証対象）は、ＵｓｅｒＴｙｐｅやＲｅｓｏｕｒｃｅといったＳＥ記述構成要素、ｇｅｔやｒｅｌｅａｓｅといったＳＥ記述振舞い要素を含んでいる。
【００６１】
次に、ドメイン特化モデル（検証対象）生成部２４は、対応するドメインのドメイン特化モデル文法を参照して、暗黙的要素を１段階目のドメイン特化モデル（検証対象）に付加して、２段階目のドメイン特化モデル（検証対象）を生成し、ドメイン特化モデル（検証対象）のＤＢ２６に格納する（ステップＳ２０２）。図２２は、図２０に示したユーザＡの１段階目のドメイン特化モデル（検証対象）から生成されるユーザＡの２段階目のドメイン特化モデル（検証対象）の一例である。同様に、図２３は、図２１に示したユーザＢの１段階目のドメイン特化モデル（検証対象）から生成されるユーザＢの２段階目のドメイン特化モデル（検証対象）の一例である。図２２及び図２３に示すように、この２段階目のドメイン特化モデル（検証対象）は、ＳＥ記述構成要素やＳＥ記述振舞い要素だけでなく、暗黙的構成要素であるｓｔａｔｅを含んでいる。そして、この２段階目のドメイン特化モデル（検証対象）では、資源（Ｒｅｓｏｕｒｃｅ）が獲得（ｇｅｔ）されると状態（ｓｔａｔｅ）が使用中（ｕｓｅｄ）になること、及び、資源（Ｒｅｓｏｕｒｃｅ）が解放（ｒｅｌｅａｓｅ）されると状態（ｓｔａｔｅ）が空き（ｉｄｌｅ）になることが記述されている。これらの記述はＵＭＬモデル１３では省略されていたものである。
【００６２】
図２２及び図２３に示すように、このドメイン特化モデル（検証対象）は、要素として、ユーザＡ（ｕｓｅｒＡ）やユーザＢ（ｕｓｅｒＢ）、プリンタ（ｐｒｉｎｔｅｒ）やスキャナ（ｓｃａｎｎｅｒ）、使用中（ｕｓｅｄ）や空き（ｉｄｌｅ）を含んでいる。そして、図２２に示すように、このドメイン特化モデル（検証対象）では、ユーザＡ（ｕｓｅｒＡ）がプリンタ（ｐｒｉｎｔｅｒ）、スキャナ（ｓｃａｎｎｅｒ）を順番に獲得（ｇｅｔ）して各資源（Ｒｅｓｏｕｒｃｅ）の状態（ｓｔａｔｅ）を使用中（ｕｓｅｄ）に変化させた後、プリンタ（ｐｒｉｎｔｅｒ）、スキャナ（ｓｃａｎｎｅｒ）を順番に解放（ｒｅｌｅａｓｅ）して各資源（Ｒｅｓｏｕｒｃｅ）の状態（ｓｔａｔｅ）を空き（ｉｄｌｅ）に変化させることが記述されている。また、図２３に示すように、このドメイン特化モデル（検証対象）では、ユーザＢ（ｕｓｅｒＢ）がスキャナ（ｓｃａｎｎｅｒ）、プリンタ（ｐｒｉｎｔｅｒ）を順番に獲得（ｇｅｔ）して各資源（Ｒｅｓｏｕｒｃｅ）の状態（ｓｔａｔｅ）を使用中（ｕｓｅｄ）に変化させた後、プリンタ（ｐｒｉｎｔｅｒ）、スキャナ（ｓｃａｎｎｅｒ）を順番に解放（ｒｅｌｅａｓｅ）して各資源（Ｒｅｓｏｕｒｃｅ）の状態（ｓｔａｔｅ）を空き（ｉｄｌｅ）に変化させることが記述されている。
【００６３】
図１５のステップＳ１０２において、モデル検証コード生成部２７は、ＤＢ２８により記憶された「ドメイン特化モデルＴｏモデル検証コードマッピングルール」に基づいて、ドメイン特化モデル（検証対象）生成部２４により生成されたドメイン特化モデル（検証対象）から、プリンタ・スキャナの獲得仕様を記述したモデル検証コードを処理装置で生成する。
【００６４】
具体的には、モデル検証コード生成部２７は、ドメイン特化モデル（検証対象）のＤＢ２６からドメイン特化モデル（検証対象）をロードする。モデル検証コード生成部２７は、ロードしたドメイン特化モデル（検証対象）の要素を抽出して、対応するドメインの「ドメイン特化モデルＴｏモデル検証コードマッピングルール」を参照して、ドメイン特化モデル（検証対象）の個々の要素を対応するモデル検証コードに変換する。そして、モデル検証コード生成部２７は、各モデル検証コードの要素をモデル検証コードのテンプレートに埋め込み、モデル検証コードを生成し、モデル検証コードのＤＢ２９に格納する。図２４は、図１２に示した「ドメイン特化モデルＴｏモデル検証コードマッピングルール」に従って、図２２及び図２３に示したドメイン特化モデル（検証対象）から生成されるモデル検証コードの一例である。図中、白抜きで示した部分がモデル検証コード生成部２７によって埋め込まれる部分であり、その他の部分はテンプレートである。
【００６５】
図２４に示すように、このモデル検証コードは、要素として、プリンタ（Ｐｒｉｎｔｅｒ）やスキャナ（Ｓｃａｎｎｅｒ）、ユーザＡ（ＵｓｅｒＡ）やユーザＢ（ＵｓｅｒＢ）を含んでいる。そして、このモデル検証コードでは、ドメイン特化モデル（検証対象）と同様に、プリンタ（Ｐｒｉｎｔｅｒ）やスキャナ（Ｓｃａｎｎｅｒ）が獲得（Ｇｅｔ）されると状態（ｐｒｉｎｔｅｒ＿ｓｔａｔｅやｓｃａｎｎｅｒ＿ｓｔａｔｅ）が使用中（Ｕｓｅｄ）になること、及び、プリンタ（Ｐｒｉｎｔｅｒ）やスキャナ（Ｓｃａｎｎｅｒ）が解放（Ｒｅｌｅａｓｅ）されると状態（ｐｒｉｎｔｅｒ＿ｓｔａｔｅやｓｃａｎｎｅｒ＿ｓｔａｔｅ）が空き（Ｉｄｌｅ）になることが記述されている。また、このモデル検証コードでは、ユーザＡ（ＵｓｅｒＡ）がプリンタ、スキャナを順番に獲得した（ｐｒｉｎｔｅｒ＿ｃｈ！Ｇｅｔ、ｓｃａｎｎｅｒ＿ｃｈ！Ｇｅｔ）後、プリンタ、スキャナを順番に解放する（ｐｒｉｎｔｅｒ＿ｃｈ！Ｒｅｌｅａｓｅ、ｓｃａｎｎｅｒ＿ｃｈ！Ｒｅｌｅａｓｅ）ことが記述されている。また、このモデル検証コードでは、ユーザＢ（ＵｓｅｒＢ）がスキャナ、プリンタを順番に獲得した（ｓｃａｎｎｅｒ＿ｃｈ！Ｇｅｔ、ｐｒｉｎｔｅｒ＿ｃｈ！Ｇｅｔ）後、プリンタ、スキャナを順番に解放する（ｐｒｉｎｔｅｒ＿ｃｈ！Ｒｅｌｅａｓｅ、ｓｃａｎｎｅｒ＿ｃｈ！Ｒｅｌｅａｓｅ）ことが記述されている。
【００６６】
図１５のステップＳ１０３において、モデル検証実行部３０は、モデル検証コード生成部２７により生成されたモデル検証コードを用いてプリンタ・スキャナの獲得仕様を処理装置で検証し、検証結果（反例）を取得する。このとき、モデル検証実行部３０は、モデル検証コード生成部２７により生成されたモデル検証コードに記述されたプリンタ・スキャナの獲得仕様の反例を検出するモデル検証ツールとしてＳｐｉｎを処理装置で実行し、当該反例を示すデータを検証結果（反例）として取得する。
【００６７】
具体的には、モデル検証実行部３０は、モデル検証コードのＤＢ２９からモデル検証コードをロードする。そして、モデル検証実行部３０は、ロードしたモデル検証コードを入力としてモデル検証ツール（Ｓｐｉｎ）の検証コマンドを実行し、実行結果（反例）を検証結果（反例）のＤＢ３１に格納する。図２５は、図２４に示したモデル検証コードを入力して検証ツールを実行した場合に出力される検証結果（反例）の一例である。
【００６８】
図２５に示すように、ここでは反例が検出されており、この反例では、まず、プロセス番号４がプロセス番号１に対してＧｅｔメッセージを送信し（ｐｒｉｎｔｅｒ＿ｃｈ！Ｇｅｔ）、プロセス番号１がこのＧｅｔメッセージを受信している（ｃ？Ｇｅｔ）。即ち、ユーザＡ（ＵｓｅｒＡ）がプリンタ（Ｐｒｉｎｔｅｒ）を獲得（Ｇｅｔ）している。次に、プロセス番号３がプロセス番号２に対してＧｅｔメッセージを送信し（ｓｃａｎｎｅｒ＿ｃｈ！Ｇｅｔ）、プロセス番号２がこのＧｅｔメッセージを受信している（ｃ？Ｇｅｔ）。即ち、ユーザＢ（ＵｓｅｒＢ）がスキャナ（Ｓｃａｎｎｅｒ）を獲得（Ｇｅｔ）している。ユーザＡ（ＵｓｅｒＡ）もユーザＢ（ＵｓｅｒＢ）も他方の資源を獲得しなければ、獲得済みの資源を解放しないため、この時点でデッドロックが発生している。
【００６９】
図１５のステップＳ１０４において、ドメイン特化モデル（反例）生成部３２は、ＤＢ３３により記憶された「検証結果Ｔｏドメイン特化モデルマッピングルール」に基づいて、モデル検証実行部３０により取得された検証結果（反例）から、Ｓｐｉｎにより検出された反例をドメイン特化モデル文法に従って記述したドメイン特化モデル（反例）を処理装置で生成する。
【００７０】
ここで、ステップＳ１０４の詳細な処理を図２６に示す。
【００７１】
図２６において、ドメイン特化モデル（反例）生成部３２は、検証結果（反例）のＤＢ３１から検証結果（反例）をロードする。そして、ドメイン特化モデル（反例）生成部３２は、ロードした検証結果（反例）を字句解析して出力に必要な要素を抽出する（ステップＳ３０１）。ドメイン特化モデル（反例）生成部３２は、対応するドメインの「検証結果Ｔｏドメイン特化モデルマッピングルール」を参照して、検証結果（反例）を１段階目のドメイン特化モデル（反例）に変換する（ステップＳ３０２）。図２７は、図１３に示した「検証結果Ｔｏドメイン特化モデルマッピングルール」に従って、図２５に示した検証結果（反例）から生成される１段階目のドメイン特化モデル（反例）の一例である。図２７に示すように、１段階目のドメイン特化モデル（反例）は、ＵｓｅｒＴｙｐｅやＲｅｓｏｕｒｃｅといった要素のほか、ｍｅｓｓａｇｅやｓｔａｔｅといった要素を含んでいるが、ｓｔａｔｅオブジェクトのインスタンス名が不足している。
【００７２】
次に、ドメイン特化モデル（反例）生成部３２は、対応するドメイン特化モデル文法を参照して、１段階目のドメイン特化モデル（反例）で不足している要素をドメイン特化モデル文法から抽出して、１段階目のドメイン特化モデル（反例）に付加することで、２段階目のドメイン特化モデル（反例）を生成する。そして、ドメイン特化モデル（反例）生成部３２は、生成したドメイン特化モデル（反例）をＤＢ３４に格納する（ステップＳ３０３）。付加する要素は、不足している要素とドメイン特化モデル文法においてドメイン特化モデルのメタモデルの検証トレースに相当する関連、及び、不足する要素に関する情報から、ドメイン特化モデル文法の他の要素の中から該当する要素を探すことで、抽出できる。前述したように、プリンタ・スキャナ獲得仕様の例の場合、１段階目のドメイン特化モデル（反例）で不足している要素は、ｓｔａｔｅオブジェクトのインスタンス名である。ドメイン特化モデル（反例）生成部３２は、ｓｔａｔｅクラスに関し、図９に示したドメイン特化モデルのメタモデルの検証トレースに相当する関連（ｓｔａｔｅクラスとｍｅｓｓａｇｅクラス間の関連）を抽出する。そして、ドメイン特化モデル（反例）生成部３２は、図１０に示したｓｔａｔｅクラスのインスタンスとｍｅｓｓａｇｅクラスのインスタンスとの関連より、ｍｅｓｓａｇｅクラスのインスタンス名が“ｇｅｔ”の場合のｓｔａｔｅクラスのインスタンス名が“ｕｓｅｄ”であることから、１段階目のドメイン特化モデル（反例）にて不足している要素（ｓｔａｔｅオブジェクトのインスタンス名）は“ｕｓｅｄ”であると判断する。
【００７３】
図１５のステップＳ１０５において、ＵＭＬモデル（反例）生成部３５は、ＤＢ３６により記憶された「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」に基づいて、ドメイン特化モデル（反例）生成部３２により生成されたドメイン特化モデル（反例）から、Ｓｐｉｎにより検出された反例をＵＭＬで記述したＵＭＬモデル１４（反例）を処理装置で生成する。
【００７４】
具体的には、ＵＭＬモデル（反例）生成部３５は、ドメイン特化モデル（反例）のＤＢ３４からドメイン特化モデル（反例）をロードする。そして、ＵＭＬモデル（反例）生成部３５は、ロードしたドメイン特化モデル（反例）の要素を抽出して、対応する「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」を参照して、ドメイン特化モデル（反例）をＵＭＬモデル１４（反例）に変換し、出力する。図２９は、図１４に示した「ドメイン特化モデルＴｏＵＭＬモデルマッピングルール」に従って、図２８に示したドメイン特化モデル（反例）から生成されるＵＭＬモデル１４（反例）の一例である。
【００７５】
図２９に示すように、このＵＭＬモデル１４（反例）では、ユーザＡ（ｕｓｅｒＡ）によってプリンタ（ｐｒｉｎｔｅｒ）が獲得（ｇｅｔ）されてプリンタ（ｐｒｉｎｔｅｒ）の状態が空き（ｉｄｌｅ）から使用中（ｕｓｅｄ）に変化し、続けてユーザＢ（ｕｓｅｒＢ）によってスキャナ（ｓｃａｎｎｅｒ）が獲得（ｇｅｔ）されてスキャナ（ｓｃａｎｎｅｒ）の状態が空き（ｉｄｌｅ）から使用中（ｕｓｅｄ）に変化すると、デッドロックが発生するということが記述されている。
【００７６】
以上のように、本実施の形態によれば、以下に示す効果を得ることができる。
・ドメイン内で共通した記述（ドメイン特化モデル文法における暗黙的要素）をサブセットとしてドメインエンジニア１２が事前に定義しておき、共通した記述（ドメイン特化モデル文法における暗黙的要素）はドメイン特化モデル（検証対象）生成部２４が行うようにすることにより、ＳＥ１１が定義する検証対象のモデルは、ドメイン特化モデルのメタモデル（ドメイン特化モデル文法）のＳＥ記述構成要素とＳＥ記述振舞い要素のみの部分となるため、記述量を汎用的なＵＭＬよりも減らすことができる。
・ドメイン特化モデル文法は、一般的なモデリング言語として知られているＵＭＬを拡張したものであるため、ＵＭＬの知識があるＳＥ１１にとっては、検証対象のモデル定義のためだけに新たな記述文法を学ぶ必要がない。
・ドメイン特化モデル（反例）生成部３２が「検証結果Ｔｏドメイン特化モデルマッピングルール」の参照によるモデル変換と、モデル変換により生成したドメイン特化モデル（反例）に不足する要素の付加を行うことにより、入力モデルと出力モデルの要素が対応するため、出力モデルの意味解析が従来よりも容易になる。
【符号の説明】
【００７７】
１０  設計モデル検証方式、１１  ＳＥ、１２  ドメインエンジニア、１３，１４  ＵＭＬモデル、２０  検証装置、２１，２２，２３，２５，２６，２８，２９，３１，３３，３４，３６  ＤＢ、２４  ドメイン特化モデル（検証対象）生成部、２７  モデル検証コード生成部、３０  モデル検証実行部、３２  ドメイン特化モデル（反例）生成部、３５  ＵＭＬモデル（反例）生成部、９０１  ＬＣＤ、９０２  キーボード、９０３  マウス、９０４  ＦＤＤ、９０５  ＣＤＤ、９０６  プリンタ、９１１  ＣＰＵ、９１２  バス、９１３  ＲＯＭ、９１４  ＲＡＭ、９１５  通信ボード、９２０  ＨＤＤ、９２１  オペレーティングシステム、９２２  ウィンドウシステム、９２３  プログラム群、９２４  ファイル群。
【図１】
2011180632.tif 000003
【図２】
2011180632.tif 000004
【図３】
2011180632.tif 000005
【図４】
2011180632.tif 000006
【図５】
2011180632.tif 000007
【図６】
2011180632.tif 000008
【図７】
2011180632.tif 000009
【図８】
2011180632.tif 000010
【図９】
2011180632.tif 000011
【図１０】
2011180632.tif 000012
【図１１】
2011180632.tif 000013
【図１２】
2011180632.tif 000014
【図１３】
2011180632.tif 000015
【図１４】
2011180632.tif 000016
【図１５】
2011180632.tif 000017
【図１６】
2011180632.tif 000018
【図１７】
2011180632.tif 000019
【図１８】
2011180632.tif 000020
【図１９】
2011180632.tif 000021
【図２０】
2011180632.tif 000022
【図２１】
2011180632.tif 000023
【図２２】
2011180632.tif 000024
【図２３】
2011180632.tif 000025
【図２４】
2011180632.tif 000026
【図２５】
2011180632.tif 000027
【図２６】
2011180632.tif 000028
【図２７】
2011180632.tif 000029
【図２８】
2011180632.tif 000030
【図２９】
2011180632.tif 000031