(57)【要約】【課題】自然言語で記述された仕様書の不備を検出する。【解決手段】本発明の一態様としての仕様検証装置は、構文解析部、仕様解析部、検出部、提示部とを備える。前記構文解析部は、自然言語で記述された要求仕様を形態素解析により単語と品詞とに分解し、係受け解析により少なくとも1つの前記単語を含む文節と、文節間の係り受け関係を表した構文データを得る。前記仕様解析部は、仕様解析ルールに従って、前記構文データを解析することにより、動詞の単語を含む文節毎に、前記動詞と、前記動詞に対する主語と、前記動詞に対する目的語と、前記動詞と前記目的とにより定まる動作が行われる前に成立している必要がある事前条件とに関する項目を含む意味表現データを生成する。前記検出部は、前記意味表現データを検査することにより、前記意味表現データにおいて前記不備のある項目を検出する。【選択図】図１
2014081680.tif 000002
【特許請求の範囲】
【請求項１】
自然言語で記述された要求仕様を形態素解析により単語と品詞とに分解し、係受け解析により少なくとも1つの前記単語を含む文節と、文節間の係り受け関係を表した構文データを得る構文解析部と、
係り受け元の文節の品詞と、係受け先の文節の品詞とから、前記係り受け元の文節と、前記係り受け先の文節との関係を定めた複数の仕様解析ルールに従って、前記構文データを解析することにより、動詞の単語を含む文節毎に、前記動詞と、前記動詞に対する主語と、前記動詞に対する目的語と、前記動詞と前記目的とにより定まる動作が行われる前に成立している必要がある事前条件とに関する項目を含む意味表現データを生成する仕様解析部と、
前記動詞、前記主語、前記目的語および前記事前条件の少なくとも1つの値またはこれらのうち2つ以上の関係から前記項目のうち不備のある項目を特定するための検査ルールを用いて、前記意味表現データを検査することにより、前記意味表現データにおいて前記不備のある項目を検出する検出部と、
前記検出部により検出した項目を提示する第1提示部と、
を備えた仕様検証装置。
【請求項２】
用語を定義した第1辞書データと、
動詞と目的語との組を定義した第2辞書データと、を備え、
前記検出部は、前記意味表現データにおいて、
前記第1辞書データで定義されていない用語、
または前記第2辞書データで定義されていない前記動詞と目的語の組、
または主語がない動詞、
または事前条件がない動詞を
前記不備のある項目として検出する、
請求項1に記載の仕様検証装置。
【請求項３】
前記意味表現データをユーザに提示する第2提示部と
ユーザからの入力に基づき前記意味表現データを修正する修正入力受付部
をさらに備えた請求項1ないし2のいずれか一項に記載の仕様検証装置。
【請求項４】
前記意味表現データは、前記動詞および前記目的語により定まる動作が行われた後に成立している必要がある事後条件の項目を含み、
前記第2辞書データは、前記動詞と前記目的後の組とともに、前記動詞および前記目的語により定まる動作が行われる前の状態である事前状態と、前記動作が行われた後の状態である事後状態とを含み、
前記意味表現データにおける前記事後条件の項目に、前記辞書データに基づき、前記事後状態を追加する
請求項2に記載の仕様検証装置。
【請求項５】
各用語に対応するクラスの継承関係および所有関係を含む第1辞書データと
動詞と、目的語と、前記動詞および前記目的語により定まる動作が行われる前の状態である事前状態と、前記動作が行われた後の状態である事後状態とを含む第2辞書データと、
前記クラスの継承関係および所有関係と、前記第2辞書データにおける前記動作、前記事前状態および前記事後状態間の関係を示す動作関係とに基づき、仕様記述言語による仕様を生成し、前記意味表現データの内容に応じた記述を前記仕様に追加することで、拡張された仕様を生成し、拡張した仕様を充足する事例を少なくとも1つ求める、仕様解釈部と、
をさらに備えた請求項1ないし4のいずれか一項に記載の仕様検証装置。
【請求項６】
前記仕様解釈部により生成された事例をユーザに提示する第3提示部
をさらに備えた請求項5に記載の仕様検証装置。
【請求項７】
ユーザからの入力により前記要求仕様または前記拡張された仕様を修正する修正入力受付部
をさらに備えた請求項6に記載の仕様検証装置。
【請求項８】
自然言語で記述された要求仕様を形態素解析により単語と品詞とに分解し、係受け解析により少なくとも1つの前記単語を含む文節と、文節間の係り受け関係を表した構文データを得る構文解析ステップと、
係り受け元の文節の品詞と、係受け先の文節の品詞とから、前記係り受け元の文節と、前記係り受け先の文節との関係を定めた複数の仕様解析ルールに従って、前記構文データを解析することにより、動詞の単語を含む文節毎に、前記動詞と、前記動詞に対する主語と、前記動詞に対する目的語と、前記動詞と前記目的とにより定まる動作が行われる前に成立している必要がある事前条件とに関する項目を含む意味表現データを生成する仕様解析ステップと、
前記動詞、前記主語、前記目的語および前記事前条件の少なくとも1つの値またはこれらのうち2つ以上の関係から前記項目のうち不備のある項目を特定するための検査ルールを用いて、前記意味表現データを検査することにより、前記意味表現データにおいて前記不備のある項目を検出する検出ステップと、
前記検出ステップにより検出した項目を提示する第1提示ステップと、
をコンピュータが実行する仕様検証方法。
【請求項９】
自然言語で記述された要求仕様を形態素解析により単語と品詞とに分解し、係受け解析により少なくとも1つの前記単語を含む文節と、文節間の係り受け関係を表した構文データを得る構文解析ステップと、
係り受け元の文節の品詞と、係受け先の文節の品詞とから、前記係り受け元の文節と、前記係り受け先の文節との関係を定めた複数の仕様解析ルールに従って、前記構文データを解析することにより、動詞の単語を含む文節毎に、前記動詞と、前記動詞に対する主語と、前記動詞に対する目的語と、前記動詞と前記目的とにより定まる動作が行われる前に成立している必要がある事前条件とに関する項目を含む意味表現データを生成する仕様解析ステップと、
前記動詞、前記主語、前記目的語および前記事前条件の少なくとも1つの値またはこれらのうち2つ以上の関係から前記項目のうち不備のある項目を特定するための検査ルールを用いて、前記意味表現データを検査することにより、前記意味表現データにおいて前記不備のある項目を検出する検出ステップと、
前記検出ステップにより検出した項目を提示する第1提示ステップと、
をコンピュータに実行させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明の実施形態は、仕様検証装置およびその方法、プログラムに関する。
【背景技術】
【０００２】
従来、自然言語で書かれた仕様書からプログラムを生成する技術が知られている。ルールに合わせて仕様解析を行い、解析結果のパターンをみて遷移図を出力する。
【０００３】
また、別の従来技術として、ソフトウェア仕様を形態素解析、意味解析を通して意味構文に変換し、意味構文の意図する内容を推論し、当該内容を必要なモジュールに展開するものが知られている。これは、ソフトウエアのモジュール構成に着目して、仕様書からモジュール構成を自動的に導こうというものである。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開平第5-46370号公報
【特許文献２】特開平第7-28630号公報
【特許文献３】特開平第6-214776号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
従来の技術は自然言語で記述された仕様書を解析し、プログラムを作成していた。このとき、もともとの仕様書に日本語としての欠陥や、仕様書の内容としての欠陥がある場合までは考慮されていなかった。さらに仕様書に含まれる、クラス階層に関する情報と、インスタンスに係る制約とを区別しておらず、それぞれに対する適切な、検証や変換方法を採用していなかった。
【０００６】
本発明の一側面は、不備のない設計仕様の作成を容易に行うことが可能な仕様検証装置およびその方法、プログラムを提供することを目的とする。
【課題を解決するための手段】
【０００７】
本発明の一態様としての仕様検証装置は、構文解析部、仕様解析部、検出部、第１提示部とを備える。
【０００８】
前記構文解析部は、自然言語で記述された要求仕様を形態素解析により単語と品詞とに分解し、係受け解析により少なくとも1つの前記単語を含む文節と、文節間の係り受け関係を表した構文データを得る。
【０００９】
前記仕様解析部は、係り受け元の文節の品詞と、係受け先の文節の品詞とから、前記係り受け元の文節と、前記係り受け先の文節との関係を定めた複数の仕様解析ルールに従って、前記構文データを解析することにより、動詞の単語を含む文節毎に、前記動詞と、前記動詞に対する主語と、前記動詞に対する目的語と、前記動詞と前記目的とにより定まる動作が行われる前に成立している必要がある事前条件とに関する項目を含む意味表現データを生成する。
【００１０】
前記検出部は、前記動詞、前記主語、前記目的語および前記事前条件の少なくとも1つの値またはこれらのうち2つ以上の関係から前記項目のうち不備のある項目を特定するための検査ルールを用いて、前記意味表現データを検査することにより、前記意味表現データにおいて前記不備のある項目を検出する。
【００１１】
前記第1提示部は、前記検出部により検出した項目を提示する。
【図面の簡単な説明】
【００１２】
【図１】本発明の実施例に係る仕様検証装置のブロック図を示す。
【図２】仕様の意味表現グラフを構造を示す。
【図３】図1の装置の全体の動作フローを示す。
【図４】仕様解析部の動作フローを示す。
【図５】矛盾・欠損検知部の動作フローを示す。
【図６】用語表（辞書データ）の一例を示す。
【図７】構文解析の結果である構文木を模式的に表す。
【図８】要求仕様の解析結果をXML形式で表す。
【図９】仕様解析ルールを表形式で表す。
【図１０】仕様解析により得られる、仕様の意味表現グラフを示す。
【図１１】仕様検証ルールの一例を示す。
【図１２】修正後の意味表現グラフを示す。
【図１３】最終的に得られた意味表現グラフを示す。
【図１４】仕様解釈部の動作フローを示す。
【図１５】修正前の仕様記述の例を示す。
【図１６】図15の仕様記述に対して、仕様解釈部により解釈例を生成し、当該解釈例をグラフ表示により示す。
【図１７】修正後の仕様記述から得られる解釈例をグラフ表示により示す。
【図１８】さらなる修正後の仕様記述から得られる解釈例をグラフ表示により示す。
【図１９】最終的に得られた仕様記述の例を示す。
【発明を実施するための形態】
【００１３】
以下、図面を参照しながら、本実施例を説明する。
【００１４】
図1に本発明の実施例に係る仕様検証装置のブロック図を示す。
【００１５】
以下ではまず、図1の仕様検証装置の構成および動作の概要について説明し、その後、具体例を説明する。
【００１６】
構文解析部11は、自然言語で記述された要求仕様に対して、構文解析を行って、構文木等の構文データを生成する。構文解析は、形態素解析および係り受け解析を含む。形態素解析では、要求仕様を単語と品詞とに分解する。係受け解析では少なくとも1つの当該単語を含む文節と、文節間の係り受け関係を解析し、構文木を得る。係り受け関係は、構文木ではノード間のリンク情報として表される。
【００１７】
仕様解析部12は、用語表（辞書データ）に基づき、仕様解析ルールに従って構文木を解析することにより、仕様の意味表現データ（仕様の意味表現グラフ）を生成する。
【００１８】
仕様解析ルールは、係り受け元の文節の品詞と、係受け先の文節の品詞とから、当該係り受け元の文節と、当該係り受け先の文節との関係を定めたものである（後述する図9参照）。
【００１９】
辞書データとしての用語表（後述する図6）は、使用可能な用語と、使用可能な動詞と目的語との組とを定義する。より詳細には、用語表は、（1）用語間の継承関係(is-a関係)および所有関係（has-a関係）と、（2）動詞と目的語と事前状態と事後状態との関係とを表す。動詞と目的語の組によって、1つの動作ないしは操作が表される。なお、用語は、少なくとも1つの単語を含み、複数の単語による連体化された名詞等も含んでよい。
【００２０】
仕様の意味表現グラフは、動詞の単語を含む文節毎に、前記動詞と、前記動詞に対する主語と、前記動詞に対する目的語と、前記動詞および前記目的語により定まる動作が起こる前に成立している必要がある条件（事前条件）と、当該動作が起こった後に成立している必要がある条件（事後条件）に関する項目を含む。
【００２１】
図2に、仕様の意味表現グラフを構造を示す。ここではテーブル形式の構造が示される。仕様の意味表現グラフは、動詞の単語を含む文節毎に、主語、目的語、事前条件、事後条件の項目を含むレコードが存在する。事前条件として、たとえば列id=xが列id=yの前提条件になる場合は、id=yの事前条件としてid=xを記録する。事後条件の項目が存在しない場合も可能である。
【００２２】
仕様記録部13は、仕様解析部12により生成された、仕様の意味表現グラフを内部に記録する。
【００２３】
意味表現提示部14は、仕様解析部12で生成された仕様の意味表現グラフを、設計者等のユーザに提示する。また、後述するようにユーザ入力に基づき修正入力受付部17により修正された意味表現グラフを設計者に提示する。
【００２４】
矛盾・欠損検出部（検出部）15は、仕様の意味表現グラフに対して、仕様検証ルールに従って検証を行い、矛盾・欠陥等の不備があれば、矛盾・欠陥の内容を表す指摘事項を生成する。
【００２５】
仕様検証ルールとしては、例えば、動詞、主語、目的語および事前条件の少なくとも1つの値またはこれらのうち２つ以上の項目の関係に基づいて、仕様の意味表現グラフの各項目のうち不備のある項目を特定するためのルールを用意する。このルールに従って、意味表現グラフを検査することにより、仕様の意味表現グラフの各行ごと（動詞ごと）に、不備のある項目を検出する。たとえば必須項目であるにもかかわらず、値が抜けている項目、用語表データで定義されていない用語を含む項目、また、用語表データで定義されていない動詞と目的語の組の項目を検出する。これらのルールに従って、意味表現グラフの各行ごとに検査し、定義されていない用語や、定義されていない動詞と目的語の組（動作）等を検出する。
【００２６】
指摘事項提示部16は、矛盾・欠陥検出部15により検出した項目と、当該項目が検出された事由とを、設計者等のユーザへの指摘事項として提示する。たとえば定義されていない用語を用いていれば、当該用語と、定義されていない用語を用いている旨のメッセージとを提示する。
【００２７】
修正入力受付部17は、設計者から仕様の意味表現グラフに対する修正を受け入れ、入力されたデータにより、仕様の意味表現グラフを更新する。
【００２８】
仕様解釈部18は、用語表と、仕様の意味表現グラフを解釈して、alloy等の任意の仕様記述言語で記述された形式仕様記述を生成し、当該記述を解釈して、具体的な事例を解釈例として生成する。より詳細に、用語表から形式仕様記述を生成し、当該形式仕様記述を仕様の意味表現グラフの内容を追加することで拡張する。拡張された形式仕様記述を解釈し、この記述を充足する事例（インスタンス）を少なくとも1つ求める。形式仕様記述は、仕様解釈部18が、公知の方法で自動生成してもよいし、設計者が用語表と仕様の意味表現グラフに基づき生成してもよい。
【００２９】
解釈例提示部19は、仕様解釈部18で生成された解釈例を設計者に提示する。解釈例は複数生成してもよい。設計者は、解釈例に不備があるかどうかを検討し、不備があれば、要求仕様または意味表現グラフまたはこれらの両方を修正し、形式仕様記述を再生成する。形式仕様記述を設計者が直接修正してもよい。そして、再度、解釈例を生成し、解釈例に不備があるかを検討する。
【００３０】
上記したような構成の仕様検証装置によれば、自然言語で記述された要求仕様を解析して、仕様の意味表現グラフとして設計者に提示すると共に、漏れや矛盾等の不備を、設計者に理解可能な形式で提示することができる。さらに設計者の仕様記述の修正を反映し、要求仕様にフィードバックできる。また要求仕様からこれを充足する具体的な事例を解釈例として生成できるので、設計者が解釈例を見て、要求仕様に不足する制約を明らかにできる。
【００３１】
以下、図3を用いて、図1の装置の全体の動作フローについて説明する。
【００３２】
まず、要求仕様と用語表（第１辞書データおよび第２辞書データ）を読み込み、仕様解析部12が仕様解析ルールに基づき仕様解析を実施し、仕様の意味表現グラフを作成する（S101）。意味表現グラフと仕様検証ルールに基づき、矛盾・欠損検出部15が、矛盾や欠損等の不備の検知を行う（S102）。矛盾・欠損があれば（S103のY）、矛盾・欠損の検知結果を、指摘事項として設計者に提示する（S104）。設計者の意味表現グラフまたは仕様修正の働きかけに対して、修正を受け入れて（S105、S106、S107）、再び矛盾・欠損検知処理を繰り返す。矛盾・欠損が検知されなくなると（S103のN）、仕様解釈部18が用語表と、意味表現グラフに基づき、仕様の解釈を行って形式仕様記述を生成し、形式仕様記述を充足する具体的な解釈例を生成し（S108）、当該解釈例を設計者に提示する（S109）。解釈例に問題があり、設計者が仕様を修正した場合には（S107）、再び矛盾・欠損の検知から再処理を行う。このとき、設計者の修正に伴って意味表現グラフに対し整合性をとる修正を行う。なお、解釈例に問題がある場合に、形式仕様記述を直接修正してもよい。
【００３３】
以下、図4を用いて、仕様解析部12の動作フローについて説明する。
【００３４】
構文解析部11により生成された構文木を読み込んで（S201）、構文木上の依存関係（リンク関係）をリンク情報として読み出す（S202）。未処理のリンク情報がある場合は（S203のY）、未処理リンクを選択し、仕様解析ルールを順次適用し（S204）、マッチするルールがあるか調べる（S205）。マッチするルールが発見されれば（S205のY）、テーブルにレコードを追加する（S206）。未処理のリンク情報がなくなるまで、以上の処理を繰り返す。リンク情報をすべて処理したら（S203のN）、必要に応じて用語表に従い、テーブルを修正する（S207）。このようにして得られたテーブルを、仕様の意味表現グラフとして出力する。
【００３５】
以下、図5を用いて、矛盾・欠損検知部15の動作フローについて説明する
仕様の意味表現グラフ（テーブル）を読み込み（S301）、レコードを順に処理する。未処理のレコードがあれば（S302のY）、仕様検証ルールを順次適用し（S303）、レコードにマッチするルールがあるかを調べる（S304）。マッチするルールが存在すれば（S304のY）、矛盾・欠損の指摘事項を、一時記憶領域またはリストに追加する（S305）。次のレコードを選択し（S306）、未処理のレコードがなくなるまで以上の操作を繰り返す。レコードをすべて処理したならば（S302のN）、ステップS305で追加した指摘事項をまとめて、設計者に提示する（S307）。
【００３６】
以下、具体的な事例を用いて、本装置の動作を説明する。
【００３７】
要求仕様として、以下の自然言語で記述された文章が与えられたとする。
【００３８】
要求仕様：
「アイドルの状態で、蓋を閉じたら、水位を確認し、条件に合えば沸騰行為をする」
【００３９】
図6は、用語表（辞書データ）の一例を示す。
【００４０】
用語表には、用語間の関係を定義するテーブル（第1辞書データ）と、動作の意味を定義するテーブル（第2辞書データ）が含まれる。用語間の関係を定義するテーブルは、用語に対応するクラスの階層関係を示すis関係、全体/部品関係を示すhas関係を定める。
【００４１】
動作の意味を定義するテーブルは、動詞、目的語、事前状態、事後状態を定義する。動詞と目的語により動作あるいは操作を表す。
【００４２】
構文解析部11は、要求仕様の文章に対し、自然言語処理である形態素解析と係り受け解析とを行う。形態素解析とは文章を単語に分解し、単語の属性（名詞、動詞、助詞など）を明らかにするものである。また係り受け解析とは、単語の間の依存関係を明らかにするものである。より具体的に、少なくとも1つの単語を含む文節と、文節間の係り受け関係を明らかにする。
【００４３】
図7は、構文解析の結果である構文木を模式的に表したものである。構文解析部11は形態素解析と係り受け解析を行うことができれば、自然言語処理で用いられる既存の技術を用いればよい。図8は、cabocha（カボチャ）と呼ばれるライブラリにより、要求仕様の解析結果をXML形式で表したものである。依存関係はリンク情報(link)としてXML形式で記述されている。
【００４４】
仕様解析部12は、構文木を読み込み、リンク情報の集合を得る。図8の構文木例では、チャンク(chank)と呼ばれるグループの配下に、単語単位であるtok要素が保存される。チャンクにはリンク(link)属性が設けられる。リンク属性には、リンク先のidが記録される。
【００４５】
以下、説明のため、チャンクおよびリンク情報を次のように表す。
【００４６】
チャンク：{id:チャンクのid,内容:チャンクに含まれる日本語}、
リンク情報：{org:リンク元id、dst:リンク先id}
【００４７】
したがって、本実施例においてはチャンクは、以下のようになる。
【００４８】
{id:0,内容:アイドルの},{id:1,内容:状態で},{id:2,内容:蓋を},{id:3, 内容:閉じたら},{id:4,内容:水位を},{id:5, 内容:確認し},{id:6, 内容:条件に},{id:7, 内容:合えば},{id:8, 内容:沸騰行為を},{id:9, 内容:する}
【００４９】
またリンクは、以下のようになる。なお、”dst:-1”は、チャンク9には、これ以上リンク先がないことを意味する。
【００５０】
{org:0,dst:1},{org:1,dst:3},{org:2,dst:3},{org:3,dst:5},{org:4,dst:5},{org:5,dst:9},{org:6,dst:7},{org:7,dst:9},{org:8,dst:9},{org:9,dst:-1}
【００５１】
図9は、仕様解析ルールを表形式で表したものである。
【００５２】
以下に、図9の仕様解析ルールに従って、仕様解析処理を行う様子を、ログテキストで表す。
【００５３】
ルール2適用：「アイドルの状態で(id0,id1)」は「閉じたら(id3)」の条件になります
ルール3適用：「蓋を(id2)」は「閉じたら(id3)」の目的語になります
ルール2適用：「閉じたら(id3)」は「確認し(id5)」の条件になります
ルール3適用：「水位を(id4)」は「確認し(id5)」の目的語になります
ルール1適用：「確認し(id5)」は「する(id9)」の条件になります
ルール4適用：「合えば(id7)」は「する(id9)」の条件になります
ルール3適用：「沸騰行為を(id8)」は「する(id9)」の目的語になります
ルール5適用：「条件に(id6)」は「合えば(id7)」の目的語になります
【００５４】
図10は、以上の動作を通じて仕様解析後に得られる、仕様の意味表現グラフを示す表である。
【００５５】
「ID」は動詞に振られた番号である。この表は、ID、動詞、主語、目的語、事前条件、事後条件の項目からなるレコードを含む。該当する値がなければ、その項目はブランクになる。この表の例では、以下のことが理解される。
【００５６】
主語（主体）は、すべての動詞に対して、存在しない。
【００５７】
目的語（対象）は、｛蓋、水位、沸騰行為、条件に｝である。
【００５８】
動詞は、｛閉じる、確認する、する、合う｝である。
【００５９】
事前条件は、｛閉じる、アイドル状態、確認する、合う｝になる。
【００６０】
また動詞に対する目的語関係は、｛蓋、閉じる｝、｛水位、確認する｝、｛沸騰行為、する｝、｛条件、合う｝の間に成立している。
【００６１】
動詞の間に成立する条件関係は、ID番号を用いて表現している。たとえばnd2の事前条件はnd1になる。2つ以上の条件関係があるとき“＆”記号により連結している。
【００６２】
次に、前述した図5に示した矛盾・欠損検出部の手順に従って仕様検証処理を行う例を示すする。
【００６３】
図11は仕様検証ルールの一例を示す。
【００６４】
最初に、ルール1：「主語のない動詞$1がある」を仕様の意味表現グラフに適用すると、
“動詞、「閉じる」、「確認する」、「する」、「合う」に主語がありません。”
ことを指摘事項として得る。
【００６５】
次に、ルール2：「用語辞書に無い動詞がある」を仕様の意味表現グラフに適用すると、
「する」および「合う」は動作として定義されていないので（図6の用語表を参照）、
“「する」は、動作として、未定義です。”
“「合う」は、動作として、未定義です。”
ことを指摘事項としてさらに得る。
【００６６】
指摘事項提示部16により、設計者にこれらの指摘事項が提示される。設計者は、提示された指摘事項に基づき、仕様の意味表現グラフを修正する。図12は、修正後の意味表現グラフを示す。
【００６７】
設計者は例えば、上記指摘事項に対して、「閉じる」、「押す」の主語として「使用者」を追加し、「確認する」の主語として「システム」を追加する。
【００６８】
また、設計者は、上述の「（沸騰行為を）する」が、用語表における「沸騰ボタンを押す」に相当すると判断し、「（沸騰行為を）する」を「沸騰ボタンを押す」に置き換える。
【００６９】
また、用語表から、動作に対応する事後状態を、事後条件の項目に追加する。ここでは、nd1の「蓋を閉じる」動作に対して「閉じた蓋」、nd3の「沸騰ボタンを押す」に対して「沸騰行為」を追加している。nd2の「水位を確認する」に対して「適正水位ＯＲ適正でない水位」を追加してもよい。なお、事後状態の追加は、本装置が自律的に判断して行っても、設計者が入力しても良い。
【００７０】
また、「条件に合う」は用語表に対応する項目が無い。設計者がこれを「適正水位」に対応させるとの指示を入力すると、依存関係からnd3の事前条件である「nd2&nd4」を特定し、この「nd4」を「適正水位」に置き換える。なお、nd4のレコードは削除してよい
最後に、これ以上マッチするルールがないので、矛盾・欠損検出を終了する。
【００７１】
図13に、以上の処理により最終的に得られた意味表現グラフを示す。
【００７２】
図13の意味表現グラフを、元の自然言語の表現に戻すと以下のようになる。
【００７３】
「ポットがアイドルの状態で、ポットの使用者が蓋を閉じたら、システムは、水位を確認し、適正水位であるならば、沸騰ボタンを押すと、沸騰行為になる。」
【００７４】
図14に仕様解釈部18の動作フローを示す。
【００７５】
仕様解釈部18は、用語表と、仕様の意味表現グラフを入力とする。仕様解釈部18は、用語表のis関係からクラス継承関係・所有関係を抽出し、用語表の動詞と目的語と事前状態と事後状態から動作関係（操作関係）を抽出し、抽出したこれらの関係を、仕様記述言語で記述された形式仕様記述に変換する（S401、S402）。動作関係は、たとえば動作前の状態、動作、動作後の状態を含む。さらに仕様の意味表現グラフから、仕様に現れるクラス、動作、および、その条件（事前条件・事後条件）、条件間の関係を抽出し、上記形式仕様記述を拡張する（S403）。具体的に、仕様の意味表現グラフの中で、形式仕様記述に含まれていない事項により、形式仕様記述を拡張する。こうして得られた形式仕様記述に対して「解釈処理」を実施し、当該記述を満たす具体的な事例を、解釈例として生成する。必要に応じて、仕様または仕様記述等を修正し（S405）、再度、解釈処理を実行する。
【００７６】
仕様記述言語、および解釈実行では、本実施例ではAlloy言語を用いる。なお仕様記述言語および解釈実行は、Alloy言語に限定せず、同等の機能を持つ他のもので代替可能である。
【００７７】
本実施例で用いる、Alloy言語における仕様記述の形式を以下に示す
【００７８】
sig クラス名 extends 上位のクラス{
部品名：部品のクラス,
..
状態遷移操作名：lone 遷移先クラス,
..
}
{
{some 操作 =>{
事前条件や事後条件
}
…
}
【００７９】
“sig”は、sig以下の記述がクラスの定義であることを示している。
【００８０】
また“extends”はクラス階層関係(is)に従って、上位のクラスを示す。
【００８１】
クラス定義の内部は、has関係で表現される部品の定義と、状態遷移に係る操作（状態遷移操作）の定義とで構成される。
【００８２】
状態遷移に係る操作に事前条件、事後条件を記述する場合は、クラス定義の直後に、操作に関する詳細を記述する(“some=>”以降に記述する)。
【００８３】
最初に、ポットに係る用語表から、has,is関係より以下のクラス定義に相当する記述を得る。下記の表は、図6の用語表から、説明に必要な部分を取り出して示したものである。
【表１】
2014081680.tif 000003
【００８４】
ここで”sig”はクラス定義であり、”abstract”は抽象クラスであることを指定している。抽象クラスとは、それ単独ではインスタンス（実体）にならない上位クラスである。ポットの例では、「ポット」、「利用できる状態」、「温度制御状態」の3つのクラスが抽象クラスに対応する。
【００８５】
“is”関係はクラス継承(extends)関係に対応する。”has”関係によりポットの部品として水位、蓋、ロックがある。それぞれデフォルトの属性名、“ポットのXXX”（XXXは部品名）を持っている。
【００８６】
抽象クラス「利用できる状態」は、より具体的な下位のクラスとして、「温度制御状態」、「アイドル」を持っている。
【００８７】
「温度制御状態」は、さらに下位のクラスとして、「沸騰状態」、「保温状態」、「沸騰行為」を持っている。
【００８８】
次に、用語表の動作に係るテーブルから、動作（操作）に係る記述を変換する。下記の表は、説明に必要な部分を取り出して示したものである。
【表２】
2014081680.tif 000004
【００８９】
「蓋を閉じる」、「蓋を開ける」操作は、蓋の状態を変更する。蓋はポットの部品であるので、ポットに対する操作として変換する。すなわち、ポットのクラス特有の操作記述として追加する。
【００９０】
一方、「コンセントを押す」、「コンセントを抜く」操作は、ポットの下位クラスである「利用できる状態」、「利用できない状態」間の状態を変更する。そこで「利用できない状態」、「利用できる状態」に対して、状態遷移操作として「コンセントを抜く」、「コンセントを押す」操作を追加する。
【００９１】
ここで「蓋を閉じる」、「蓋を開ける」操作には事前条件と事後条件が記述されている。
【００９２】
事前条件は、
“部品名  (not)in 部品の事前の状態”
事後条件は、
“操作名  (not) in 事後の状態”
あるいは
操作名.@部品名 (not)in 部品の事後状態
という形式でAlloyでは記述される。「操作名.@」は、遷移後のポットの状態に対応している。
【００９３】
次に、仕様の意味表現グラフに基づく下記の情報を、仕様記述に追加する。
【表３】
2014081680.tif 000005
【００９４】
操作である「沸騰ボタンを押す」は、事前条件をnd2→nd1とたどるとアイドルであり、アイドルはポットの下位クラスであるので、アイドル状態特有の操作として定義する。
【００９５】
操作の結果、ポットが「沸騰行為」状態になるので、操作の結果を(lone 沸騰行為)としている。
【表４】
2014081680.tif 000006
【００９６】
このように、用語辞書に基づき形式的な仕様記述言語で書かれた仕様を生成し、仕様の意味表現グラフに基づく、事前条件および事後条件を当該仕様に追加することにより、図15に示すような仕様記述を得る。
【００９７】
図16は、図15の仕様記述に対して、仕様解釈部18により仕様を満たす具体例（解釈例）を生成し、当該解釈例をグラフ表示したものである。ここで解釈例とは、仕様記述で定義したクラス情報に準拠した具体例のことである。図16の具体例では、「沸騰状態」の水位は「適正水位」で、「沸騰状態」の蓋は「開いた蓋」である。解釈例の生成および可視化は、実施例ではAlloyツールを用いたが、同様の機能を持つ別の言語およびツールを用いても良い
図16をみると、「沸騰行為」から「沸騰する」操作で「沸騰状態」への遷移が確認できる。遷移先の「沸騰状態」の蓋は開いている。したがって、「沸騰する」操作の事後条件として、「閉じた蓋」という条件が不足していることがわかる。そこで「沸騰する」操作の事後条件に
“沸騰する.@ポットの蓋  in  閉じた蓋”
を追加する。同様に「沸騰ボタンを押す」に対しては、同様の事後条件を、追加する。再び、仕様解釈部18により解釈例を生成することで、図17に示すグラフを得る。なお、事後条件に該当する記載を、要求仕様に追加し、本装置の動作フローを最初から行ってもよい。あるいは、意味表現グラフに当該事後条件を追加して、仕様解釈部18を動作させてもよい。
【００９８】
図17を見ると「沸騰行為1」から「蓋を開ける」操作で「沸騰行為0」への遷移が確認できる。蓋が開いたまま沸騰行為を行うのは望ましくない。したがって、「蓋を開ける」操作の事後条件に「温度制御状態」以外に遷移するという制限が欠けていることがわかる。
【００９９】
そこで、「蓋を開ける」操作の事後条件として
“蓋を開ける not in 温度制御状態”
を仕様記述に追加する。
【０１００】
当該仕様記述に基づき再び解釈例を生成すると、図18のグラフを得られ、所望の遷移が確認できる。図19は、ここまで述べてきた修正を反映した仕様記述を示す。図15の仕様記述に対して、記述101〜103が追加されている。
【０１０１】
なお、上記の例では事後条件が抜けている場合を示したが、事前条件が抜けている場合も本実施例は適用可能である。
【０１０２】
このように、仕様記述に対して、解釈例を生成し、解釈例に基づき遷移を確認しながら不足している事前条件や事後条件を修正（追加、削除、変更）し、仕様記述を完成させる。仕様記述を元の要求仕様にフィードバックすることで、不備のない要求仕様を生成できる。
【０１０３】
なお、以上に説明した本実施形態における仕様検証装置は、例えば、汎用のコンピュータ装置を基本ハードウェアとして用いることで実現することが可能である。すなわち、仕様検証装置の各処理部は、上記のコンピュータ装置に搭載されたプロセッサにプログラムを実行させることにより実現することができる。このとき、仕様検証装置は、上記のプログラムをコンピュータ装置にあらかじめインストールすることで実現してもよいし、CD-ROMなどの記憶媒体に記憶して、あるいはネットワークを介して上記のプログラムを配布して、このプログラムをコンピュータ装置に適宜インストールすることで実現してもよい。また、仕様検証装置内の記憶部またはデータベースは、装置内もしくは外付けのメモリ装置およびハードディスク、あるいは、CD-R, CD-RW, DVD-RAM, DVD-R 等の記録媒体によって構成されてもよい。
【０１０４】
なお、本発明は前記実施形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化できる。また、前記実施形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成できる。例えば、実施形態に示される全構成要素から幾つかの構成要素を削除してもよい。さらに、異なる実施形態にわたる構成要素を適宜組み合わせてもよい。また、以下に例示するような種々の変形が可能である。
【図１】
2014081680.tif 000007
【図２】
2014081680.tif 000008
【図３】
2014081680.tif 000009
【図４】
2014081680.tif 000010
【図５】
2014081680.tif 000011
【図６】
2014081680.tif 000012
【図７】
2014081680.tif 000013
【図８】
2014081680.tif 000014
【図９】
2014081680.tif 000015
【図１０】
2014081680.tif 000016
【図１１】
2014081680.tif 000017
【図１２】
2014081680.tif 000018
【図１３】
2014081680.tif 000019
【図１４】
2014081680.tif 000020
【図１５】
2014081680.tif 000021
【図１６】
2014081680.tif 000022
【図１７】
2014081680.tif 000023
【図１８】
2014081680.tif 000024
【図１９】
2014081680.tif 000025