(57)【要約】      （修正有）【課題】用語の不統一や、暗黙知の不表出、および要件の曖昧さを排除することによる設計者の理解齟齬の抑制と、要件の矛盾や考慮漏れの発生を防止するための上位要件に対する下位要件の必要十分性の検証を可能とする、要求仕様の記述・検証システムを提供する。【解決手段】要件や暗黙知を示す要求関連事項について、要求関連事項の構成要素の各々を記号で表現するとともに構成要素の関係を数学記号で表現する方法により要求関連事項を入力する要件内容入力部１１１と、要件内容入力部１１１から入力された複数の要件関連事項の相互の関係を上位から下位に分解する形で設定し入力する要件構造入力部１１２と、要件内容入力部１１１に入力された要求関連事項と要件構造入力部１１２に入力された要求関連事項との関係を表示する要件表示部１０２を具備する。【選択図】図１
2016051234.tif 000002
【特許請求の範囲】
【請求項１】
要件や暗黙知を示す要求関連事項について、前記要求関連事項の構成要素の各々を記号で入力する要件内容入力部と、
前記要件内容入力部から入力された複数の前記要件関連事項の相互の関係を上位から下位に分解する形で設定し入力する要件構造入力部と、
前記要件内容入力部に入力された前記要求関連事項と前記要件構造入力部に入力された前記要求関連事項との関係を表示する要件表示部と、
を具備することを特徴とする要求仕様の記述・検証システム。
【請求項２】
要件や暗黙知を示す要求関連事項について、前記要求関連事項の構成要素の各々を記号で入力する要件内容入力部と、
前記要件内容入力部から入力された複数の前記要件関連事項の相互の関係を上位から下位に分解する形で設定し入力する要件構造入力部と、
前記要件内容入力部に入力された前記要求関連事項と、前記要件構造入力部に入力された前記要求関連事項との関係に基づく論理式を生成する論理生成部と、
前記論理生成部が生成した前記論理式の完全性を検証し判定結果を出力する論理検証部と、
前記論理検証部の前記論理式の検証結果を元に前記要件関連事項の論理構造の正誤を表示する検証結果表示部と、
を具備することを特徴とする要求仕様の記述・検証システム。
【請求項３】
請求項１又は２の何れかに記載の要求仕様の記述・検証システムであって、
ユーザ定義の記号や数学記号と同義の記号を管理する辞書データベースと、
前記辞書データベースを編集・更新するデータを入力する記号入力部とを備え、
前記要件入力部は、前記辞書データベースに登録された前記記号から選択される記号を入力として受け付けるか、又は、直接入力された前記記号のうち、前記辞書データベースに登録されていない記号の入力はエラーとすることにより、前記辞書データベースに登録された前記記号のみを入力として受け付けることを特徴とする、要求仕様の記述・検証システム。
【請求項４】
請求項１〜３の何れかに記載の要求仕様の記述・検証システムシステムであって、
前記要件関連事項の構成要素の少なくとも一部がパラメータで表現され、
前記要件関連事項の上位および下位の関係性をツリー形式のデータとして定めたテンプレートを入力するテンプレート入力部と、
前記テンプレートの前記パラメータの具体値を入力するパラメータ入力部と、
前記パターン入力部に入力された前記テンプレートと、前記パラメータ入力部に入力された前記パラメータの具体値とから要件関連事項のデータを生成する要件具体化部と、
を具備することを特徴とする要求仕様の記述・検証システム。
【請求項５】
請求項３に記載の要求仕様の記述・検証システムであって、
前記辞書データベースは、登録された前記記号に対応する自然言語を管理し、
前記辞書データベースの参照により、前記要件内容入力部に前記記号を用いて入力された前記要求関連事項を同義の自然言語表現へ変換する記号変換部を具備することを特徴とする要求仕様の記述・検証システム。
【請求項６】
請求項３に記載の要求仕様の記述・検証システムであって、
前記要件内容入力部は自然言語を用いた前記要求関連項目の入力を受け入れ可能であり、
前記辞書データベースは、登録された前記記号に対応する自然言語を管理し、
前記辞書データベースの参照により、前記要件内容入力部に自然言語を用いて入力された前記要求関連事項を同義の記号表現へ変換する自然言語変換部を具備することを特徴とする要求仕様の記述・検証システム。
【請求項７】
請求項１〜４の何れかに記載の要求仕様の記述・検証システムであって、
前記要件内容入力部は自然言語を用いた前記要求関連項目の入力を受け入れ可能であり、
前記要件内容入力部に自然言語を用いて入力された前記要求関連事項と、前記要件構造入力部に入力された前記要求関連事項の関係とから、要件定義書または要求仕様書を生成する要件出力部を備えることを特徴とする要求仕様の記述・検証システム。
【請求項８】
請求項１に記載の要求仕様の記述・検証システムであって、
前記要件内容入力部は、前記要求関連事項の各々に対して、暗黙知である旨の情報を付与可能であり、
前記要件表示部は、前記暗黙知である旨の情報を付与された前記要求関連事項に関して、表示有無又は表示方法を切り替えることを特徴とする要求仕様の記述・検証システム。
【請求項９】
請求項４に記載の要求仕様の記述・検証システムであって、
前記要件内容入力部は、前記要求関連事項の各々に対して、暗黙知である旨の情報を付与可能であり、
前記要件出力部は、前記暗黙知である旨の情報を付与された前記要求関連事項に関して、出力有無や出力方法を切り替えることを特徴とする要求仕様の記述・検証システム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、要求仕様、特に安全に関する要求仕様の記述・検証を行なうためのシステムに関する。
【背景技術】
【０００２】
近年大規模化・複雑化する情報制御システムの開発において、システムの高信頼・高安全化のために、システム設計者は、システムに求められる信頼性・安全性の水準を正しく認識し、正確な要件定義（要求仕様作成）を行う必要がある。
【０００３】
ＩＥＣ６１５０８やＩＳＯ２６２６２などの機能安全規格では、システムの安全性を示す根拠をアシュアランスケースやセーフティケースとして用意することが求められており、これらの中で安全に関する要件を正確に規定することが必要となる。
【０００４】
ある要件は一般に複数の要件に分解でき、それらは上位要件とその下位要件として構造化することが可能である。そして下位要件をもとにシステムの設計がなされる。
【０００５】
したがって要件定義書（要求仕様書）の記述の完全さを保証するために要件定義には、要件を曖昧さなく要件が設計者に正しく伝わるように記述すること、上位の要件や意図を理解し、認識誤りや考慮漏れなく下位要件に分解することが求められる。
【０００６】
例えばＩＳＯ２６２６２準拠の安全要件を作成する際には、まず安全目標を達成する機能安全要件（ＦＳＲ：Ｆｕｎｃｔｉｏｎａｌ  Ｓａｆｅｔｙ  Ｒｅｑｕｉｒｅｍｅｎｔｓ）を設定し、これを上位要件とし、これを満たすように下位要件である技術安全要件(ＴＳＲ：Ｔｅｃｈｎｉｃａｌ  Ｓａｆｅｔｙ  Ｒｅｑｕｉｒｅｍｅｎｔｓ)を設定する。さらに技術安全要件を上位要件とし、これを満たすように下位要件であるソウトウェア安全要件（ＳＳＲ：Ｓｏｆｔｗａｒｅ  Ｓａｆｅｔｙ  Ｒｅｑｕｉｒｅｍｅｎｔｓ）及びハードウェア安全要件（ＨＳＲ：Ｈａｒｄｗａｒｅ  Ｓａｆｅｔｙ  Ｒｅｑｕｉｒｅｍｅｎｔｓ）を設定する。
【０００７】
また、要件定義には、要件間に矛盾なく全ての要件が整合することが求められる。
なお上位要件を分解した下位要件群が上位要件を満たせば当然、下位要件間や、下位要件と上位要件の間に矛盾はない。
【０００８】
しかしながら実際の要件定義では、要件間の用語（単語、語彙）の不統一や、暗黙知の不表出、要件の表現が曖昧なこと等が原因で、下位要件が誤って定義されたり、設計者が要件を誤って解釈することがありうる。ここで暗黙知とは、要件の根拠となる知識のことであるとする。また要件間の矛盾や要件の考慮漏れが起こり得る。これには上位要件から下位要件への分解が不十分であったり適切でないことが要因としてある。これらの問題を完全に防止することは容易でない。
【０００９】
これらの課題に対し、用語の統一については特許文献１のように、類語や同義語を含む辞書データを利用する方法が考えられる。要件定義書の記述の曖昧さを排除する技術は特許文献２で提案されている。また、要件や要求仕様の矛盾や抜け不備の発見には、形式検証技術の活用が考えられる。例えば特許文献３では、コンピュータプログラムなど非同期に振舞う対象の仕様誤りを検出可能な、モデル検査技術が提案されている。
【００１０】
特許文献２には、要件定義書に対して抜けのない適格性試験仕様書の作成を可能とする仕様書作成支援装置が示されている。要件定義書の内容、事前条件、事後条件の記述の曖昧さを排除する手段として、それら記述を自然言語、論理演算子、数型演算子の組合せで記述することができるフォームが提供される。また特許文献２は、事前条件もしくは事後条件が要件に対して不成立になる場合をチェックリストとして出力する機能を提供し、このようなチェックリストにより、異常な値が入力された場合等における異常処理が要求仕様を満たすか否かの確認を容易にする。
【００１１】
特許文献３では、コンピュータプログラムおよび非同期に振舞う対象の仕様を表現する状態遷移表から、遷移列とその遷移条件を表現するツリー形式のデータを生成し、ツリーの所定の深さの階層に含まれる遷移列と遷移条件から論理式を生成し、検査器(ＳＡＴソルバ、ＳＡＴ；ｓａｔｉｓｆｉａｂｉｌｉｔｙ ｐｒｏｂｌｅｍ)で解くことにより、仕様の抜け漏れ・矛盾を検査する。
【先行技術文献】
【特許文献】
【００１２】
【特許文献１】特開２０１２−２３４２８２号公報
【特許文献２】特開２００８−１６５２７３号公報
【特許文献３】特開２０１２−１５５５１７号公報
【発明の概要】
【発明が解決しようとする課題】
【００１３】
しかしながら、特許文献２では、要件間の矛盾や、上位要件に対する下位要件の必要十分性を検証する手段を用意していない。また暗黙知を扱っていないので、前提としている暗黙知の表明や、暗黙知を前提とする要件の必要十分性を検証できない。
【００１４】
また特許文献３の検証手法は状態遷移を検証対象とするため、要件では記述される備えるべき機能やハード構成等の、状態遷移以外の対象を検査できない。暗黙知を含む検査や、上位要件に対する下位要件の必要十分性も検査できない。加えて特許文献３では有界モデル検査の形態を取ることから、階層数の指定次第では仕様に検査されない部分が残り、仕様の完全性が確認されない。
【００１５】
上述した技術的背景および従来技術の課題を鑑み、本発明では、高信頼・高安全な情報制御システムを構築する上で重要な要件定義において、従来課題であった用語の不統一、暗黙知の不表出、および要件の曖昧さを排除することによる設計者の理解祖語の抑制と、要件の矛盾や考慮漏れの発生を防止するための上位要件に対する下位要件の必要十分性の検証を可能とする、要求仕様の記述・検証システムの提供を目的とする。
【課題を解決するための手段】
【００１６】
上記課題を解決するために、本発明は、特許請求の範囲に記載の構成を採用する。即ち、本発明は、要件や暗黙知を示す要求関連事項について、前記要求関連事項の構成要素の各々を記号で表現するとともに構成要素の関係を数学記号で表現する方法により前記要求関連事項を入力する要件内容入力部と、前記要件内容入力部から入力された複数の前記要件関連事項の相互の関係を上位から下位に分解する形で設定し入力する要件構造入力部と、前記要件内容入力部に入力された前記要求関連事項と前記要件構造入力部に入力された前記要求関連事項との関係を表示する要件表示部とを具備する。
【００１７】
或いは、本発明は、要件や暗黙知を示す要求関連事項について、前記要求関連事項の構成要素の各々を記号で入力する要件内容入力部と、前記要件内容入力部から入力された複数の前記要件関連事項の相互の関係を上位から下位に分解する形で設定し入力する要件構造入力部と、前記要件内容入力部に入力された前記要求関連事項、および前記要件構造入力部に入力された前記要求関連事項間の関係に基づいて論理式を生成する論理生成部と、前記論理生成部が生成した前記論理式の成立性を検証し判定結果を出力する論理検証部と、前記論理検証部の前記論理式の検証結果を元に前記要件関連事項の論理構造の正誤を表示する検証結果表示部とを具備する。  
【発明の効果】
【００１８】
本発明によれば、高信頼・高安全な情報制御システムを構築する上で重要な要件定義において、要件関連事項を記号で表現することにより、用語の不統一、暗黙知の不表出、および要件の曖昧さを排除することによる設計者の理解齟齬の抑制が可能である。また本発明によれば、記号で表現された複数の要求関連事項の相互の関係を表示することにより、上位要件に対する下位要件の必要十分性の目視による確認が容易となる。加えて本発明によれば、複数の要求関連事項とそれらの関係から論理式を生成し検証に掛けることにより、要件関連事項の内容や要件関連事項間の関係に誤りがあれば検出できる。以上により、要件定義者は曖昧さ、矛盾や抜けのない要件の記述が可能となり、設計者は要件を正しく理解することができる。
【図面の簡単な説明】
【００１９】
【図１】要件記述検証プログラムの構成図
【図２】検証対象とするモータドライブシステムの構成図
【図３】記号定義表
【図４】要求関連事項一覧
【図５】要求関連事項モデル
【図６】自然言語で表現した要求関連事項モデル
【図７】テンプレート
【図８】テンプレートのパラメータ一覧
【図９】テンプレートから生成した要求関連事項モデル
【図１０】テンプレートから生成し自然言語で表現した要求関連事項モデル
【図１１】テンプレートから生成した要求関連事項一覧
【図１２】要件記述検証システムの構成図
【図１３】要件検証部の処理フロー
【発明を実施するための形態】
【００２０】
以下、本発明の実施例について図面を参照しながら説明する。各図において、共通な機能を有する構成要素には同一の番号を付与し、その説明を省略する。本実施例では「要件」と記載するとき、要求関連事項を示す場合がある。
【実施例１】
【００２１】
図１２は、本実施例を実現する要件記述検証システム１２００の構成図である。要件記述検証システム１２００は、ソフトウェアツールとして実現されている。各機能はソフトウェアとして実装されており、表示画面、主演算装置、主記憶装置（メインメモリ）、ハードディスク等の記憶媒体、キーボードやポインティングデバイス等の入力装置を備えるコンピュータ上で実行される。
【００２２】
要件記述検証システム１２００を実現するソフトウェアは、要件記述検証プログラム１００として、コンピュータ１２１０のＲＯＭ１２１３に格納されており、ＣＰＵ１２１１により読み出されて実行される。コンピュータ１２１０は、要件記述検証プログラム１００によって規定された処理を実行する。要求関連事項のデータファイルは、コンピュータ１２１０上のハードディスク１２１４に格納されている。要件記述検証プログラム１００に対するユーザ操作は、キーボードなどの入力装置１２３０から行うことができる。要件記述検証プログラム１００による出力は、ディスプレイなどの表示装置１２４０への表示や、ハードディスク１２１４へデータファイル生成としてなされるが、図示しない外部コンピュータへのネットワークを介した出力、ＣＤ−ＲＯＭなどの外部記憶媒体へのデータファイル形式での書き込みによる出力であってもよい。
【００２３】
図１は要件記述検証プログラム１００の基本構成図である。要件記述検証プログラム１００は、要件入力部１０１、要件表示部１０２、要件検証部１０３、検証結果表示部１０４、要件生成部１０５、記号入力部１０６、要件出力部１０７から構成される。
【００２４】
要件入力部１０１は、要件や暗黙知を示す要求関連事項を、要求関連事項の構成要素の各々を定義された記号で表現し、前記要求関連事項内の前記構成要素間の関係を数学記号または数学記号と同義に定義された記号で表現する方法で入力する機能を備えた要件内容入力部１１１と、要件内容入力部から入力された複数の要求関連事項の相互の関係を、上位から下位に分解する形で設定でき、さらに分解された下位の要求関連事項間の論理演算の関係を設定できる機能を備えた要件構造入力部１１２と、要件内容部１１１に入力された要求関連事項について、記号表現から自然言語表現への変換、またその逆の変換を実施する要件変換部１１３とからなる。
【００２５】
要求関連事項の構成要素は、ハードウェア、ソフトウェア、システム、データ、信号、機能、状態などの名詞、およびそれらの振る舞い（述語）である。
【００２６】
要件内容入力部１１１に入力された要求関連事項、および要件構造入力部１１２に入力された要求関連事項間の関係は、要件入力部１０１によりツリー形式のデータで表現される。以降ではこのデータを、要求関連事項モデルと呼ぶ。
【００２７】
要件変換部１１３は、記号入力部１０６の辞書データベースを参照して記号表現と自然言語表現の間の変換を行なう。
【００２８】
要件表示部１０２は、要件入力部１０１で生成された要求関連事項モデル、つまり要求関連事項自体と要求関連事項間の関係を表示する機能を備える。
【００２９】
要件検証部１０３は、要件入力部１０１が生成した要求関連事項モデル、すなわち要件内容入力部１１１に入力された要求関連事項、および要件構造入力部１１２に入力された要求関連事項間の関係から、論理式を生成する論理生成部１３１と、論理生成部１３１が生成した論理式を検証し判定結果を出力する論理検証部１３２とからなり、検証結果表示部１０４は論理式の検証結果を論理検証部１３２から受け取り、要件関連事項の論理構造の正誤を出力・表示する機能を備える。要件検証部１０３による検証は、形式検証の一種である。
【００３０】
要件生成部１０５は、構成要素の全てもしくは一部をパラメータとして表現した要件関連事項を１ないし複数、およびそれら要件関連事項間の関係を上位から下位に分解する形で定めたテンプレートを入力するテンプレート入力部１５１と、テンプレート入力部１５１に入力されたテンプレートに含まれるパラメータの具体値を入力可能なパラメータ入力部１５２と、テンプレート入力部１５１に入力されたテンプレート、およびパラメータ入力部１５２に入力された具体値から、テンプレートのパラメータを具体値に置換することにより要求関連事項モデルを生成する要件具体化部１５３とを備え、要件具体化部１５３により生成された要求関連事項モデルを、要件入力部１０１に出力する機能を備える。
【００３１】
記号入力部１０６は、ユーザ定義の記号や、数学記号または数学記号と同義に定義された記号、およびそれら記号に対応する自然言語を記録した辞書データベースを備えるとともに、記号入力部１０６は前記辞書データベースを編集・更新するサービスをユーザに提供する機能を備える。
【００３２】
記号入力部１０６の辞書データベースは要件入力部１０１、要件表示部１０２、パラメータ入力部１５２、論理検証部１３２、検証結果表示部１０４から参照可能となっている。
【００３３】
要件出力部１０７は、要求関連事項モデルの内容を所定のフォーマットに整形して、要件定義書（要求仕様書）の電子ファイルを作成し出力する。
【００３４】
以降、図２に示す異常検知・停止機能を備えたモータドライブシステム２００を対象とした要求仕様の記述を例に、本実施例の実現について具体的に説明する。
【００３５】
図２に示す異常検知・停止機能を備えたモータドライブシステム２００は、
マイコン２０１、プレドライバ２０２、インバータ２０３、モータ２０４、バッテリー２０５、リレー２０６、センサ２０７から構成される。
【００３６】
バッテリー２０５はリレー２０６を介して、インバータ２０３に対して直流電圧を供給する。プレドライバ２０２は、マイコン２０１からのPWM(Pulse Width Modulation)方式による制御信号を受け、インバータ２０３に対してPWM信号を出力し、インバータ２０３はプレドライバ２０２から受けたPWM信号を基に、インバータ２０３内部の半導体素子をスイッチングすることで、バッテリー２０５から供給された直流電圧を３相交流の電圧に変換し、これをモータ２０４に供給する。モータ２０４は、インバータ２０３から供給された電圧により駆動される。
【００３７】
モータドライブシステム２００の異常検知および停止機能は次の通りである。
【００３８】
マイコン２０１はセンサ２０７が検出したインバータ電圧を常時受け取り、事前に設定された閾値を超過することを異常判定条件としてインバータ電圧を常時監視し、異常判定条件成立時にはリレー２０６に対して遮断信号を出力する。
【００３９】
リレー２０６は、マイコン２０１から遮断信号を受けた場合、バッテリー２０５からインバータ２０３へ供給される直流電圧を遮断する。これによりモータドライブシステム２００は、インバータ電圧に異常が発生した際、インバータ２０３への電圧供給を停止しモータ２０４を停止させることで、モータ２０４の異常運転を防止することができる。
【００４０】
要件内容入力部１１１は、要件や暗黙知を示す要求関連事項を記号および自然言語で入力するサービスをユーザに提供する。
【００４１】
要件内容入力部１１１で入力する記号には、要求関連事項の構成要素を示す記号として、アルファベットなどの文字で構成された文字列を利用できる。それに加えて、論理記号である量化記号（「∀」や「∃」）、論理積「∧」、論理和「∨」、否定「¬」や論理包含「⇒」等を利用できる。またそれら論理記号と同義の記号表現を新たに定義して使用することができる。例えば「⇒」を「if」と定義し、要求関連事項「Ｘ⇒Ｙ」を、「Ｙ if Ｘ」と記述できる。なお「Ｘ」「Ｙ」は各々構成要素を示す記号である。ここで記号は自然言語より簡潔に表現されることが期待される。
【００４２】
本実施例では、要件内容入力部１１１は記号で入力された要求関連事項に対応した自然言語での表現を入力するサービスを提供する機能も備える。
【００４３】
異常検知・停止機能を備えたモータドライブシステム２００の要件を例に、要件内容入力部１１１に入力される具体的な内容を説明する。
【００４４】
モータドライブシステム２００の要求関連事項は以下とする。
（１） Motor shall stop if Inverter voltage error occurred. （インバータ電圧が異常のときに、モータ２０４が停止すること。）
（１）を以下のように分解する。
（２．１）Relay shall  open if Inverter voltage error occurs.（インバータ電圧が異常のときに、リレー２０６を開放すること。)
（２．２）Motor shall stop if Relay  opened. (リレー２０６が開放されると、モータ２０４が停止すること。)
なお本実施例では、（１）（２．１）を要件、（２．２）を暗黙知と位置付ける。
【００４５】
上記（１）（２．１）〜（２．２）の各々が自然言語で表現された要求関連事項である。また（１）が上位の要求関連事項であり、これを分解した（２．１）〜（２．２）が要求関連事項（１）に対する下位の要求関連事項である。要件内容入力部１１１には（１）（２．１）〜（２．２）を記号で表現したものも入力される。たとえば（１）を記号を用いて表現した例を以下に示す。
（１）InvErr.ocr ⇒ M.stop
以下ではこの記号表現を（１ｓ）とも示す。記号表現（１ｓ）において、「M」および「InvErr」は要求関連事項の構成要素であり、各々モータ２０４、インバータ２０３の電圧異常に対応した記号である。また本表現において、「M.stop」や「InvErr.ocr」も構成要素を示す記号であり、各々「Motor stops」および「Inverter voltage error occurs」を略記したものである。ただし自然言語表現においてはshallなどの助動詞が付いたり時制が変化したりする。
【００４６】
記号で要求関連事項を表現することにより、自然言語よりも表現が簡素化・短縮されるため、ユーザが要求関連事項を入力する手間が減り、また読むときに内容の把握がしやすい。
【００４７】
記号入力部１０６は、要件内容入力部１１１への入力に利用できる記号について図３に示すような記号定義表３００を用いて定義された記号と、記号に対応する自然言語表現を管理している。記号定義表３００は辞書データベースである。記号定義表３００はユーザが閲覧可能であるとともに、ユーザは記号定義表３００に対して例えば記号「M」を記号欄３０１に新規項目として追加し、自然言語表現欄３０２に「M」の自然言語表現「Motor」を入力できる。ユーザは記号欄３０１や自然言語表現欄３０２の内容を編集できる。
【００４８】
また記号入力部１０６は、ユーザが記号定義表３００の記号欄３０１に記号「M.stop」を追加するとき、記号定義表３００を参照し「M.stop」に含まれる「M」の自然言語表現を引用することで、「M.stop」の自然言語表現のデフォルト値を「Motor stops」とする機能を備えていてもよい。これは記号「M」を対応する自然言語「Motor」に置換し、「.」を空白に置換するルールを予め記号入力部１０６に設定しておくことで実現する。
【００４９】
記号入力部１０６において、予め記号「⇒」と同義の記号として記号「if」を定義した場合、要件内容入力部１１１に対しユーザは（１ｓ）を記号を用いた表現として
（１）M.stop if InvErr.ocr
と記述できる。以下ではこの記号表現を（１ｓ’）とも表す。このような定義によりユーザは要求関連項目の記号での入力をより簡易に行なうことができ、より理解しやすい表現ができる。
【００５０】
さらに、(２．１)を以下のように分解する。
（３．１）Inverter error shall be detected if Inverter voltage error occurs. (インバータ電圧が異常のとき、インバータ電圧異常は検出されること。)
（３．２）Stop signal shall be output if Inverter voltage error is detected by sensor. (インバータ電圧異常がセンサ２０７により検出されると、遮断信号が出力されること。)
（３．３）Stop signal is received by Relay if Stop signal is output. (遮断信号がマイコン２０１により出力されると、遮断信号は受信されること。)
（３．４）Relay opens if Stop signal is received by Relay. (遮断信号がリレー２０６によって受信されると、リレー２０６は開放されること。)
なお本実施例では、（３．３）（３．４）を暗黙知と位置付ける。
【００５１】
要件入力部１０１は、図４に示すような要求関連事項の一覧４００をユーザに表示し、要求内容入力部１１１はユーザに対して、記号表現欄４０４に要件関連事項を記号を用いて記入できるサービスを提供するとともに、記号表現欄４０４への入力に用いる記号を、記号定義表３００から選択できる機能を提供する。また要件内容入力部１１１は、自己ＩＤ欄４０１にて各要件関連事項の自己ＩＤを入力するサービスをユーザに提供する。
【００５２】
例えば要求関連事項（１）の場合、記号表現欄４０４において、ユーザは記号定義表３００から「M.stop」と「InvErr.ocr」を選択でき、予め定義された「if」も選択あるいは直接入力することで（１ｓ’）を記入することができる。またユーザは、要求関連事項（１）の自己ＩＤを自己ＩＤ欄４０１に「（１）」と記入できる。
【００５３】
要件内容入力部１１１には、記号定義表３００に定義された以外の記号を入力することもできるが、要件内容入力部１１１はユーザの指定時または１つの要求関連事項の入力完了時に、入力された要件関連事項に含まれる記号と、記号定義表３００で定義された記号とを照合し、入力された要件関連事項に含まれる記号が記号定義表３００で未定義である場合、検証結果表示部１０４に未定義記号とそれが書かれた要件を表示する。これにより、ユーザは未定義な記号で表現された要件、すなわち意味が不明瞭な要件の存在を知ることができる。
【００５４】
さらに要件内容入力部１１１は、入力された各要求関連事項に対して、ユーザが暗黙知である旨の情報を付与する機能を有する。例えば、要求関連事項（２．２）および（３．３）（３．４）について、図４の暗黙知欄４０５にチェックを入れることができる。
【００５５】
また要件内容入力部１１１は、記号を用いて表現された要件関連事項と同義の自然言語表現をユーザが入力できるサービスを提供する機能を備える。
【００５６】
例えば、要求関連事項の一覧４００の要件関連事項（１）の記号表現欄４０４に記載の「M.stop if InvErr.ocr」に対して、ユーザが「Motor shall stop if Inverter voltage error occurs」を自然言語表現欄４０３に入力できる。この自然言語表現は、記号表現の意味の説明を記号定義表３００のほかに補うと共に、最終的に利用される要件定義書で記載される内容にもなりうる。
【００５７】
要件内容入力部１１１は、記号を用いて表現された要件関連事項を、記号入力部１０６の記号定義表３００を参照することで対応する自然言語表現へ変換し要件表示部１０２に表示する機能を備えていてもよい。例えば、要求関連事項の一覧４００の要件関連事項（１）の記号表現欄４０４に記載の要件関連事項「M.stop if InvErr.ocr」は「Motor stops if Inverter voltage error occurs」に変換され、要件関連事項（１）の自然言語表現欄４０３に入力・表示される。この変換はユーザの指示により実施する。このように変換された自然言語表現にユーザが修正を加え、「Motor shall stop if Inverter voltage error occurred」とする。
【００５８】
このような記号表現から自然言語表現への変換を可能とすることで、要求関連事項の入力は記号により少ない労力で実施でき、また要件定義書で必要な自然言語表現のベースが用意されるため、自然言語表現の入力の手間も削減される。記号表現に対して後述の形式検証や目視による論理構造の確認が実施されている場合、要求関連事項に論理構造の誤りがないため、自然言語表現では助動詞などの修正が必要なほかには、誤りがない。
【００５９】
また逆に要件内容入力部１１１は、自然言語を用いて表現された要件関連事項を、記号入力部１０６の記号定義表３００を参照することで対応する記号表現へ変換し要件表示部１０２に表示する機能を備えていてもよい。例えば要求関連事項の一覧４００の要件関連事項（１）の自然言語表現欄４０３に「Motor shall stop if Inverter voltage error occurred」と入力されていたとき、形態素解析や論理記号（ｉｆ）での単語分割により、「Motor shall stop」と「Inverter voltage error occurred」を抽出し、それぞれ記号定義表３００の自然言語表現から類似の「Motor stops」と「Inverter voltage error occurs」を抽出し、それらに対応する記号「M.stop」と「InvErr.ocr」を抽出し、論理記号（ｉｆ）ともとの語順で接続して「M.stop if InvErr.ocr」として、要件関連事項（１）の記号表現欄４０４に入力・表示する。この変換はユーザの指示により実施する。このように変換された記号表現にユーザが修正を加えてもよい。
【００６０】
このような自然言語表現から記号表現への変換を可能とすることで、要求関連事項の内容や関係が明確に定まっていない段階においても、ユーザは自然言語で要求関連事項を記述し推敲していくことができ、後から記号表現に変換することで、ユーザは後述の形式検証や目視による論理構造の確認を実施することができる。
【００６１】
要件構造入力部１１２は、要件内容入力部１１１から入力された要求関連事項、例えば（１）（２．１）〜（２．２）（３．１）〜（３．４）の上位および下位の関係を設定するサービスをユーザに提供する。
【００６２】
上位および下位の関係の設定は、例えば図４記載の要求関連事項の一覧４００の自己ＩＤ４０１が付与された要件関連事項の各々に対して、上位に相当する要件関連事項の自己ＩＤを、上位ＩＤ欄４０２に記載することで実現される。
【００６３】
要件出力部１０７は要求関連事項の一覧４００の要求関連項目の自然言語表現や上位下位の関係を出力するが、その出力フォーマットは例えば要求関連事項の一覧４００から記号表現を除いたものが考えられる。
【００６４】
要件出力部１０７の出力時に、ユーザ指定に応じて暗黙知欄４０４にチェックが入れられた要求関連事項は出力しない、または備考表記とするなど出力方法を要件とは変更する、としてもよい。暗黙知には設計者には当然の内容である場合もあり、暗黙知を要件定義書から除外することで、要件定義書の記述量を減らして読みやすくすることができる。この場合、前提とされている暗黙知を把握するには、要求関連事項モデルを参照すればよい。ただし、要求関連項目の必要十分性を検証するには、暗黙知の記述は依然として必要である。
【００６５】
図５の要求関連事項モデル５００は、要求関連事項の一覧４００から要件入力部１０１が生成した要求関連事項モデルを要件表示部１０２が表示したものである。要求関連事項モデルのデータは要求関連事項モデル５００に自然言語表現の情報を加えたものになる。また要件構造入力部１１２で要求関連事項の内容や項目間の上位・下位の関係を入力する方法は、図５の形式のように視覚的に入力するものであってもよい。要件入力部１０１は、また図５のツリー形式で入力された要求関連事項モデルを、図４のテーブル形式での要求関連事項の一覧に変換可能とする。
【００６６】
要求関連事項モデル５００は要求関連事項が記号表現され、要求関連事項間の上位下位の関係はツリーで示されている。要求関連事項モデル５００では、下位要件間の関係はすべて論理積（ＡＮＤ）であるが、ＯＲを指定できるようにしてもよい。この場合、要求関連事項の一覧４００に、ＡＮＤ／ＯＲを入力する一列が必要となる。
【００６７】
ツリー形式での表示により、ユーザは要求関連事項間の上位から下位への分解の様子を把握できる。さらに要求関連事項が記号表現されていることにより、表現が簡素化・短縮され、かつ要求関連事項間での共通の構成要素を認識しやすくなる。このように、要件定義者が視覚的に検証するための手段が用意されているため、上位要件に対する下位要件の必要十分性の目視による確認での検証が容易になる。
【００６８】
要件出力部１０７から出力される要件定義書に含まれる要求関連項目の内容と関係は目視で確認済みとなるため、論理に誤りのない要件定義書を自動的に作成することができる。
【００６９】
例えば、上位要件（１）について（２．１）∧（２．２）⇒（１）を確認する場合、自然言語での表現の場合には、確認する内容は「Relay shall open if Inverter voltage error occurred」∧「Motor stops if Relay opened」⇒「Motor shall stop if Inverter voltage error occurred」となる。これに対し記号表現では「Rly.open if InvErr.ocr」∧「M.stop if Rly.open」⇒「M.stop if InvErr.ocr」となり簡素化・短縮される。記号Ａ，Ｂ，Ｃを用いると、上位要件（１）についての論理構造は（Ａ⇒Ｂ）∧（Ｂ⇒Ｃ）⇒（Ａ⇒Ｃ）になっている。ここでＡ：InvErr.ocr、Ｂ：Rly.open、Ｃ：M.stopに対応する。この論理構造の把握が記号表現では容易になる。これにより、ユーザの目視による要求関連事項の矛盾や考慮漏れも発見が容易になる。
【００７０】
要求関連事項モデル５００では、暗黙知に指定されている要求関連事項（２．２）（３．３）（３．４）と他項目とでは、要求関連事項を示すブロックの形状が異なっている。これによりユーザには、要求関連事項が要件か暗黙知かの判別が目視で容易に可能となる。要求関連事項の内容と関係をユーザが把握する上で、要求関連事項が要件か暗黙知かの判別は、要件とその導出根拠の関係を把握することであるため、重要である。暗黙知に指定されている要求関連事項を要件とは区別する表示方法としては、形状のほか、色や印しを利用してもよい。またユーザ指定により、暗黙知に指定されている要求関連事項を表示しないようにしてもよい。これは要件出力部１０７の出力と同様の理由による。
【００７１】
図６の要求関連事項モデル６００は、要求関連事項モデル５００を自然言語で要件表示部１０２が表示したものである。ユーザの指示により記号表現と自然言語表現とを切替できる。ユーザが自然言語表現で論理構造を確認したい場合に要求関連事項モデル６００の表示を利用できる。
【００７２】
以上により、要件や暗黙知を示す要求関連事項を、記号を用いた表現で、上位から下位に分解するツリー形式のデータとして表示することが可能となる。これにより用語の不統一や暗黙知の不表出による設計者の理解齟齬を抑制し、
要件定義者が上位要件と下位要件の関連性や下位要件の上位要件に対する必要十分性を確認することを容易にすることができる。
【００７３】
以下では、要件検証部１０３の詳細を説明する。図１３は、要件検証部１０３の処理フローを示している。要件検証部１０３はユーザ指定時またはユーザが１つの要求関連項目を入力完了したときに、図１３の処理フローをステップ１３００から開始する。なお図１３の処理フローは、要求関連事項モデルのツリーの最上位から下位に向けて全ての要件関連事項を対象に実施してもよいし、１つの要求関連項目を対象に実施してもよい。
【００７４】
論理生成部１３１は、ステップ１３１０において、要件入力部１０１が生成する要求関連事項モデル、例えば図５記載の要求関連事項モデル５００の、１つの要求関連項目とその下位にある要求関連項目の内容、および要求関連事項モデル５００に規定されたそれら要件関連項目間の関係性（論理積や論理和など）から論理式を生成する。論理式は、下位の要求関連事項間の関係が論理積のときには、下位の要求関連事項の論理積から上位の要求関連事項が導出されるように構成する。
【００７５】
要求関連事項（１）（２．１）〜（２．２）を例に挙げると、論理生成部１３１は、上位の要求関連事項である（１）を、（１）の下位の要求関連事項である（２．１）〜（２．２）の論理積から導出されるとして、以下のように論理式を構成する。
（２．１）∧（２．２）⇒（１）・・・・・・・・・・・・・・・・・・・・式１
式１の記号を用いた具体的な表現は、次の通りである。
(Rly.open if InvErr.ocr)∧(M.stop if Rly.open) →(M.stop if InvErr.ocr)
本論理式の第１項および第２項は、第３項を分解したものである。本論理式の成立性は演繹法にて確認できる。上記の例は、論理が成立する場合である。
【００７６】
論理検証部１３２はステップ１３２０において、論理生成部１３１が生成した論理式を検証器（ＳＡＴソルバ）が検証可能な形に変換し、ステップ１３３０において検証器を用いて論理生成部１３１が生成した論理式の完全性を判定する。また論理検証部１３２はステップ１３４０において、ステップ１３００の判定結果を検証結果表示部１０４に出力する。判定結果はファイルに出力してもよい。最後にステップ１３９０にて処理を終了する。
【００７７】
ステップ１３２０における論理式の変換は、論理生成部１３１が生成した論理式の否定形を、論理式の前提条件を踏まえてＣＮＦ(Ｃｏｎｊｕｎｃｔｉｖｅ  Ｎｏｒｍａｌ  Ｆｏｒｍ)へと変換するものである。この式をＳＡＴソルバで解き、解なし（ＵＮＳＡＴ）となることが確認できれば、検証対象とする要求関連項目に対する下位の要求関連項目の必要十分性が検証される。例えばブール型変数Ａ，Ｂ，Ｃを用いてＡ：InvErr.ocr，Ｂ：Rly.open、Ｃ：M.stopと定義した場合、式１の前件(Ａ⇒Ｂ)∧（Ｂ⇒Ｃ）が常に成立することを前提条件とし、式１の否定形の成立性を評価する。すなわちステップ１３２０では、式１から以下に示す式２のようなＣＮＦへの変換が行われ、これをＳＡＴソルバで解くことにより式１の完全性が評価される。
式１の否定形∧式１の前件
≡｛(Ａ⇒Ｂ)∧（Ｂ⇒Ｃ）⇒¬（Ａ⇒Ｃ）} ∧(Ａ⇒Ｂ)∧(Ｂ⇒Ｃ)
＝｛¬（（¬Ａ∨Ｂ）∧（¬Ｂ∨Ｃ））∨¬（¬Ａ∨Ｃ）}
∧(¬Ａ∨Ｂ)∧(¬Ｂ∨Ｃ)
＝｛（¬（¬Ａ∨Ｂ）∨¬（¬Ｂ∨Ｃ））∨（Ａ∧¬Ｃ）}
∧(¬Ａ∨Ｂ)∧(¬Ｂ∨Ｃ)
＝｛（Ａ∧¬Ｂ）∨（Ｂ∧¬Ｃ）∨（Ａ∧¬Ｃ）｝∧(¬Ａ∨Ｂ)∧(¬Ｂ∨Ｃ)
＝（Ａ∨Ｂ）∧（Ａ∨¬Ｃ）∧（¬Ｂ∨¬Ｃ）∧(¬Ａ∨Ｂ)∧(¬Ｂ∨Ｃ)
・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・・式２
式２は、ＳＡＴソルバにより充足しないと判定される。これにより論理検証部１３２において式１の完全性が確認される。
【００７８】
同様に要求関連事項モデル５００の他の部分についても検証され、論理に誤りがなければ、検証結果表示部１０４は要求関連事項モデル５００、または要求ツリー６００、または要求関連項目の一覧４００に誤りがないことを表示する。
【００７９】
本例において、仮に暗黙知である（２．２）が要求関連事項の一覧４００から欠落していた場合、要求関連事項（１）（２．１）の論理式はステップ１３２０にて以下の式１’から式２’となる。
（２．１）⇒（１）・・・・・・・・・・・・・・・・・・・・・・・・・・式１’
式１’の否定形∧式１’の前件
≡｛(Ａ⇒Ｂ)⇒¬（Ａ⇒Ｃ）}∧(Ａ⇒Ｂ)
＝｛¬（¬Ａ∨Ｂ）∨¬（¬Ａ∨Ｃ）}∧(¬Ａ∨Ｂ)
＝｛（Ａ∧¬Ｂ）∨（Ａ∧¬Ｃ）}∧（¬Ａ∨Ｂ）
＝｛（Ａ∨（Ａ∧Ｃ））∧（¬Ｂ∨（Ａ∧¬Ｃ））}∧（¬Ａ∨Ｂ）
＝Ａ∧（Ａ∨Ｃ）∧（Ａ∨¬Ｂ）∧（¬Ｂ∨¬Ｃ）∧（¬Ａ∨Ｂ）・・・・・式２’
式２’はＳＡＴソルバにより充足すると判定される。解はＡ＝１，Ｂ＝１，Ｃ＝０である。これにより論理検証部１３２において式１’が完全でないことが確認される。検証結果表示部１０４は要求関連事項モデル５００、または要求ツリー６００、または要求関連項目の一覧４００において、要求関連事項（１）（２．１）の論理に誤りがあることを表示する。この表示は要求ツリーや一覧と重ね合わせても、別表示でもよい。重ね合わせて表示する場合、例えば要求ツリー５００の要求関連事項（１）のブロックにエラーを示す「×」を表示する。ユーザはこの検証結果を検証結果表示部１０４で確認し、要求関連事項（２．２）の抜けに気付くことができる。
【００８０】
また、仮に要求関連事項（２．１）が以下のように間違いを含んでユーザにより定義された場合について説明する。
（２．１’）Relay shall close if Inverter voltage error occurred.（インバータ電圧が異常なときに、リレー２０６を閉鎖すること。)
自然言語表現「Relay closes」の記号表現をRelay.closeとし、ブール型変数Ｄを用いて、Ｄ：Relay.close とすると、関連事項（１）（２．１’）（２．２）の論理式はステップ１３２０にて以下の式１’’から式２’’となる。
【００８１】
（２．１’）∧（２．２）⇒（１）・・・・・・・・・・・・・・・・式１’’
式１’’の否定形∧式１’’の前件
≡｛(Ｄ⇒Ｂ)∧（Ｂ⇒Ｃ）⇒（Ａ⇒Ｃ）｝∧(Ｄ⇒Ｂ)∧（Ｂ⇒Ｃ）
＝｛¬（（¬Ｄ∨Ｂ）∧（¬Ｂ∨Ｃ））∨（¬Ａ∨Ｃ）｝
∧(¬Ｄ∨Ｂ)∧（¬Ｂ∨Ｃ）
＝（Ａ∨Ｂ∨Ｄ）∧（Ａ∨Ｂ∨¬Ｃ）∧（Ａ∨¬Ｃ）∧（¬Ｂ∨¬Ｃ）
∧(¬Ｄ∨Ｂ)∧（¬Ｂ∨Ｃ）・・・・・・・・・・・・・・・・・式２’’
式２’’はＳＡＴソルバにより充足すると判定される。例えば解は、Ａ＝１，Ｂ＝０，Ｃ＝１，Ｄ＝０である。つまり要求関連事項（１）（２．１’）（２．２）には論理の誤りが存在する。ユーザはこの検証結果を検証結果表示部１０４で確認し、(２．１’)の誤りに気付くことができる。
【００８２】
もし「Relay closes」の記号表現を「¬Relay.open」で定義したときには、やはり論理の完全性が示されず、検証結果表示部１０４で示される検証結果から、ユーザは要求関連事項（１）（２．１’）（２．２）には論理の矛盾が存在することを確認することができる。
【００８３】
このように本実施例によれば、要求関連事項の誤りや矛盾、抜けを確実に自動で検出できる手段が用意されているため、ユーザは要求関連事項に誤り、矛盾および抜けのない要件定義が可能となる。検証対象とする要求関連事項には要件のほか暗黙知も含まれるので、要件の前提としている暗黙知が正しいか、暗黙知を前提とした要件が正しいかも検証される。
【００８４】
また、要件検証部１０３の検証方法は、検証対象を１つの要求関連事項とその下位の要求関連事項のみとし、要求関連事項モデル全体を対象とするものではないため、検証に要する処理時間やメモリなどのリソースが小さく、要求関連事項モデルが大きくなっても検証が可能であるという特徴がある。
【００８５】
要件出力部１０７から出力される要件定義書に含まれる要求関連項目の内容と関係は、要件検証部１０３により検証済みとなるため、論理に誤りのない要件定義書を自動的に作成することができる。
【００８６】
以下では要件生成部１０５の詳細を説明する。
【００８７】
要件生成部１０５は要求関連事項モデルのテンプレート（以下では単にテンプレートと呼ぶ）として、要件関連事項の構成要素の全て、もしくは一部をパラメータの形で持つ、記号表現された要求関連事項モデルを複数記憶している。ユーザは要件生成部１０５に新たなテンプレートを登録して記憶させることができる。テンプレートの一例を図７に示す。図７のテンプレート７００は、「条件Cが成立したら条件Tcも成立すること」という上位要件７０１を下位要件７０２〜７０４に分解したモデルとなっている。下位要件７０２は「条件Cが成立したらメッセージMsgが（機能１により）送信されること」、下位要件７０３は「メッセージMsgが（機能１により）送信されたら、Msgは（機能２により）受信される」、下位要件７０４は「メッセージMsgが（機能２により）受信されたら、条件Tcを成立させること」を示している。なお下位要件７０３は暗黙知に指定されている。テンプレート７００のTc、C、およびMsgがパラメータである。
【００８８】
テンプレート入力部１５１は、要件生成部１０５に記憶されたテンプレートをユーザに選択式に提示しユーザの選択を受け付けるか、またはテンプレートのデータファイル入力を受け付ける。これにより１つのテンプレートがテンプレート入力部１５１に入力される。
【００８９】
パラメータ入力部１５２は、テンプレート入力部１５１に入力されたテンプレート７００が有するパラメータについて、図８に示すパラメータ一覧８００をユーザに提示する。ユーザは入力欄８０１にパラメータに対する具体値を入力することができる。記号表現欄８０３には記号を用いた表現、自然言語表現欄８０２には自然言語表現が入力される。記号表現欄８０３、自然言語表現欄８０２ともに、記号定義表３００に定義された記号や自然言語表現から選択式に入力することも可能とする。
【００９０】
テンプレート７００のパラメータ、記号定義表３００の記号ともに型情報（例：ハードウェア、データ、状態など）が付与されている場合には、
パラメータ入力部１５２は、記号表現欄８０３に入力可能な記号を、記号定義表３００に定義され、かつパラメータと型が一致する記号に制限してもよい。
【００９１】
テンプレート７００にはTc, C, Msgのほかに記号として、Msg.sentとMsg.receivedが用いられている。これらの記号の意味は、記号テーブル８１０に記載されており、それぞれ「メッセージMsgが（機能１により)送信されること」「メッセージMsgが（機能２により）受信されること」である。記号テーブル８１０は、パラメータ入力部１５２により表示される。機能１、機能２は予め具体値にしておいてもよいし、別のパラメータにしてもよい。
【００９２】
要件具体化部１５３はテンプレート入力部に入力されたテンプレートのパラメータを、パラメータ入力部１５２に入力された具体値に置換して、パラメータのない要求関連事項モデルを生成し、要件入力部１０１に入力する。
【００９３】
テンプレート７００については、パラメータTc, C, Msgが具体値に置換されるほか、Msg.sentとMsg.receivedのMsgも、Msgの具体値で置換される。
【００９４】
例えば、ユーザが記号表現欄８０３に具体値としてTcは「Alm.on」、Cは「Temp.high」、Msgは「AlmSig」と入力した場合、要件具体化部１５３によってテンプレート７００から図９の記号表現された要求関連事項モデル９００が生成される。要求関連事項モデルは要件入力部１０１に入力され、要件表示部１０２に表示される。具体値の記号に対応する自然言語表現は、自然言語表現欄８０２に入力されており、Alm.onは「Alarm is turned on」、Temp.highは「Temperature is too high」、Msgは「Alarm Signal」とされている。自然言語表現欄８０３の情報は要求関連事項モデル９００に付与されており、要件表示部１０２は図１０に示される要求関連事項モデル９００を自然言語表現した要求関連事項モデル１０００を表示する。なお要求関連事項モデル１０００はユーザにより助動詞などが追加・修正されている。
【００９５】
パラメータ入力部１５２での具体値の入力方法は、図７のツリー形式での表示上であってもよい。この場合例えば、パラメータTc, C, Msgの部分に具体値の入力欄を設ける。
【００９６】
要件入力部１０１は、要件具体化部１５３が出力した要求関連事項モデル９００の情報を元に、図４の要求関連事項の一覧４００と同様のテーブルである、要求関連事項の一覧１１００を表示する。
【００９７】
なお要件生成部１０５が記憶し提供するテンプレートは、テンプレートに含まれるパラメータの具体値によらず、テンプレートに含まれる下位要件が上位要件に対し必要十分であることが既に保証されたものとするのがよい。
【００９８】
例えば図７に示したテンプレート７００は、パラメータの具体値によらず、下位要件は上位要件に対し必要十分である。
【００９９】
論理に誤りのないテンプレートから生成した要求関連事項モデルには論理の誤りがない。ただし、例えばパラメータＡ，Ｂ，Ｃで表現されるテンプレートＡ∧Ｂ⇒ＣのＡとＢに、具体値としてaと¬aを入力すると、論理の矛盾が発生する。このような矛盾の発生有無は、要件入力部１０１が要求関連事項モデルを要件具体化部１５３から受け取った際に、要件検証部１０３を用いて検出すればよい。また、テンプレート入力部１５１がテンプレートの登録または入力を受け付ける際に、要件検証部１０３を用いて論理の検証を行なってもよい。この場合、テンプレート入力部１５１は論理の誤りが検出されたテンプレートを受け付けない。
【０１００】
論理に誤りがないことを検証済みの要求関連事項モデルの一部または全部の構成要素をパラメータ化してテンプレートを作成すると、論理に誤りのないテンプレートを用意することができる。要件入力部１０１は、入力されている要求関連事項モデルの任意の構成要素を、ユーザ指定に応じてパラメータに置換し、テンプレートを生成して、要件生成部１０５に登録する機能を有してもよい。具体的なユーザ操作として、要求関連事項の一覧４００や、要求関連事項モデル５００の表示上で、パラメータ化する構成要素をユーザが指定すると、パラメータ一覧８００と同様のテーブルが生成され、ユーザはパラメータの記号とその意味を入力する。この操作により、テンプレートのデータが生成される。テンプレート化できる要求関連事項モデルは、要件検証部１０３により誤りがないことを検証済のものに限定してもよい。
【０１０１】
本実施例の要件生成部１０５によれば、テンプレートを活用することで、上位要件に対し下位要件を矛盾や抜けなく記述する作業を、パラメータの指定により実施できるので、作業の簡略化が可能である。また要件生成部１０５にテンプレートが登録されていれば、要件を定義する対象に応じたテンプレートの選択により、要件記述をさらに効率的に行うことができる。
【０１０２】
要件出力部１０７から出力される要件定義書に含まれる要求関連項目の内容と関係もテンプレートから生成されたものとなるため、論理に誤りのない要件定義書を自動的に作成することができる。
【０１０３】
テンプレートは要求関連事項モデルをパターン化したものである。特に安全関連の機能は、監視・異常検出・異常処理のようにパターン化できる部分が多いため、検証された要求関連事項モデルのテンプレート化は有効である。
【０１０４】
以上のように、本実施例に係る記述・検証システムによれば、要件や暗黙知を示す要求関連事項を、定義された記号で表現することで用語が統一され、自然言語のような曖昧さがなく、また前提とする暗黙知も表明されるため、設計者の理解齟齬が抑制される。
さらに要求関連事項間の関係を上位から下位に分解する形で定義し、複数の要求関連事項とそれらの関係を表示することで、上位要件に対する下位要件の必要十分性を容易に目視で確認することができる。また複数の要求関連事項とそれらの関係から論理式を生成し検証に掛けることで、要件関連事項の内容や要件関連事項間の関係に誤りがあれば検出することができる。以上により、要件定義者は曖昧さ、矛盾や抜けや考慮漏れのない要件の記述が可能となり、設計者は要件を正しく理解することができる。
【符号の説明】
【０１０５】
１００： 要件記述検証プログラムの構成図
１０１： 要件入力部
１０２： 要件表示部
１０３： 要件検証部
１０４： 検証結果表示部
１０５： 要件生成部
１０６： 記号入力部
１０７： 要件出力部
１１１： 要件内容入力部
１１２： 要件構造入力部
１３１： 論理生成部
１３２： 論理検証部
１５１： テンプレート入力部
１５２： パラメータ入力部
１５３： 要件具体化部
２００： 異常検知・停止機能を備えたモータドライブシステム
５００： 要求関連事項モデル
７００： テンプレート
【図１】
2016051234.tif 000003
【図２】
2016051234.tif 000004
【図３】
2016051234.tif 000005
【図４】
2016051234.tif 000006
【図５】
2016051234.tif 000007
【図６】
2016051234.tif 000008
【図７】
2016051234.tif 000009
【図８】
2016051234.tif 000010
【図９】
2016051234.tif 000011
【図１０】
2016051234.tif 000012
【図１１】
2016051234.tif 000013
【図１２】
2016051234.tif 000014
【図１３】
2016051234.tif 000015