(57)【特許請求の範囲】
【請求項１】
自然言語から形式言語に変換して仕様書を作成する仕様書作成支援装置であって、
要件ごとに、当該要件の自然言語による表現形式と、当該要件の形式言語による表現形式と、当該自然言語による表現形式に求められる入力情報の各々について当該入力情報の仕様書における参照元を示す入力参照元と、を有する記述変換ルールと、
自然言語で記載された不足要件導出要件形式と形式言語で記載された不足要件導出要件形式とを有する不足要件導出要件形式と、自然言語で記載された不足要件形式と、を有する要件補間ルールと、
前記記述変換ルールに基づき、一以上の自然言語による表現形式の候補を出力する自然言語形式出力手段と、
前記一以上の自然言語による表現形式の候補から一以上の自然言語による表現形式の選択を受け付ける自然言語表現受付手段と、
前記記述変換ルールに基づき、前記自然言語表現受付手段が受け付けた前記一以上の自然言語による表現形式各々に対応する入力参照元を当該一以上の自然言語による表現形式に求められる入力情報の候補として出力する入力情報候補出力手段と、
前記入力情報の候補から前記一以上の自然言語による表現形式各々に対する入力情報の選択を受け付ける入力情報受付手段と、
選択された前記一以上の自然言語による表現形式と前記入力情報から、自然言語により表現された一以上の要件を生成し、当該自然言語により表現された一以上の要件を有する自然言語の仕様書を作成する自然言語仕様書作成手段と、
前記自然言語の仕様書に含まれる各要件について、当該要件の生成に用いられた自然言語による表現形式と対応する自然言語で記載された不足要件導出要件形式が前記要件補間ルールに登録されているか検索する不足要件導出要件形式検索手段と、
前記不足要件導出要件形式検索手段によって抽出された自然言語で記載された不足要件導出要件形式と対応付けられている形式言語で記載された不足要件導出要件形式に前記要件の作成に用いられた入力情報を適用し、不足要件導出情報を生成する不足要件導出情報生成手段と、
前記要件補間ルールに基づき、前記不足要件導出要件形式検索手段によって抽出された自然言語で記載された不足要件導出要件形式についての不足要件形式を抽出し、当該不足要件形式に前記不足要件導出情報を適用して自然言語で記載された不足要件を生成する不足要件生成手段と、
前記自然言語で記載された不足要件を前記自然言語の仕様書に追記する不足要件追記手段と、
当該自然言語の仕様書を前記記述変換ルールに基づいて形式言語の仕様書に変換し形式言語の仕様書を生成する言語変換手段と、
前記形式言語の仕様書を検証する仕様書検証手段と、を有する
ことを特徴とする仕様書作成支援装置。
【請求項２】
請求項１にかかる仕様書作成支援装置であって、
前記要件補間ルールの前記不足要件導出要件形式は、第一の自然言語で記載された不足要件導出要件形式と、第一の形式言語で記載された不足要件導出要件形式と、第二の自然言語で記載された不足要件導出要件形式と、第二の形式言語で記載された不足要件導出要件形式と、を有し、
前記不足要件導出要件形式検索手段は、
前記自然言語による仕様書に含まれる各要件について、当該要件の生成に用いられた自然言語による表現形式と対応する第一の自然言語で記載された不足要件導出要件形式が前記要件補間ルールに登録されているか検索し、
前記不足要件導出情報生成手段は、
前記不足要件導出要件形式検索手段によって抽出された前記第一の自然言語で記載された不足要件導出要件形式と対応づけられている第一の形式言語で記載された不足要件導出要件形式に、前記要件の作成に用いられた入力情報を適用し、第一の不足要件導出情報を生成し、
前記不足要件導出要件形式検索手段は、
前記要件補間ルールに基づき、当該不足要件導出要件形式検索手段によって抽出された前記第一の自然言語で記載された不足要件導出要件形式に対応する第二の自然言語で記載された不足要件導出要件形式を抽出し、当該第二の自然言語で記載された不足要件導出要件形式と対応する要件が、前記自然言語による仕様書に存在するか検索し、
前記不足要件導出情報生成手段は、
前記第二の自然言語で記載された不足要件導出要件形式と対応する要件が前記自然言語による仕様書に存在する場合に、前記第二の自然言語で記載された不足要件導出要件形式と前記第一の不足要件導出情報から、第二の不足要件導出情報を生成し、
前記不足要件生成手段は、
前記要件補間ルールに基づき、前記第一の自然言語で記載された不足要件導出要件形式及び前記第二の自然言語で記載された不足要件導出要件形式に対応する自然言語で記載された不足要件形式を抽出し、当該自然言語で記載された不足要件形式に前記第一の不足要件導出情報と前記第二の不足要件導出情報を適用して自然言語で記載された不足要件を生成する
ことを特徴とする仕様書作成支援装置。
【請求項３】
請求項２にかかる仕様書作成支援装置であって、
さらに、前記仕様書検証手段による前記形式言語の仕様書の検証に失敗した場合に、前記自然言語の仕様書または前記形式言語の仕様書の修正を受け付ける仕様書修正手段を有し、
前記仕様書修正手段により前記自然言語の仕様書の修正を受け付けた場合は、前記仕様書作成支援装置は、修正された自然言語の仕様書に含まれる各要件について、自然言語で記載された不足要件を生成して当該修正された自然言語の仕様書に追記する
ことを特徴とする仕様書作成支援装置。
【請求項４】
請求項３にかかる仕様書作成支援装置であって、
前記記述変換ルールは、さらに、要件ごとに当該要件を一意に識別する変換識別子を有し、
前記要件補間ルールの不足要件導出要件形式の各々は、さらに、当該不足要件導出要件形式と対応する要件の変換識別子を有し、
前記不足要件導出要件形式検索手段は、前記自然言語の仕様書に記載された各々の要件について、当該要件の変換識別子と同じ変換識別子を有する不足要件導出要件形式が前記要件補間ルールに登録されているか検索する
ことを特徴とする仕様書作成支援装置。
【請求項５】
形式言語で仕様書を生成する仕様書作成支援装置であって、
形式言語で記載された第一の不足要件導出要件形式と、形式言語で記載された第二の不足要件導出要件形式と、形式言語で記載された不足要件形式と、を有する要件補間ルールと、
形式言語による仕様書に記載された要件各々について、当該要件の形式と対応する第一の不足要件導出要件形式が前記要件補間ルールに登録されているか検索する第一不足要件導出要件形式検索手段と、
前記第一不足要件導出要件形式検索手段によって抽出された前記第一の不足要件導出要件形式に前記要件を構成する入力情報を適用し、第一の不足要件導出情報を生成する第一不足要件導出情報生成手段と、
前記要件補間ルールに基づき、前記第一不足要件導出要件形式検索手段によって抽出された前記第一の不足要件導出要件形式に対応する第二の不足要件導出要件形式を抽出し、当該第二の不足要件導出要件形式に対応する要件が前記形式言語による仕様書に存在するか検索する第二不足要件導出要件形式検索手段と、
前記第二不足要件導出要件形式検索手段によって抽出された前記第二の不足要件導出要件形式に前記第一の不足要件導出情報を適用し、第二の不足要件導出情報を生成する第二不足要件導出情報生成手段と、
前記要件補間ルールに基づき、前記第一の不足要件導出要件形式及び前記第二の不足要件導出要件形式に対応する不足要件形式を抽出し、当該不足要件形式に前記第一の不足要件導出情報と第二の不足要件導出情報を適用して、形式言語で記載された不足要件を生成する不足要件生成手段と、
前記形式言語で記載された不足要件を前記形式言語の仕様書に追記する不足要件追記手段と、
前記形式言語の仕様書を検証する仕様書検証手段と、を有する
ことを特徴とする仕様書作成支援装置。
【請求項６】
自然言語から形式言語に変換して仕様書を作成する仕様書作成支援装置における方法であって、
前記仕様書作成支援装置は、
自然言語仕様作成部と、モデル変換部と、形式検証実行部と、
要件ごとに、当該要件の自然言語による表現形式と、当該要件の形式言語による表現形式と、当該自然言語による表現形式に求められる入力情報の各々について当該入力情報の仕様書における参照元を示す入力参照元と、を有する記述変換ルールと、
自然言語で記載された不足要件導出要件形式と形式言語で記載された不足要件導出要件形式とを有する不足要件導出要件形式と、自然言語で記載された不足要件形式と、を有する要件補間ルールと、
を有し、
前記自然言語仕様作成部が、
前記記述変換ルールに基づき、一以上の自然言語による表現形式の候補を出力する自然言語形式出力ステップと、
前記一以上の自然言語による表現形式の候補から一以上の自然言語による表現形式の選択を受け付ける自然言語表現受付ステップと、
前記記述変換ルールに基づき、前記自然言語表現受付ステップが受け付けた前記一以上の自然言語による表現形式各々に対応する入力参照元を当該一以上の自然言語による表現形式に求められる入力情報の候補として出力する入力情報候補出力ステップと、
前記入力情報の候補から前記一以上の自然言語による表現形式各々に対する入力情報の選択を受け付ける入力情報受付ステップと、
選択された前記一以上の自然言語による表現形式と前記入力情報から、自然言語により表現された一以上の要件を生成し、当該自然言語により表現された一以上の要件を有する自然言語の仕様書を作成する自然言語仕様書作成ステップと、
前記自然言語の仕様書に含まれる各要件について、当該要件の生成に用いられた自然言語による表現形式と対応する自然言語で記載された不足要件導出要件形式が前記要件補間ルールに登録されているか検索する不足要件導出要件形式検索ステップと、
前記不足要件導出要件形式検索ステップによって抽出された自然言語で記載された不足要件導出要件形式と対応付けられている形式言語で記載された不足要件導出要件形式に前記要件の作成に用いられた入力情報を適用し、不足要件導出情報を生成する不足要件導出情報生成ステップと、
前記要件補間ルールに基づき、前記不足要件導出要件形式検索ステップによって抽出された自然言語で記載された不足要件導出要件形式についての不足要件形式を抽出し、当該不足要件形式に前記不足要件導出情報を適用して自然言語で記載された不足要件を生成する不足要件生成ステップと、
前記自然言語で記載された不足要件を前記自然言語の仕様書に追記する不足要件追記ステップと、
を有し、
前記モデル変換部が、
当該自然言語の仕様書を前記記述変換ルールに基づいて形式言語の仕様書に変換し形式言語の仕様書を生成する言語変換ステップと、
前記形式検証実行部が、
前記形式言語の仕様書を検証する仕様書検証ステップと、を有する
ことを特徴とする方法。
【請求項７】
請求項６にかかる方法であって、
前記要件補間ルールの前記不足要件導出要件形式は、第一の自然言語で記載された不足要件導出要件形式と、第一の形式言語で記載された不足要件導出要件形式と、第二の自然言語で記載された不足要件導出要件形式と、第二の形式言語で記載された不足要件導出要件形式と、を有し、
前記不足要件導出要件形式検索ステップは、
前記自然言語による仕様書に含まれる各要件について、当該要件の生成に用いられた自然言語による表現形式と対応する第一の自然言語で記載された不足要件導出要件形式が前記要件補間ルールに登録されているか検索し、
前記不足要件導出情報生成ステップは、
前記不足要件導出要件形式検索ステップによって抽出された前記第一の自然言語で記載された不足要件導出要件形式と対応づけられている第一の形式言語で記載された不足要件導出要件形式に、前記要件の作成に用いられた入力情報を適用し、第一の不足要件導出情報を生成し、
前記不足要件導出要件形式検索ステップは、
前記要件補間ルールに基づき、当該不足要件導出要件形式検索ステップによって抽出された前記第一の自然言語で記載された不足要件導出要件形式に対応する第二の自然言語で記載された不足要件導出要件形式を抽出し、当該第二の自然言語で記載された不足要件導出要件形式と対応する要件が、前記自然言語による仕様書に存在するか検索し、
前記不足要件導出情報生成ステップは、
前記第二の自然言語で記載された不足要件導出要件形式と対応する要件が前記自然言語による仕様書に存在する場合に、前記第二の自然言語で記載された不足要件導出要件形式と前記第一の不足要件導出情報から、第二の不足要件導出情報を生成し、
前記不足要件生成ステップは、
前記要件補間ルールに基づき、前記第一の自然言語で記載された不足要件導出要件形式及び前記第二の自然言語で記載された不足要件導出要件形式に対応する自然言語で記載された不足要件形式を抽出し、当該自然言語で記載された不足要件形式に前記第一の不足要件導出情報と前記第二の不足要件導出情報を適用して自然言語で記載された不足要件を生成する
ことを特徴とする方法。
【請求項８】
請求項７にかかる方法であって、
さらに、前記仕様書検証ステップによる前記形式言語の仕様書の検証に失敗した場合に、前記自然言語の仕様書または前記形式言語の仕様書の修正を受け付ける仕様書修正ステップを有し、
前記仕様書修正ステップにより前記自然言語の仕様書の修正を受け付けた場合は、前記方法は、修正された自然言語の仕様書に含まれる各要件について、自然言語で記載された不足要件を生成して当該修正された自然言語の仕様書に追記する
ことを特徴とする方法。
【請求項９】
請求項８にかかる方法であって、
前記記述変換ルールは、さらに、要件ごとに当該要件を一意に識別する変換識別子を有し、
前記要件補間ルールの不足要件導出要件形式の各々は、さらに、当該不足要件導出要件形式と対応する要件の変換識別子を有し、
前記不足要件導出要件形式検索ステップは、前記自然言語の仕様書に記載された各々の要件について、当該要件の変換識別子と同じ変換識別子を有する不足要件導出要件形式が前記要件補間ルールに登録されているか検索する
ことを特徴とする方法。
【請求項１０】
形式言語で仕様書を生成する仕様書作成支援装置における方法であって、
前記仕様書作成支援装置は、
形式言語仕様作成部と、形式検証実行部と、
形式言語で記載された第一の不足要件導出要件形式と、形式言語で記載された第二の不足要件導出要件形式と、形式言語で記載された不足要件形式と、を有する要件補間ルールと、
を有し、
前記形式言語仕様作成部が、
形式言語による仕様書に記載された要件各々について、当該要件の形式と対応する第一の不足要件導出要件形式が前記要件補間ルールに登録されているか検索する第一不足要件導出要件形式検索ステップと、
前記第一不足要件導出要件形式検索ステップによって抽出された前記第一の不足要件導出要件形式に前記要件を構成する入力情報を適用し、第一の不足要件導出情報を生成する第一不足要件導出情報生成ステップと、
前記要件補間ルールに基づき、前記第一不足要件導出要件形式検索ステップによって抽出された前記第一の不足要件導出要件形式に対応する第二の不足要件導出要件形式を抽出し、当該第二の不足要件導出要件形式に対応する要件が前記形式言語による仕様書に存在するか検索する第二不足要件導出要件形式検索ステップと、
前記第二不足要件導出要件形式検索ステップによって抽出された前記第二の不足要件導出要件形式に前記第一の不足要件導出情報を適用し、第二の不足要件導出情報を生成する第二不足要件導出情報生成ステップと、
前記要件補間ルールに基づき、前記第一の不足要件導出要件形式及び前記第二の不足要件導出要件形式に対応する不足要件形式を抽出し、当該不足要件形式に前記第一の不足要件導出情報と第二の不足要件導出情報を適用して、形式言語で記載された不足要件を生成する不足要件生成ステップと、
前記形式言語で記載された不足要件を前記形式言語の仕様書に追記する不足要件追記ステップと、
を有し、
前記形式検証実行部が、
前記形式言語の仕様書を検証する仕様書検証ステップと、を有する、
ことを特徴とする方法。
【発明の詳細な説明】
【技術分野】
【０００１】
ソフトウェア開発を支援する技術に関し、特に、ソフトウェア仕様の作成、及び、検証、修正する技術に関する。
【背景技術】
【０００２】
ソフトウェアの仕様作成に当たっては、曖昧さや誤りのない仕様を記述することによって設計品質を向上させ、ソフトウェア開発における出戻りを低減することが重要である。そこで、厳密な仕様記述が可能な記述言語を用いて仕様作成を行い、その検証を行うことによって、曖昧性や誤りのない仕様を作成する、形式検証技術が知られている。なお、以下では、形式検証技術によって作成された仕様を、形式言語仕様と呼ぶ。
【０００３】
また、形式言語仕様のための仕様作成、検証を行うための支援ツールが知られている。例えば、モデル規範型記述言語のひとつである「Ｅｖｅｎｔ−Ｂ」では、その仕様作成支援ツールとして「Ｒｏｄｉｎ  Ｐｌａｔｆｏｒｍ」（非特許文献１）が知られている。  これらの仕様作成支援ツールを用いて形式言語仕様を作成するためには、図や自然言語によって表現されていた仕様記述（自然言語仕様）を、形式言語仕様で表現しなおし、仕様の検証、修正を行う必要がある。そのため、形式言語仕様を用いて、曖昧さや誤りのない仕様を作成するためには、形式検証技術に精通している必要がある。
【０００４】
そこで形式検証技術に精通していない設計者に対して、曖昧さや誤りのない仕様作成を支援するための設計書作成支援方法が知られている。例えば、特許文献１では、予め自然言語仕様から形式言語仕様への変換規則を定めておき、設計者の仕様作成を支援することによって、形式言語仕様を直接記述しなくとも、曖昧さや誤りを低減する、設計書作成支援方法が開示されている。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２００８−１５８８５３
【非特許文献】
【０００６】
【非特許文献１】Ｅｖｅｎｔ−Ｂ．ｏｒｇ、“Ｅｖｅｎｔ−Ｂ  ａｎｄ  Ｒｏｄｉｎ  Ｐｌａｔｆｏｒｍ”［Ｏｎｌｉｎｅ］，［平成２３年７月１１日検索］，インターネット＜ＵＲＬ：ｈｔｔｐ：／／ｗｗｗ．ｅｖｅｎｔ−ｂ．ｏｒｇ／＞
【発明の概要】
【発明が解決しようとする課題】
【０００７】
従来技術では、自然言語仕様から形式言語仕様への変換規則を定めることによって、自然言語を用いて、形式検証技術に基づく曖昧さや誤りのない設計書の作成を支援することを目的としている。
【０００８】
しかしながら、形式言語仕様の作成に当たっては、従来の自然言語による仕様作成と比較して、より厳密な仕様記述の作成が必要となる。そのため、従来の自然言語仕様では意識しなかった要件も明示的に記述することが必要となる。そこで、形式検証技術を用いた仕様作成に当たって、仕様内に記述された要件から不足している要件を生成することで、曖昧さや誤りのない仕様作成を支援することを目的とする。
【課題を解決するための手段】
【０００９】
上記の課題に対し、本発明では、要件ごとに、当該要件の自然言語による表現形式と、当該要件の形式言語による表現形式と、当該自然言語による表現形式に求められる入力情報の各々について当該入力情報の仕様書における参照元を示す入力参照元と、を有する記述変換ルールと、自然言語で記載された不足要件導出要件形式と形式言語で記載された不足要件導出要件形式とを有する不足要件導出要件形式と、自然言語で記載された不足要件形式と、を有する要件補間ルール有し、前記記述変換ルールに基づき、一以上の自然言語による表現形式の候補を出力し、前記一以上の自然言語による表現形式の候補から一以上の自然言語による表現形式の選択を受け付け、前記記述変換ルールに基づき、前記事前言語表現受付手段が受け付けた前記一以上の自然言語による表現形式各々に対応する入力参照元を当該一以上の自然言語による表現形式に求められる入力情報の候補として出力し、前記入力情報の候補から前記一以上の自然言語による表現形式各々に対する入力情報の選択を受け付け、選択された前記一以上の自然言語による表現形式と前記入力情報から、自然言語により表現された一以上の要件を生成し、当該自然言語により表現された一以上の要件を有する自然言語の仕様書を作成し、前記自然言語の仕様書に含まれる各要件について、当該要件の生成に用いられた自然言語による表現形式と対応する自然言語で記載された不足要件導出要件形式が前記要件補間ルールに登録されているか検索し、抽出された自然言語で記載された不足要件導出要件形式と対応付けられている形式言語で記載された不足要件導出要件形式に前記要件の作成に用いられた入力情報を適用し、不足要件導出情報を生成し、前記要件補間ルールに基づき、抽出された自然言語で記載された不足要件導出要件形式についての不足要件形式を抽出し、当該不足要件形式に前記不足要件導出情報を適用して自然言語で記載された不足要件を生成し、前記自然言語で記載された不足要件を前記自然言語の仕様書に追記し、当該自然言語の仕様書を前記記述変換ルールに基づいて形式言語の仕様書に変換し形式言語の仕様書を生成し、前記形式言語の仕様書を検証することを特徴とする。
【発明の効果】
【００１０】
形式検証技術を用いたソフトウェア仕様の作成に当たって、厳密な仕様作成を支援し、曖昧さや誤りのない仕様作成の支援が可能となる。
【図面の簡単な説明】
【００１１】
【図１】第一の実施例における仕様作成支援装置の構成を示すブロック図の一例である。
【図２】仕様作成支援装置のハードウェア構成の一例を示す図である。
【図３】第一の実施例における自然言語仕様と形式言語仕様の対応関係の一例を示す図である。
【図４】第一の実施例における自然言語仕様の作成処理の概要を示す図である。
【図５】第一の実施例における自然言語と形式言語の記述/変換ルール表の一例を示す図である。
【図６】第一の実施例における要件補間ルールの構成の一例を示す図である。
【図７】第一の実施例における記述/変換ルールに基づき自然言語仕様を作成するフローの一例を示す図である。
【図８】第一の実施例における記述/変換ルールに基づき自然言語から形式言語に変換するための処理フローの一例を示す図である。
【図９】第一の実施例における要件補間ルールに基づき、不足要件を生成するための処理フローの一例を示す図である。
【図１０】第一の実施例における自然言語仕様作成部による仕様作成の一例を示す図である。
【図１１】第一の実施例における自然言語仕様格納ＤＢ内に格納された自然言語仕様の一例を示す図である。
【図１２】第一の実施例における要件補間ルールに基づき、自然言語仕様を修正した結果の一例を示す図である。
【図１３】形式言語仕様の一例を示す図である。
【図１４】第二の実施例における仕様作成支援装置の最小構成を示すブロック図の一例である。
【図１５】第二の実施例における要件補間ルールの構成の一例を示す図である。
【発明を実施するための形態】
【実施例１】
【００１２】
図１は、本実施例の仕様作成支援装置１００の構成図である。仕様作成支援装置１００は、入力部１０１、表示部１０６、入出力制御部１０７、自然言語仕様作成部１０２、モデル変換部１０３、形式仕様作成部１０４、形式検証実行部１０５、及び、要件補間ルール格納データベース（要件補間ルール格納ＤＢ１２０）、自然言語仕様格納データベース（自然言語仕様格納ＤＢ１２１）、及び、記述/変換ルール格納データベース（記述/変換ルール格納ＤＢ１２２）、及び、形式仕様格納データベース（形式仕様格納ＤＢ１２３）を備える。また、自然言語仕様作成部は、設計書作成部１０８、要件補間部１０９、及び、要件記述部１１０を備える。
【００１３】
ここで、自然言語仕様格納ＤＢ１２１は、自然言語仕様を格納するための格納領域であり、形式仕様格納ＤＢ１１３は、形式言語仕様を格納するための格納領域である。また、記述/変換ルール格納ＤＢ１１２は、自然言語仕様作成のための記述ルールと作成された自然言語仕様と形式言語仕様とを相互に変換するための変換ルールを格納した格納領域であり、要件補間ルール格納ＤＢ１１０は、作成された自然言語仕様内で、不足している要件を補完するためのルールを格納した格納領域である。
【００１４】
形式検証実行部１０５は、形式仕様格納ＤＢ１２３に格納された形式言語仕様を基に、形式言語の構文チェック、検証等を行う。また、モデル変換部１０３は、記述/変換ルール格納ＤＢ１２２の変換ルールに従い、自然言語仕様格納ＤＢ１２１に格納された自然言語仕様を形式仕様言語への変換、又は、その逆変換を行うとともに、形式検証実行部１０５における検証結果を自然言語仕様格納ＤＢ１２１に反映する。
【００１５】
自然言語仕様作成部１０２は設計書作成部１０８、要件補間部１０９、及び、要件記述部１１０とを含んで構成される。設計書作成部１０８は、自然言語仕様に基づく設計書を作成するための処理部であり、設計書作成部１０８は、要件記述部１１０と通信し、記述/変換ルールに従い、入力部１０１からのユーザ入力を受付、自然言語による要件記述、及び、仕様作成を行う。さらに、設計書作成部１０８は、要件補間部１０９と通信し、作成された要件から不足している要件を生成する。
【００１６】
なお、形式言語仕様作成部１０４は、直接形式言語仕様を作成するための処理部であり、形式仕様作成部１０４、形式仕様格納ＤＢ１２３、形式検証実行部１０５は、形式検証技術に関わる、仕様記述、及び、構文チェック、検証を行う、既存の形式検証技術の仕様作成支援ツール（例えば、非特許文献１）を用いて構成よい。
【００１７】
本実施例によれば、ユーザは仕様作成支援装置１００内の記述/変換ルール格納ＤＢ１２２内に格納された記述/変換ルールに格納された記述ルールに基づき自然言語仕様を作成することで、形式言語仕様への変換を行う。また、要件補間ルール格納ＤＢ１２０内に格納された要件補間ルールを用いることで、自然言語仕様内に記述された要件から不足している要件を生成する。これによって、ユーザに対し、形式言語仕様を利用した曖昧さや誤りのない仕様作成のための支援を行う。
【００１８】
図２は、図1に示した仕様作成支援装置１００を実現するハードウェア構成の一例を示している。
【００１９】
図２の構成例では、仕様作成支援装置１００は、ＣＰＵ（Ｃｅｎｔｒａｌ Ｐｒｏｃｅｓｓｏｒ Ｕｎｉｔ）２０１、ＲＡＭ（Ｒａｎｄｏｍ Ａｃｃｅｓｓ Ｍｅｍｏｒｙ）２０２、入力装置１０１、表示装置２０４、及び、外部記憶装置２１０がインターフェイス２０５を介して接続された、一般的な構成を有するコンピュータ（電子計算機）である。
【００２０】
入力装置１０１は、例えば、キーボードやマウスなどであり、表示装置２０４は、表示用ディスプレイ、外部記憶装置２１０は、ＨＤＤ（Ｈａｒｄ Ｄｉｓｋ Ｄｒｉｖｅ）などである。ＣＰＵ２０１は、ＲＡＭ２０２上にロードしたプログラムを実行することで、図１に示す自然言語仕様作成部１０２、モデル変換部１０３、形式言語仕様作成部１０４、及び、形式検証実行部１０５をプロセスとして具現化する。また、インターフェイス２０５は、装置内の各構成要素間のデータを送受信する内部パスであり、外部記憶装置２１０には、各データベース(要件補間ルール格納ＤＢ１２０など)、及び、自然言語仕様作成部１０２、モデル変換部１０３、形式言語仕様作成部１０４、及び、形式検証実行部１０５の実行プログラムが格納される。表示装置２０３は、自然言語仕様作成部１０２、形式言語仕様作成部１０４において、作成中の自然言語仕様、又は、形式言語仕様をディスプレイ等に表示する。
【００２１】
以下、本実施例では、形式言語仕様としてモデル規範型仕様記述言語「Ｅｖｅｎｔ−Ｂ」を用いた場合を例として、設計書支援装置１００について説明する。なお、以下では「Ｅｖｅｎｔ−Ｂ」を例として仕様作成支援装置１００の具体的な構成について説明するが、本発明は、例えば「Ｂ−ｍｅｔｈｏｄ」など、他のモデル規範型仕様記述言語でも同様に実現可能である。
【００２２】
図３は、Ｅｖｅｎｔ−Ｂを用いた場合の本実施例における自然言語仕様３０１と形式言語仕様３２０の対応関係を表している。形式言語「Ｅｖｅｎｔ−Ｂ」では、形式言語仕様は、Ｃｏｎｔｅｘｔ  ３２１、ＭＡＣＨＩＮＥ  ３２３から構成される。Ｃｏｎｔｅｘｔ  ３２１内には、形式言語仕様(Ｅｖｅｎｔ−Ｂでは、抽象機械と呼ばれる)を作成するための集合３３１、定数に関する情報３３２が含まれ、ＭＡＣＨＩＮＥ  ３２３には、システムの状態を表す変数３３３、及び、変数の満たすべき条件を示した不変条件３３４、変数の初期化３３９、及び、変数の状態変化の事前条件３３７、事後条件(アクション)３３８を記述するイベント３３５が含まれる。
【００２３】
図３に図示したごとく、第一の実施例では、形式言語仕様３２０に対応する自然言語仕様３０１は、集合一覧３０５、定数一覧３０６からなるモデリング情報３０２、変数一覧３０７、データ要件一覧３０８からなるデータ要件関連情報３０３、及び、ユースケース設計書３０４から構成される。ここでユースケース設計書３０４は、各ユースケースのユースケース名３０９、ユースケース概要３１０、パラメータ３１１、事前条件３１２、アクション３１３から構成される。なお、図３の矢印は、モデリング情報３０２、データ要件関連情報３０３、ユースケース設計書３０４が、形式言語仕様３２０内の対応する構成要素を表している。
【００２４】
図３に示した設計書の構成、及び、名称は特に上記に限らなくてもよい。また、設計書の作成単位も、上記に限らず、例えば、モデリング情報３０２、及び、データ要件関連情報３０３を、ひとつの設計書としてまとめてもよい。また、設計書の記載内容は、上記以外の項目を含んで構成されてもよい。
【００２５】
図４は、図3に示した自然言語仕様による仕様作成フローの概略を示している。そのフローは以下のとおりである。
４０１：開始
４０２：入力部１０１がユーザから記述/変換ルール１１２に基づく入力を受け付け、自然言語作成部１０２の設計書作成部１０８、要件記述部１１１が、モデリング情報３０２を作成する。
４０３：入力部１０１がユーザから記述/変換ルール１１２に基づく入力を受け付け、自然言語作成部１０２の設計書作成部１０８、要件記述部１１１が、データ要件関連３０３を作成する。
４０４：入力部１０１がユーザから記述/変換ルール１１２に基づく入力を受け付け、自然言語作成部１０２の設計書作成部１０８、要件記述部１１１が、ユースケース設計書３０４を作成する。
４０５：すべてのユースケース設計書を作成した場合にはステップ４０６へ。まだ作成するユースケース設計書がある場合にはステップ４０４に進む。
４０６：自然言語作成部１０２の設計書作成部１０８、及び、要件補間部１１２が、要件補間ルール１２０に基づき作成した仕様内の要件から不足要件を生成し、設計書に反映する。
４０７：ユーザが自然言語仕様作成部１０２から、モデル変換部１０３を呼び出し、モデル変換部１０３を用いて、自然言語作成部１０２で作成した自然言語仕様３０２を形式言語仕様３２０に変換する。
４０８：仕様作成支援装置１００が、形式検証実行部を用いて、ステップ４０７で生成した形式言語仕様３２０の構文チェック、検証を行い、その結果を自然言語仕様３２０に反映する。
４０９： すべての要件(証明責務)が検証に成功した場合にはステップ４１１に進み、検証に失敗した要件があれば４１０に進む。
４１０：ユーザが自然言語仕様作成部１０２を用いて、ステップ４０２、４０３、４０４と同様の作業を行い、自然言語仕様の修正を行う。
４１１：終了
なお、上記の作成フローでは、すべてのユースケース設計書が作成された後、ステップ４０６以降で、要件の補間（ステップ４０６）、形式言語仕様への変換（ステップ４０７）、形式言語仕様の検証（ステップ４０８）を行っているが、上記に限らず、例えば、各設計書の作成段階(ステップ４０２、４０３，４０４)ごとにステップ４０６、４０７、４０８の処理を実行してもよい。また、ユーザが明示的にステップ４０６、４０７、４０８等の処理を呼び出すのではなく、ユーザの要件記述に合わせ、設計書作成部１０８が自動で呼び出すようにしてもよい。
【００２６】
ステップ４１０における仕様の修正は、自然言語仕様作成部１０２ではなく、形式言語仕様作成部１０４を用いて、形式言語仕様３２０に対して直接行い、その結果を、モデル変換部１０３を用いて、自然言語仕様３０１に反映してもよい。
【００２７】
上記処理では、自然言語仕様から形式言語仕様を全て作成することを想定した処理フローとなっているが、上記と異なっていてもよい。例えば、既存のシステム、或いは、複数のシステムで共通的に使われる項目がある場合には、モデリング情報３０２、或いは、データ要件関連情報３０３の一部を予め作成しておき、これらを用いて仕様作成を行ってもよい。
【００２８】
図５は、本実施例における記述/変換ルールＤＢ１２２内に格納された記述/変換ルールの一例を示している。図５に示したごとく、本実施例における記述/変換ルールＤＢ１２２は、記述/変換ルールの識別子を表す変換ＩＤ５０１、自然言語仕様内での要件記述パターンを表した自然言語表現５０３、自然言語表現に対応する形式言語仕様内での要件記述パターンを表した形式言語表現５０４を含み構成される。また、各記述/変換ルールには、変数、不変条件など、その記述/変換ルールが利用可能な対象５０２、及び、各記述/変換ルールを用いて要件インスタンスを生成する際に必要となる入力情報５０５が含まれる。
【００２９】
本実施例の入力情報５０５の参照元５０６、５０８、及び、次に示す図６の不足要件導出要件６０２及び不足要件６０５の対象６０６、６０８、６１０では、自然言語仕様書３０１の集合一覧３０５を参照する場合はＳ（Ｓｅｔ）、定数一覧３０６を参照する場合は、Ｃ（Ｃｏｎｓｔａｎｔ）、変数一覧３０７を参照する場合はＶ（Ｖａｒｉａｂｌｅｓ）、データ要件一覧３０８を参照する場合はＩ（Ｉｎｖａｒｉａｎｔｓ）、イベントのパラメータ３１１を参照する場合にはＰ（Ｐａｒameter），事前条件３１２を参照する場合はＷ（Ｗｈｅｒｅ）、アクション３１３を参照する場合はＡ（Ａｃｔｉｏｎ）と略記している。なお、入力情報５０５の参照元５０６、５０８には、仕様記述のために宣言した集合一覧３０５、定数一覧３０６、変数一覧３０７、パラメータ３１１のいずれかから選択するため、Ｓ，Ｃ，Ｖ，Ｐのいずれかとなる。同様に、種別５０７，５０９は、入力情報の種別が要素の場合はＥ（Ｅｌｅｍｅｎｔ），集合の場合はＳ（Ｓｅｔ）と略記している。なお、種別は、要素や集合だけでなく、例えば写像等、上記以外の種別を追加してもよい。また、例えばクラスや属性など、異なる観点で纏めてもよい。
【００３０】
次に図６は、本実施例における要件補間ルールＤＢ１２０内に格納された記述/変換ルールの一例を示している。図６に示したごとく、要件補間ルールＤＢ１２０は、要件補間ルールの識別子を表す補間ＩＤ６０１と、不足要件の記述パターンを記述した不足要件６０５と不足要件を生成するための条件（仕様内の要件記述パターン）を記述した不足要件導出要件６０２とからなる。不足要件導出要件６０２は、さらに基底要件６０３、従属要件６０４から構成される。なお、基底要件６０３、従属要件６０４は、不足要件導出要件６０２として、ひとつの列としてまとめてもよいが、本実施例では、不足要件(不足要件６０５)の導出を容易にするため、基底要件６０３、従属要件６０４の二つの列に分けている。これは、仕様内から不足要件導出要件６０２を用いて不足要件の生成を行う際、全ての不足要件導出要件を纏めて検索する手間を低減するためである。不足要件の生成に当たっては、まず基底要件６０３を元に該当する不足要件の候補を探索し、該当する候補に対して、仕様内の要件記述から従属要件６０４を絞り込むことで、不足している要件の特定、生成を行う。
【００３１】
以下に、図５、図６を用いた、要件記述部１１０による要件の記述処理、モデル変換部１０３による形式言語仕様への変換処理、及び、要件補間部１０９による不足要件の生成処理の処理フローについて説明する。なお、具体例は図１０から図１３を用いて後述する。
【００３２】
図７は、本実施例における各設計書内への要件記述の処理フロー（要件記述部１１０における処理フロー、図４ステップ４０２〜ステップ４０４の処理）の概略を示している。
７０１：開始
７０２：要件記述部１１０が、記述/変換ルールＤＢ１２２から、対象５０２に基づき、記述項目に応じた記述/変換ルールを読み込み、読み込んだ記述/変換ルールの一覧を表示する。
７０３：表示した記述/変換ルールの一覧からユーザが選択した記述/変換ルールを入力部１０１が受け付け、要件記述部１１０に送る。
７０４：要件記述部１１０が、受け付けた記述/変換ルールから、対応する入力情報５０５を読み込む。
７０５：入力情報がまだあればステップ７０５に、なければ７１１に進む。
７０６：要件記述部１１０が、入力情報５０５から参照元情報を取得する。
７０７：要件記述部１１０が、参照元５０６、５０８の記述に従い、入力情報の候補（入力候補）を取得する。
７０８：要件記述部１１０が種別５０７、５０９を取得し、ステップ７０７の入力候補から該当する入力候補のみを取得する。
７０９：ステップ７０８で取得した入力候補を一覧表示する。
７１０：表示した入力候補の一覧からユーザが選択した入力候補選択を入力部１０１が受け付け要件記述部１１０に送り、ステップ７０５に進む。
７１１：要件記述部１１０が、記述/変換ルールの変換ＩＤ５０１，及び、ステップ７１０で取得した入力候補（入力情報インスタンスと呼ぶ）を自然言語仕様格納ＤＢ１２１に要件インスタンスとして保管する。
７１２：終了
図３に示した例では、自然言語仕様３０１は、複数の設計書（モデリング情報３０２、データ要件関連情報３０３、ユースケース設計書３０４）から構成され、各設計書内の記載項目（データ要件一覧３０８など）が、形式言語仕様の各構成要素（不変条件３３４など）に対応する。
【００３３】
上記の処理は、自然言語仕様３０１の各記載項目内に記述する要件を個別に作成するための処理フローであり、例えば、データ要件一覧３０８を記載する場合には、対象５０２の欄が「データ要件」となっている記述/変換ルールを一覧表示し、アクション３１３を記載する場合には、対象５０２が「アクション」となっている記述/変換ルールを一覧表示し、変数３０７を記載する場合には、対象５０２が「変数」となっている記述/変換ルールを一覧表示する（ステップ７０２）。
【００３４】
そして、ユーザ選択を受け付け（ステップ７０３）、選択された記述/変換ルールを取得する。たとえば、図５の変換ＩＤ５０１がＴ１１の記述/変換ルールをユーザが選択した場合には、「ＡはＢを含む」という記述/変換ルールの入力情報“Ａ”，“Ｂ”に対し、入力情報インスタンスを生成するための処理（ステップ７０５からステップ７１０）を実行する。
【００３５】
ステップ７０６、ステップ７０７では、Ｔ１１の入力情報Ａに関する参照元情報と種別情報を参照し、入力情報Ａの入力候補を取得する。具体的には、Ｔ１１の入力情報Ａに関する参照情報は“Ｖ（変数一覧）”であるため変数一覧３０７から入力候補を取得する。そして、入力情報Ａに関する種別が“Ｅ（要素）”であるため、ステップ７０８では、取得した入力候補から要素として宣言された変数を取得する。そして、取得された変数を入力情報Ａの入力候補として一覧表示し、入力情報Ａのユーザ選択を受け付ける（ステップ７０９、７１０）。同様の処理（ステップ７０５からステップ７１０）を入力情報Ｂに対しても実施し、入力情報Ｂのユーザ選択を受け付ける。そして、ユーザが選択した入力情報Ａ及び入力情報Ｂから入力情報インスタンスを作成し、変換ＩＤ５０１と入力情報インスタンスから要件インスタンスを生成する。生成された要件インスタンスは、設計書作成部１０８により自然言語仕様格納ＤＢ１２１内に保管される（ステップ１２１）。
【００３６】
上記の処理フローでは、入力情報インスタンスを入力候補の中から選択する方法を示したが、集合一覧３０５、定数一覧３０６、変数一覧３０７、及び、パラメータ３１０は、システム内で用いる集合や定数、変数、或いは、ユースケース内で用いるパラメータを定義するための項目であるので、入力候補から受け付けるのではなく、ユーザからのテキスト入力を受付けるようにする。例えば、図５に示した変換ＩＤ５０１がＴ０１，Ｔ０２の記述/変換ルールは、変数への記述/変換テンプレートとなっている。このとき、自然言語表現５０３には、Ｔ０１の「Ｂの要素」のように、入力情報Ａの情報がない。また、入力情報５０５のＡに関して、参照元５０６、及び、種別５０７には“―”が記載されている。これは、入力情報Ａについては、ユーザからのテキストによる自由入力を受け付け、その結果を用いて変数を宣言することを表している。
【００３７】
また、Ｔ１１の自然言語表現「ＡはＢを含む」は、Ｔ１２の自然言語表現と同じになっている。この場合、ユーザがＴ１１、Ｔ１２を明示的に指名するのではなく、自然言語表現から記述/変換ルール候補を取得し、その後の入力情報インスタンスにおいて、ユーザから選択された入力情報インスタンスを基に変換ＩＤを特定するようにしてもよい。このようにすることによって、ユーザは形式言語表現を意識することなく、自然言語表現による仕様記述が可能となる。また、図５に示した記述/変換テンプレートでは、自然言語表現としてテキスト表現による記述/変換ルールを記述したが、例えば、自然言語表現としてＵＭＬのクラス図などを用いてもよい。
【００３８】
次に、図７の処理によって作成された要件インスタンスにより構成された自然言語仕様３０１から、形式言語仕様３２０を生成するための処理（図４ステップ４０７の処理）を説明する。
【００３９】
図３に示した如く、自然言語仕様３０１内のデータ要件一覧３０８等の各記載項目は、形式言語仕様３２０内の各構成要素に対応する。モデル変換部１０３の自然言語仕様３０１から形式言語仕様３２０への変換に当たっては、まず作成された各設計書（モデリング情報、データ要件関連情報、ユースケース設計書）の各記載項目から対応する形式言語仕様の各構成要素を生成し、各記載項目に記述された要件インスタンスを、形式言語表現に変換することによって、形式言語仕様３２０を生成する。
【００４０】
図８は、モデル変換部１０３における、上記の各記載項目内に格納された要件インスタンスから形式言語表現に変換するための処理フローを示している。
８０１：開始
８０２：モデル変換部１０３が自然言語仕様格納ＤＢ１２１から要件インスタンスを取得する。
８０３：モデル変換部１０３がステップ８０２で取得した要件インスタンスから、変換ＩＤを取得する。
８０４：ステップ８０２で取得した要件インスタンス内に入力情報インスタンスがまだある場合にはステップ８０５に、そうでない場合にはステップ８０６に進む。
８０５：モデル変換部１０３が要件インスタンス内の入力情報インスタンスを取得する。
８０６：モデル変換部１０３が記述/変換ルールＤＢ１２２から、ステップ８０３で取得した変換ＩＤと一致する変換ＩＤ５０１を有する記述/変換ルールを取得する。
８０７：モデル変換部１０３が、ステップ８０６で取得した変換ＩＤ５０１を有する記述/変換ルールの形式言語表現５０４にステップ８０５で取得した入力情報インスタンスを代入する。
８０８：終了
図７の要件インスタンスの処理フローで述べたとおり、各要件インスタンスは、変換ＩＤ、及び、入力情報インスタンスから構成される。また、図５に示した記述/変換ルールの構成により、変換ＩＤ５０１から対応する形式言語表現５０４が定まるため、入力情報の実体値（入情報インスタンス）が与えられれば、形式言語表現への変換が可能である。  従って、上記のステップ８０３による変換ＩＤの取得、及び、ステップ８０５における入力情報インスタンスの取得、さらにステップ８０６による形式言語表現の取得によって、各要件インスタンスの形式言語仕様内での記述への変換（ステップ８０７）が可能となる。  上記の変換処理を全ての要件インスタンスに対して実行することで、自然言語仕様３０１が形式言語仕様３２０に変換される。
【００４１】
図９は、要件補間部１０９による、要件補間ルール格納ＤＢ１２０を用いた不足要件生成の処理フローを示している（図４ステップ４０６の処理）
９０１：開始
９０２：要件補間部１０９が、自然言語仕様格納ＤＢ１２１から要件インスタンスを取得する。
９０３：要件補間部１０９が、要件補間ルールＤＢ１２０の要件補間ルールを探索し、ステップ９０２で取得した要件インスタンスと一致する変換ＩＤを有する基底要件６０３の要件補間ルールがあれば、ステップ９０４へ、なければステップ９０５に進む。
９０４：要件補間部１０９が、ステップ９０２で取得した要件インスタンス、及び、ステップ９０３で取得した変換ＩＤから基底要件６０３のインスタンスを作成する。
９０５：要件補間部１０９が、ステップ９０３で取得した要件補間ルールの従属要件６０４を取得する。
９０６：要件補間部１０９が、ステップ９０５で取得した従属要件の各々について、従属要件の有する変換ＩＤと一致する変換ＩＤを有する要件インスタンスがないか、自然言語仕様格納ＤＢ１２１内の要件インスタンスを探索する。全ての従属要件について、変換ＩＤが一致する要件インスタンスがあれば、ステップ９０７へ、なければステップ９１０に進む。
９０７：要件補間部１０９が、ステップ９０６で取得された要件インスタンスに対し、基底要件６０３のインスタンスを用いて、従属要件６０４のインスタンスの生成を試み、生成可能であればステップ９０８へ、そうでなければステップ９１０へ進む。
９０８：要件補間部１０９が、ステップ９０３で取得した要件補間ルールの不足要件５０５を取得する。
９０９：要件補間部１０９が、取得された不足要件６０５を用いて不足要件を生成する。
９１０：終了
ステップ９０２において取得された要件インスタンスに対し、ステップ９０３において要件補間ルールＤＢ１２０内から変換ＩＤが要件インスタンスと一致する基底要件６０３を探索する。基底要件６０３の要件に記述された変換ＩＤと要件インスタンスの変換ＩＤが一致する場合には、基底要件内のＸ，ＸＸ、Ｙ、…に要件インスタンスの入力情報インスタンスを代入し、基底要件６０３のインスタンスを作成する（ステップ９０４）。ここで、ＸはＸＸの部分集合であることを意味し、ＹはＹＹの部分集合であることを意味する。次に前記の基底要件６０３に対応する従属要件６０４を取得し（ステップ９０５）、従属要件６０４の対象６０８が一致する要件インスタンスを抽出し、抽出した要件インスタンスについて、従属要件６０４内に記載された変換ＩＤと一致する変換ＩＤを持つ要件インスタンスの有無を検索する（ステップ９０６）。全ての従属要件６０４について要件インスタンスがある場合には、従属要件のインスタンスの生成を試みる（ステップ９０７）。このとき、Ｘ，ＸＸ，…が基底要件にある場合には、基底要件と同じ入力情報インスタンスを用いる。ない場合には、ステップ９０６で取得した入力情報インスタンスを用いる。
【００４２】
上記の処理によって、従属要件６０４内のすべての要件について従属要件の要件インスタンスが生成できた場合には、不足要件６０５に記載された不足要件のインスタンスを生成し、設計書内の不足要件６０５の対象で指定された場所に不足要件を生成する。なお、不足要件にＡ’のように“シングルクォーテーション”がついている場合には、その入力情報を新たに生成することを表すものとする。
【００４３】
なお、上記により生成された不足要件は、設計書作成部１０８が自動で設計書への反映を行ってもよいし、不足要件候補として表示し、ユーザに反映の確認作業を行うようにしてもよい。また、前述のように設計書への自動反映を行う場合には、設計書への直接的な反映を行わず（設計書上には表示せず）、非表示要件として自然言語仕様格納ＤＢ１２１内に格納し、モデル変換部１０３内で形式言語仕様へ変換するようにしてもよい。このようにすることによって、形式言語仕様に精通していないユーザに、形式検証固有の冗長な表現を意識させることなく設計書の作成を支援することができ、設計書を見やすくすることができる。
【００４４】
上記の処理によって生成された不足要件が、ひとつでない場合には、例えば不足要件候補として一覧表示し、ユーザからの入力を受け付けることにより、不足要件を各設計書の該当箇所に反映するようにすればよい。また、複数の不足要件が表示される場合には、あらかじめ要件補間ルールＤＢ１２０ないに優先度欄を別途設け、優先度欄に応じて優先順位の高い要件から順に不足要件を表示するようにしてもよい。
【００４５】
以下、図１０から図１３を用いて、図７，８，９の処理について説明する。
【００４６】
図１０は、本実施例によって作成された設計書の一例を示している。図１０内のデータ要件関連情報１０００は、図３内のデータ要件関連情報３０３の一例であり、記述/変換ルールＤＢ１２２を用いて変数一覧１００１、及び、データ要件一覧１００２が記載されている。また、図１０内のユースケース設計書１０１０は、図３内のユースケース設計書３０４の一例であり、データ要件関連情報１０００と同様、記述/変換ルールＤＢ１２２を用いてユースケース名１０１１、パラメータ１０１３、事前条件１０１４、アクション１０１５が記載されている。さらに、ユースケース概要１０１２は、ユースケースの概要を説明する欄であり、形式言語仕様への変換が不要な自由記述欄である。
【００４７】
なお、図１０の検証結果欄１０２０は、形式言語仕様３２０に変換し、形式検証実行部１０５による仕様検証（証明責務の生成とその検証）を行った結果、モデル変換部１０３が、その結果を表示する欄である。図１０の場合、仕様検証の結果、「全ての登録帳票は帳票フォルダに割り当てられる」という要件を満たしていないことを意味する。
【００４８】
図１１は、図１０のデータ要件関連情報１０００、及び、ユースケース設計書１０１０の自然言語仕様格納ＤＢ１２１内でのデータ表現を部分的に表した例である。図１１に示したとおり、自然言語仕様格納ＤＢ１２１は、図１０に示した設計書をそのまま保管する必要はない。図１１の例では、自然言語仕様格納ＤＢ１２１は、ＸＭＬ（ｅＸｔｅｎｓｉｂｌｅ  Ｍａｒｋｕｐ  Ｌａｎｇｕａｇｅ）を用いて各設計書の情報を変換ＩＤと入力情報インスタンスから構成されている。
【００４９】
図１０のデータ要件関連情報１０００は、図１１のデータ要件関連情報要素１１０１から構成されるＸＭＬデータとして、変数一覧を表す変数一覧要素１１０３、データ要件一覧を表すデータ要件一覧要素１１０４を含み記述される。また、ユースケース設計書１０１０は、ユースケース設計書要素１１０２から構成されるＸＭＬデータとして、ユースケース名要素１１０５、パラメータ要素１１０７、事前条件要素１１０８、アクション要素１１０９から構成される。なお、補足情報要素１１０６は、形式言語仕様に変換する必要のない情報を記載する欄であり、図１１にはユースケースの概要を説明する概要要素（概要１０１２、ユースケース概要３１０に対応）を含む。
【００５０】
図１１の例では、各要件要素（１１２０〜１１２４）は、各要件インスタンスを表しており、変換ＩＤ（要件要素のＩＤ属性）と入力情報インスタンス（要件要素のＡ、Ｂ、…子要素）を含み構成される。変換ＩＤ、及び、入力情報インスタンスが自然言語仕様格納ＤＢ１２１内に格納されることにより、図８に示した処理フローにより、各要件インスタンスを形式言語表現に変換することが可能である。また、変換ＩＤ，及び、入力情報インスタンスから、図５に示した表を用いることによって、図１１の自然言語仕様格納ＤＢ１２１内の情報から、図１０に示した自然言語仕様を復元することができる。
【００５１】
例えば、要件要素１１２４は、その属性として“ｉｄ＝Ｔ４４” が格納されており、子要素Ａ，Ｂにそれぞれ、“新規帳票”、“登録済帳票”が格納されている。図５より、変換ＩＤが“Ｔ４４”の自然言語表現は、“ＡをＢに追加する”であり、子要素Ａ，Ｂの入力情報インスタンスより、要件インスタンスの自然言語表現が“新規帳票を登録済帳票に追加する”となることが分かる。同様にして、形式言語表現は“Ｂ：＝Ｂ∪｛Ａ｝”であることから、“登録済帳票：＝登録済帳票∪｛新規帳票｝”となることが分かる（変換結果は、後述する図１３の要件４  １３１１のａｃｔ１を参照）。
【００５２】
なお、図１０、図１１の例では、記述/変換ルールに基づき、各設計書を作成し、自然言語仕様格納ＤＢ１２１に格納した例を示した。図１０の設計書の作成に当たって、記述/変換ルールにない要件を記述できるようにしてもよい。この場合には、例えば、対応する形式言語表現も合わせて入力できるようにし、自然言語表現に対応する形式言語表現が分かるようにすることが望ましい。
【００５３】
また、図１１の自然言語仕様３２０では、自由記述に対して入力された自然言語表現、及び、形式言語表現を、自由記述を表す特殊な変換ＩＤ（例えば、Ｔ９９９９など）をあらかじめ定めておき、子要素として自然言語表現、及び、形式言語表現を記述するための要素を定義することによって、自由記述による自然言語表現、及び、形式言語表現を格納するようにすればよい。
【００５４】
なお、自由記述した要件に対して、必ずしも形式言語表現への変換が不要な要件（例えば補足情報など）は、子要素として形式言語表現を含める必要はない。
【００５５】
また、図１０の自然言語仕様３０１の表示に当たっては、例えば各要件の形式言語表現との対応が分かるよう、記述/変換ルール格納ＤＢ１２２を用いて変換後の形式言語表現をポップアップ表示する（自由記述の場合には、形式言語表現を記述するための要素を用いればよい）。また、対応する形式言語表現がない場合には、例えば文字や背景色を変更するなどして、対応する形式言語表現がないことを明示してもよい。
【００５６】
図１１では、自然言語仕様３０１の一実現例として、ＸＭＬによるデータ表現を用いたが、これと異なっていてもよい。また、ＸＭＬを用いた場合でも、要素名やＸＭＬの構造は、必ずしも図１１に示した限りでなくてもよい。
【００５７】
図１２は、図１０、図１１に示した自然言語仕様から、図６、及び、図９に示した要件補間ルール格納ＤＢ１２０を用いた不足要件の生成処理に基づき、不足要件を補間した結果を表している。図１２内の要件１、２が追加された不足要件を表している。要件１の生成は、図９の処理フローによって、以下により生成される。まず、ステップ９０２の処理によって、データ要件一覧の要件「全ての登録済み帳票は帳票フォルダに割当てられる。」について要件インスタンスを取得する。この要件インスタンスは、図１１の要件要素１１２１に示すように、要件ｉｄ（変換ＩＤ）がＴ１３である。次に、ステップ９０３の処理により、変換ＩＤがＴ１３である補間ＩＤ“Ａ１１”の要件補間ルールが取得され、要件インスタンスの入力情報インスタンス（Ａ＝登録済帳票、Ｂ＝帳票フォルダ）に基づき“Ｘ＝登録済帳票”、“Ｙ＝帳票フォルダ”を代入することにより、基底要件６０３のインスタンスが生成される（ステップ９０４）。さらに、ステップ９０５により、対応する従属要件６０４から要件が取得され、ステップ９０６、ステップ９０７の処理により、変換ＩＤがＴ０１である要件インスタンスを取得する。この場合、図１１の変数一覧要素１１２０が示すように、取得した要件インスタンスの入力情報インスタンスが“登録済帳票(帳票全体の部分集合)”、“帳票フォルダ(フォルダ全体の部分集合)”であるため、従属要件６０４では“Ｘ＝登録済帳票、ＸＸ＝帳票全体”、Ｙ＝帳票フォルダ“ＹＹ＝フォルダ全体”となり、従属要件６０４のインスタンスが生成可能である。以上の処理から、ステップ９０８、ステップ９０９によって、対応する不足要件の不足要件「Ｔ０２：ＢからＣへの関係」のインスタンス「登録済帳票to帳票フォルダ(登録済帳票から帳票フォルダへの関係)」が生成される。生成された要件は、対象欄と対応する設計書の該当箇所「変数一覧」に追加される（要件１  １２０１）。
【００５８】
要件２も同様にして、ユースケース設計書１０１０内のアクションに記載された要件、「新規帳票を登録済帳票に追加する。（変換ＩＤ：Ｔ４４）」「登録先フォルダを帳票フォルダに追加する。（変換ＩＤ：Ｔ４４）」から、補間ＩＤが“Ａ２３”となる基底要件が選択され（ステップ９０１〜ステップ９０４）、従属要件の検索、インスタンスの生成（ステップ９０５〜９０７）を通して、要件２  １２０２が生成される（ステップ９０８〜ステップ９１０）。
【００５９】
図１３は、図１２に示した設計書から、形式言語仕様（Ｅｖｅｎｔ−Ｂによる仕様記述）の生成結果を示した例である。設計書作成部１０８を用いてユーザが作成した各設計書は、自然言語格納ＤＢ１２１内に保管される。モデル変換部１０３によって、図８に示した処理フローにより、個々の要件が記述/変換ルールに基づき形式言語仕様に変換される（本実施例では、前述したとおり、個々の要件インスタンスは、変換ＩＤと入力情報インスタンスの情報を含み構成されるため、これの情報から形式言語表現への変換が可能である）。さらに、モデル変換部１０３は、形式言語表現に変換された各要件を、形式言語（本例では、Ｅｖｅｎｔ−Ｂ）の構文規則にのっとり、該当部分に記述する。これによって、ユーザが作成した自然言語仕様に対応する形式言語仕様が作成される。なお、図１３は、図５、図６に示した記述/変換ルール、及び、要件補間ルールの例に基づき生成された形式言語仕様の例を示しており、異なる記述/変換ルール、要件補間ルールを用いた場合には、必ずしも図１３のような形式言語仕様が生成されるとは限らない。
【００６０】
記述/変換ルール格納ＤＢ１２２内に格納する記述/変換ルールは、形式言語仕様に誤りなく変換でき、かつ、設計書内で検証したい性質に合わせて、適切な記述/変換ルールを格納することが望ましい。また、要件補間ルール格納ＤＢ１２０内に格納する要件補間ルールは記述/変換ルールに合わせて、形式言語仕様に変換された際に誤りのない仕様を作成するための、不足要件、あるいは、不足要件候補が生成されるように、適切な情報を格納することが望ましい。
【実施例２】
【００６１】
第一の実施例では、ユーザは、あらかじめ用意された記述/変換ルールを用いて、自然言語仕様により設計書の作成を行う。また、生成された設計書に対して不足要件の生成を行い、作成された設計書から形式言語仕様への変換を行う。これによって、形式検証技術に精通していないユーザが、形式検証技術に基づき、曖昧さや誤りのない設計書の作成を支援する方法を述べた。第二の実施例では、不足要件の導出を形式言語仕様上で行う方法を述べる。これによって、形式言語による仕様作成が可能なユーザに対しても、形式言語仕様作成の過程で忘れがちな要件や従属的に導かれる追加要件の記述支援を行う。これによって、直接形式言語仕様を作成する場合の支援を行う。
【００６２】
図１４は、第二の実施例における設計書作成支援装置１００の最小構成を示す図である。第二の実施例では、第一の実施例と異なり、形式言語仕様上で不足要件の生成を行う。そのため、自然言語仕様の作成にかかわる処理部（自然言語仕様作成部１０２、モデル変換部１０３）、及び、格納領域（自然言語仕様格納ＤＢ１２１、記述/変換ルール格納ＤＢ１２２）はなくてもよい。ただし、図１４の構成に、第一の実施例の構成を含めてもよい。この場合、不足要件の補間は形式言語仕様上で行うため、図１の要件補間部１０９、要件補間ルール格納ＤＢ１２０は、なくてもよい。
【００６３】
第二の実施例では、形式言語仕様上で不足要件の生成を行うため、形式言語仕様作成部１０４が形式仕様記述部１０４ａ、要件補間部１１２ａから構成される。ここで、形式言語仕様記述部１０４ａは、形式言語による仕様作成を直接行うための処理部であり、形式言語のための作成支援ソフトウェア（例えば、非特許文献１）を用いてよい。前述の通り、第二の実施例における要件補間部１１２ａは、ユーザにより作成された形式言語仕様から、要件補間ルール格納ＤＢ１２０ａ内に格納された要件補間ルールに基づき不足要件の生成を行う。
【００６４】
図１５は、第二の実施例における要件補間ルール格納ＤＢ１２０ａ内の構成を表す一例である。図１５に示したとおり、要件補間ルール格納ＤＢ１２０ａは、第一の実施例（図６）の構成と同様、補間ＩＤ６０１ａ、基底条件６０３ａ、前提条件６０４ａ、及び、従属条件６０５ａから構成される。ただし、第二の実施例における要件補間ルール格納ＤＢ１２０ａは、第一の実施例（図６）と異なり、基底要件６０３ａ、従属要件６０４ａ、不足要件６０５ａ内に格納される要件補間ルールは、形式言語表現が直接記述される。これは、第一の実施例では、自然言語仕様を形式言語仕様に変換し、自然言語仕様上で不足要件の生成を行っていたのに対し、第二の実施例では、形式言語仕様上で直接不足要件の補間を行うため、自然言語表現から形式言語表現への変換が必要ないためである。
【００６５】
不足要件の生成処理は、第一の実施例における不足要件の生成処理（図９）と同様にして生成することが可能である。ただし、第一の実施例と第二の実施例では、以下の点が異なる。前述のとおり、第一の実施例では、自然言語表現から形式言語表現への変換処理に基づき、不足要件の生成を行う。このため、第一の実施例では、記述/変換ルールの変換ＩＤを用いて、自然言語仕様から基底要件、従属要件の探索を行い、その結果から、記述/変換ルールに基づき、不足要件の生成を行う（生成される不足要件は、変換ＩＤと入力情報インスタンスによって表現される）。
【００６６】
一方、第二の実施例では、形式言語仕様上で不足要件の生成を行うため、その要件補間ルール格納ＤＢ１２０ａ内には、基底要件６０３ａ、従属要件６０４ａ、不足要件６０５ａには、形式言語表現で直接記載される。そのため、例えば、ステップ９０３、ステップ９０６における変換ＩＤによる要件インスタンスの検索は、形式表現上で記載された要件間の一致、不一致を検索する。また、その他、基底要件、従属要件等のインスタンスの生成は、形式言語表現でのインスタンスを直接生成する。
【００６７】
図１３に示した形式言語仕様において、要件３、要件４がユーザによって作成されていた場合には、図９の処理フローと図１５の要件補間ルール格納ＤＢ１２０ａを用いて、第一の実施例の要件２  １２０２（図１２）と同様、以下のように要件５が生成される。まず、要件補間部１１２ａによって、アクション内の要件４  １３１１と基底要件６０３ａから、補間ＩＤ６０１ａが“Ａ２３”の基底要件が選択され（ステップ９０２〜９０３）、“ＸＸ＝登録済帳票”、“Ｘ＝新規帳票”、“ＹＹ＝帳票フォルダ”、“Ｙ＝登録先フォルダ”として、基底要件のインスタンスが生成される（ステップ９０４）。次に、対応する従属要件を取得し（ステップ９０５）、従属用件に対応する要件として要件３  １３１０が存在し（ステップ９０６）、基底要件のインスタンスから従属要件の対応するインスタンスが生成される（ステップ９０７）。そして、対応する不足要件の要件補間ルールを取得し（ステップ９０８）、不足要件のインスタンスとして、「登録済帳票to帳票フォルダ:=登録済帳票to帳票フォルダ登録済帳票∪{新規帳票|->帳票フォルダ}」が生成される（ステップ９１０）。
【００６８】
なお、前述の通り、第二の実施例では、形式言語仕様上での直接要件の補間を行うため、図１４の構成図では、自然言語仕様の作成にかかわる処理部（自然言語仕様作成部１０２、モデル変換部１０３）、及び、格納領域（自然言語仕様格納ＤＢ１２１、記述/変換ルール格納ＤＢ１２２）は含まれていないが、これらを含む構成であってもよい。
【００６９】
この場合、第二の実施例に基づき生成された不足要件、あるいは、形式仕様記述部１０４ａによって作成された各要件は、記述/変換ルール格納ＤＢ１２２内の形式言語表現を元に、変換ＩＤ，及び、入力情報インスタンスを特定し、対応する自然言語表現に変換すればよい。
【００７０】
記述/変換ルール格納ＤＢ１２２に複数の形式言語表現が該当する場合には、記述/変換ルールＤＢ１２２内にあらかじめ優先度を設けておき、優先度に基づき、自然言語表現を決定する。あるいは、対応する複数の自然言語表現を（優先度に基づき）、一覧表示し、ユーザ選択により決定するようにしてもよい。また、記述/変換ルール格納ＤＢ１２２に該当する形式言語表現がない場合には、ユーザに対応する自然言語表現を直接記述させるようにしてもよい。
【００７１】
このような実施例の実現方法は、仕様作成支援装置１００を形式検証に精通していないユーザに設計書の基本部分を作成し、形式検証による検証、修正を形式検証の専門家が行う、などの利用の際に有用である。
【符号の説明】
【００７２】
１００  仕様作成支援装置
１０１  入力部
１０２  自然言語仕様作成部
１０３  モデル変換部
１０４  形式言語仕様作成部
１０５  形式検証実行部
１０６  表示部
１０７  入出力制御部
１０８  設計書作成部
１０９  要件補間部
１１０  要件記述部
１２０  要件補間ルール格納データベース
１２１  自然言語仕様格納データベース
１２２  記述/変換ルール格納データベース
１２３  形式仕様格納データベース
２００  電子計算機
２０１  ＣＰＵ
２０２  ＲＡＭ
２０３  表示装置
２０４  入力装置
２０５  インターフェイス
２１０  外部記憶装置
【図１】
0005634374.tif 000002
【図２】
0005634374.tif 000003
【図３】
0005634374.tif 000004
【図４】
0005634374.tif 000005
【図５】
0005634374.tif 000006
【図６】
0005634374.tif 000007
【図７】
0005634374.tif 000008
【図８】
0005634374.tif 000009
【図９】
0005634374.tif 000010
【図１０】
0005634374.tif 000011
【図１１】
0005634374.tif 000012
【図１２】
0005634374.tif 000013
【図１３】
0005634374.tif 000014
【図１４】
0005634374.tif 000015
【図１５】
0005634374.tif 000016