(57)【要約】【課題】テスト項目の網羅性および品質の向上を図ること。【解決手段】検証対象のユースケース図１０１からユースケース（たとえば、ユースケース１）を選択するとともに、検証対象の仕様をあらわす有限状態機械モデル群１０２から当該ユースケース１に対応する有限状態機械モデル９００を選択する。選択された有限状態機械モデル９００をＫｒｉｐｋｅモデル１０３に変換する。Ｋｒｉｐｋｅモデル１０３からＫｒｉｐｋｅプロパティを生成する。Ｋｒｉｐｋｅプロパティが求まれば、Ｋｒｉｐｋｅプロパティを公知の形式検証ツールに与えるだけで、ユースケースの状態カバレッジ（ＵＣＳＣ）用Ｔｒａｐプロパティ１０５とユースケースの遷移カバレッジ（ＵＣＴＣ）用Ｔｒａｐプロパティ１０６を得ることができる。【選択図】図１
2010009384.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータを、
検証対象に関するユースケース図の中から任意のユースケースを選択する選択手段、
前記選択手段によって選択されたユースケース（以下、「選択ユースケース」という）の事前条件および事後条件を抽出する抽出手段、
前記選択ユースケースに対応する有限状態機械モデルをＫｒｉｐｋｅモデルに変換する変換手段、
前記抽出手段によって抽出された事前条件および事後条件に基づいて、前記変換手段によって変換されたＫｒｉｐｋｅモデルのＫｒｉｐｋｅ初期状態、Ｋｒｉｐｋｅ事前条件およびＫｒｉｐｋｅ事後条件を特定する特定手段、
前記特定手段によって特定されたＫｒｉｐｋｅ事前条件およびＫｒｉｐｋｅ事後条件に基づいて、前記選択ユースケースのＫｒｉｐｋｅプロパティを生成する生成手段、
として機能させることを特徴とする検証支援プログラム。
【請求項２】
前記生成手段は、
前記Ｋｒｉｐｋｅ事前条件から前記Ｋｒｉｐｋｅ事後条件までの全状態を通す前記選択ユースケースのＫｒｉｐｋｅプロパティを生成することを特徴とする請求項１に記載の検証支援プログラム。
【請求項３】
前記生成手段は、
前記Ｋｒｉｐｋｅ事前条件から前記Ｋｒｉｐｋｅ事後条件までの全遷移を通す前記選択ユースケースのＫｒｉｐｋｅプロパティを生成することを特徴とする請求項１または２に記載の検証支援プログラム。
【請求項４】
前記生成手段は、
前記Ｋｒｉｐｋｅプロパティを形式検証ツールに与えることにより、前記Ｋｒｉｐｋｅプロパティに関するＴｒａｐプロパティを生成することを特徴とする請求項１〜３のいずれか一つに記載の検証支援プログラム。
【請求項５】
検証対象に関するユースケース図の中から任意のユースケースを選択する選択手段と、
前記選択手段によって選択されたユースケース（以下、「選択ユースケース」という）の事前条件および事後条件を抽出する抽出手段と、
前記選択ユースケースに対応する有限状態機械モデルをＫｒｉｐｋｅモデルに変換する変換手段と、
前記抽出手段によって抽出された事前条件および事後条件に基づいて、前記変換手段によって変換されたＫｒｉｐｋｅモデルのＫｒｉｐｋｅ初期状態、Ｋｒｉｐｋｅ事前条件およびＫｒｉｐｋｅ事後条件を特定する特定手段と、
前記特定手段によって特定されたＫｒｉｐｋｅ事前条件およびＫｒｉｐｋｅ事後条件に基づいて、前記選択ユースケースのＫｒｉｐｋｅプロパティを生成する生成手段と、
を備えることを特徴とする検証支援装置。
【請求項６】
コンピュータが、
検証対象に関するユースケース図の中から任意のユースケースを選択する選択工程と、
前記選択工程によって選択されたユースケース（以下、「選択ユースケース」という）の事前条件および事後条件を抽出する抽出工程と、
前記選択ユースケースに対応する有限状態機械モデルをＫｒｉｐｋｅモデルに変換する変換工程と、
前記抽出工程によって抽出された事前条件および事後条件に基づいて、前記変換工程によって変換されたＫｒｉｐｋｅモデルのＫｒｉｐｋｅ初期状態、Ｋｒｉｐｋｅ事前条件およびＫｒｉｐｋｅ事後条件を特定する特定工程と、
前記特定工程によって特定されたＫｒｉｐｋｅ事前条件およびＫｒｉｐｋｅ事後条件に基づいて、前記選択ユースケースのＫｒｉｐｋｅプロパティを生成する生成工程と、
を実行することを特徴とする検証支援方法。
【発明の詳細な説明】
【技術分野】
【０００１】
この発明は、ＬＳＩ（Ｌａｒｇｅ  Ｓｃａｌｅ  Ｉｎｔｅｇｒａｔｉｏｎ）の形式的な仕様からテスト項目を自動生成する（ＳＢＴ（Ｓｐｅｃｉｆｉｃａｔｉｏｎ  Ｂａｓｅｄ  Ｔｅｓｔ）技術）ための検証支援プログラム、検証支援装置、および検証支援方法に関する。
【背景技術】
【０００２】
ＬＳＩ設計では、従来から設計期間の短縮による作業効率化が要求されている一方、ＬＳＩが正しく動作するかどうかを検証する検証作業が必要不可欠であり、特に、大規模化、高機能化、高速化および低消費電力化が要求されているＬＳＩについては、高品質を維持するためにもこの検証作業は重要である。
【０００３】
このような検証作業をおこなうための検証ツールには、機能仕様からテスト項目を自動生成するもの（たとえば、下記特許文献１を参照。）や、テストタイミングデータを自動生成するもの（たとえば、下記特許文献２を参照。）や、要求仕様を示すテスト仕様から検証プログラムを直接生成するもの（たとえば、下記特許文献３を参照。）や、代表的な操作パターンから試験項目を生成するもの（たとえば、下記特許文献４を参照。）がある。
【０００４】
上記検証ツールのほか、検証作業では、ＳＢＴ技術が用いられる。ＳＢＴ技術とは、形式的な仕様からテスト項目を生成する技術である。具体的には、検証対象の仕様をあらわす有限状態機械モデルと上記検証ツールでは使用されないカバレッジ基準（状態カバレッジ、遷移カバレッジ、パスカバレッジ）とを与えることで、テスト項目を自動生成する技術である。
【０００５】
図９は、検証対象についての有限状態機械モデルを示す説明図である。図９の有限状態機械モデル９００中、“Ｓ０”，“Ｓ１”，“Ｓ２”は状態を、“ｒｅｓｅｔ”，“！ｒｅｓｅｔ＆ｍｏｄｅ＝０”，“！ｒｅｓｅｔ＆ｍｏｄｅ＝１”は遷移をあらわしている。
【０００６】
図１０は、状態カバレッジを示す説明図である。図１０において、左欄は、従来のＳＢＴ技術により生成される状態カバレッジによりカバーされるシーケンス（パス集合）であり、右欄は、状態カバレッジではカバーできないパスを示している。
【０００７】
図１１は、遷移カバレッジを示す説明図である。図１１において、左欄は、従来のＳＢＴ技術により生成される遷移カバレッジによりカバーされるシーケンス（パス集合）であり、右欄は、遷移カバレッジではカバーできないパスを示している。
【０００８】
図１２は、パスカバレッジを示す説明図である。図１２では、状態“Ｓ０”から状態“Ｓ０”までのパスカバレッジによりカバーされるシーケンス（パス集合）を示している。
【０００９】
【特許文献１】特開２００６−２０９５２１号公報
【特許文献２】特開平５−２１５８１９号公報
【特許文献３】特開平６−１９５２１６号公報
【特許文献４】特開２００３−１０８４０５号公報
【発明の開示】
【発明が解決しようとする課題】
【００１０】
しかしながら、上述した図１０の状態カバレッジでは、右欄のパスは、状態Ｓ２をカバーできていない。このように、状態カバレッジでは、パスをカバーできない場合があるという問題がある。また、上述した図１１の遷移カバレッジでは、右欄のパスは、状態“Ｓ０”で自己ループする遷移“ｒｅｓｅｔ”をカバーできていない。このように、遷移カバレッジでは、状態カバレッジと同様、パスをカバーできない場合があるという問題がある。
【００１１】
また、図１２に示したように、パスカバレッジでは、全パスをカバーできるが、ループが含まれるとパス数が無限になり、すべて検証するには現実的でないという問題がある。また、同じループは２度通らないという制約を付けることでパス数を有限個に抑えることは可能であるが、どの状態が開始条件で、どの状態が終了状態であるかを特定することができないという問題がある。
【００１２】
本技術は、上述した従来技術による問題点を解消するため、テスト項目の網羅性および品質の向上を図ることができる検証支援プログラム、検証支援装置、および検証支援方法を提供することを目的とする。
【課題を解決するための手段】
【００１３】
上述した課題を解決し、目的を達成するため、本開示技術は、検証対象に関するユースケース図の中から任意のユースケースを選択し、選択ユースケースの事前条件および事後条件を抽出し、前記選択ユースケースに対応する有限状態機械モデルをＫｒｉｐｋｅモデルに変換し、抽出された事前条件および事後条件に基づいて、前記ＫｒｉｐｋｅモデルのＫｒｉｐｋｅ初期状態、Ｋｒｉｐｋｅ事前条件およびＫｒｉｐｋｅ事後条件を特定し、前記Ｋｒｉｐｋｅ事前条件および前記Ｋｒｉｐｋｅ事後条件に基づいて、前記選択ユースケースのＫｒｉｐｋｅプロパティを生成することを要件とする。
【発明の効果】
【００１４】
この検証支援プログラム、検証支援装置、および検証支援方法によれば、テスト項目の網羅性および品質の向上を図ることができるという効果を奏する。
【発明を実施するための最良の形態】
【００１５】
以下に添付図面を参照して、本開示技術の好適な実施の形態を詳細に説明する。図１は、本開示技術の概要を示す説明図である。本開示技術では、検証対象のユースケース図１０１からユースケース（たとえば、ユースケース１）を選択するとともに、検証対象の仕様をあらわす有限状態機械モデル群１０２から当該ユースケース１に対応する有限状態機械モデル９００を選択する。
【００１６】
そして、選択された有限状態機械モデル９００をＫｒｉｐｋｅモデル１０３に変換する。Ｋｒｉｐｋｅモデル１０３は、有限状態機械モデル９００内の遷移を状態とするモデルである。このＫｒｉｐｋｅモデル１０３からＫｒｉｐｋｅプロパティを生成する。符号１０４は、Ｋｒｉｐｋｅプロパティの制約式である。
【００１７】
Ｋｒｉｐｋｅプロパティが求まれば、Ｋｒｉｐｋｅプロパティを公知の形式検証ツールに与えるだけで、ユースケースの状態カバレッジ（ＵＣＳＣ）用Ｔｒａｐプロパティ１０５とユースケースの遷移カバレッジ（ＵＣＴＣ）用Ｔｒａｐプロパティ１０６を得ることができる。ここで、「プロパティ」とは、たとえば、“ａはｂより大きい”というような制約条件式である。
【００１８】
また、Ｋｒｉｐｋｅプロパティとは、Ｋｒｉｐｋｅモデル１０３から得られるプロパティである。また、Ｔｒａｐプロパティとは、『元となるプロパティ（この場合はＫｒｉｐｋｅプロパティ）を満たしたときは、テストする／しない』といった元となるプロパティの制約条件式である。本開示技術では、Ｔｒａｐプロパティは、パス集合で表現される。
【００１９】
図１に示したように、検証対象をユースケース図１０１で表現した場合、検証対象が実現しようとする機能をあらわすユースケースにより構成されている。各ユースケースは、事前条件、事後条件およびパスを有する。ここで、事前条件とは、ユースケースを開始するために真となる条件である。事後条件とは、ユースケース実行後に真になる条件である。パスとは、事前条件から事後条件に到達可能なシーケンスである。すなわち、ユースケースは、事前条件から事後条件に到達可能なすべてのシーケンスの集合である。
【００２０】
図２は、ユースケース１の内容を示す説明図である。図２において、パス１およびパス２は、事前条件（Ｓ０）と事後条件（Ｓ１）を満たしている。
【００２１】
（検証支援装置のハードウェア構成）
図３は、実施の形態にかかる検証支援装置のハードウェア構成を示すブロック図である。図３において、検証支援装置は、ＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）３０１と、ＲＯＭ（Ｒｅａｄ‐Ｏｎｌｙ  Ｍｅｍｏｒｙ）３０２と、ＲＡＭ（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ）３０３と、磁気ディスクドライブ３０４と、磁気ディスク３０５と、光ディスクドライブ３０６と、光ディスク３０７と、ディスプレイ３０８と、Ｉ／Ｆ（Ｉｎｔｅｒｆａｃｅ）３０９と、キーボード３１０と、マウス３１１と、スキャナ３１２と、プリンタ３１３と、を備えている。また、各構成部はバス３００によってそれぞれ接続されている。
【００２２】
ここで、ＣＰＵ３０１は、検証支援装置の全体の制御を司る。ＲＯＭ３０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ３０３は、ＣＰＵ３０１のワークエリアとして使用される。磁気ディスクドライブ３０４は、ＣＰＵ３０１の制御にしたがって磁気ディスク３０５に対するデータのリード／ライトを制御する。磁気ディスク３０５は、磁気ディスクドライブ３０４の制御で書き込まれたデータを記憶する。
【００２３】
光ディスクドライブ３０６は、ＣＰＵ３０１の制御にしたがって光ディスク３０７に対するデータのリード／ライトを制御する。光ディスク３０７は、光ディスクドライブ３０６の制御で書き込まれたデータを記憶したり、光ディスク３０７に記憶されたデータをコンピュータに読み取らせたりする。
【００２４】
ディスプレイ３０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ３０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００２５】
インターフェース（以下、「Ｉ／Ｆ」と略する。）３０９は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク３１４に接続され、このネットワーク３１４を介して他の装置に接続される。そして、Ｉ／Ｆ３０９は、ネットワーク３１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ３０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００２６】
キーボード３１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力をおこなう。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス３１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などをおこなう。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００２７】
スキャナ３１２は、画像を光学的に読み取り、検証支援装置内に画像データを取り込む。なお、スキャナ３１２は、ＯＣＲ（Ｏｐｔｉｃａｌ  Ｃｈａｒａｃｔｅｒ  Ｒｅａｄｅｒ）機能を持たせてもよい。また、プリンタ３１３は、画像データや文書データを印刷する。プリンタ３１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００２８】
（検証支援装置の機能的構成）
つぎに、検証支援装置の機能的構成について説明する。図４は、実施の形態にかかる検証支援装置の機能的構成を示すブロック図である。検証支援装置４００は、選択部４０１と、抽出部４０２と、取得部４０３と、変換部４０４と、特定部４０５と、生成部４０６と、を含む構成である。この制御部となる機能（選択部４０１〜生成部４０６）は、具体的には、たとえば、図３に示したＲＯＭ３０２、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶領域に記憶されたプログラムをＣＰＵ３０１に実行させることにより、または、Ｉ／Ｆ３０９により、その機能を実現する。
【００２９】
選択部４０１は、検証対象のユースケース図１０１の中から、任意のユースケースを選択する機能を有する。具体的には、たとえば、未選択のユースケースを選択する。この選択部４０１により、ユースケース図１０１内のすべてのユースケースを網羅的に選択することができる。以降、選択されたユースケースを「選択ユースケース」と称す。選択ユースケースは、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶領域に記憶される。
【００３０】
抽出部４０２は、選択ユースケースの事前条件および事後条件を抽出する機能を有する。ユースケース内には、図２に示したように、事前条件と事後条件の記述が存在するため、当該記述を抽出する。抽出された事前条件および事後条件は、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶領域に記憶される。
【００３１】
取得部４０３は、選択ユースケースに対応する有限状態機械モデル９００を取得する機能を有する。有限状態機械モデル９００は、検証対象のユースケースの仕様をあらわす。どの有限状態機械モデル９００がどのユースケースに対応するかは、検証者が判断して与えることとなる。取得された有限状態機械モデル９００は、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶領域に記憶される。
【００３２】
変換部４０４は、選択ユースケースに対応する有限状態機械モデル９００をＫｒｉｐｋｅモデル１０３に変換する機能を有する。Ｋｒｉｐｋｅモデル１０３は、有限状態機械モデル９００の遷移を基準とするモデルである。
【００３３】
図５は、有限状態機械モデル９００からＫｒｉｐｋｅモデル１０３への変換例を示す説明図である。図５に示したＫｒｉｐｋｅモデル１０３において、状態“Ｋ０”は、状態“Ｓ０”における遷移“ｒｅｓｅｔ”とその遷移元である状態“Ｓ０”とを有する状態である。状態“Ｋ１”は、状態“Ｓ０”における遷移“！ｒｅｓｅｔ＆ｍｏｄｅ＝０”でかつ“ｆｌａｇ＝０”とその遷移元である状態“Ｓ０”とを有する状態である。
【００３４】
状態“Ｋ２”は、状態“Ｓ０”における遷移“！ｒｅｓｅｔ＆ｍｏｄｅ＝０” でかつ“ｆｌａｇ＝１”とその遷移元である状態“Ｓ０”とを有する状態である。状態“Ｋ３”は、状態“Ｓ１”における遷移“！ｒｅｓｅｔ”とその遷移元である状態“Ｓ１”とを有する状態である。
【００３５】
状態“Ｋ４”は、状態“Ｓ０”における遷移“！ｒｅｓｅｔ＆ｍｏｄｅ＝１”でかつ“ｆｌａｇ＝０”とその遷移元である状態“Ｓ０”とを有する状態である。状態“Ｋ５”は、状態“Ｓ０”における遷移“！ｒｅｓｅｔ＆ｍｏｄｅ＝１”でかつ“ｆｌａｇ＝１”とその遷移元である状態“Ｓ０”とを有する状態である。状態“Ｋ６”は、状態“Ｓ２”における遷移“！ｒｅｓｅｔ”とその遷移元である状態“Ｓ１”とを有する状態である。
【００３６】
なお、有限状態機械モデル９００からＫｒｉｐｋｅモデル１０３への変換は公知であるため、有限状態機械モデル９００からＫｒｉｐｋｅモデル１０３へ変換するツールであれば、どのような手法を適用してもよい。Ｋｒｉｐｋｅモデル１０３は、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶領域に記憶される。
【００３７】
また、図４において、特定部４０５は、抽出部４０２によって抽出された事前条件および事後条件に基づいて、変換部４０４によって変換されたＫｒｉｐｋｅモデル１０３のＫｒｉｐｋｅ初期状態、Ｋｒｉｐｋｅ事前条件およびＫｒｉｐｋｅ事後条件を特定する機能を有する。Ｋｒｉｐｋｅ初期状態とは、Ｋｒｉｐｋｅモデル１０３における初期状態である。
【００３８】
Ｋｒｉｐｋｅ事前条件とは、Ｋｒｉｐｋｅモデル１０３における事前条件をあらわす状態である。Ｋｒｉｐｋｅ事後条件とは、Ｋｒｉｐｋｅモデル１０３における事後条件をあらわす状態である。ここで、ユースケース１の事前条件は、状態“Ｓ０”であり、遷移“ｒｅｓｅｔ”により状態“Ｓ０”を維持する。したがって、“Ｓ０＆ｒｅｓｅｔ”である状態“Ｋ１”がＫｒｉｐｋｅ初期状態となる。
【００３９】
また、ユースケース１の事後条件は、状態“Ｓ１”であり、遷移“！ｒｅｓｅｔ”により状態“Ｓ１”を維持する。したがって、“Ｓ１＆！ｒｅｓｅｔ”である状態“Ｋ３”がＫｒｉｐｋｅ事後条件となる。また、状態“Ｋ３”がＫｒｉｐｋｅ事後条件なので、その遷移元の状態“Ｋ１”，“Ｋ２”がＫｒｉｐｋｅ事前条件となる。
【００４０】
なお、ユースケース１の事後条件が“Ｓ１ｏｒＳ２”である場合、Ｋｒｉｐｋｅ事後条件は、“Ｋ３ｏｒＫ６”であり、Ｋｒｉｐｋｅ事前条件も“Ｋ１ｏｒＫ２ｏｒＫ３ｏｒＫ４”となる。特定されたＫｒｉｐｋｅ初期状態、Ｋｒｉｐｋｅ事前条件、およびＫｒｉｐｋｅ事後条件は、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶領域に記憶される。
【００４１】
図４において、生成部４０６は、特定部４０５によって特定されたＫｒｉｐｋｅ事前条件およびＫｒｉｐｋｅ事後条件に基づいて、選択ユースケースのＫｒｉｐｋｅプロパティを生成する機能を有する。具体的には、Ｋｒｉｐｋｅ事前条件からＫｒｉｐｋｅ事後条件までの全状態を通す選択ユースケースのＫｒｉｐｋｅプロパティを生成する。
【００４２】
このＫｒｉｐｋｅプロパティをユースケースの状態カバレッジ（以下、「ＵＣＳＣ」と略す。）用Ｋｒｉｐｋｅプロパティと称す。また、Ｋｒｉｐｋｅ事前条件からＫｒｉｐｋｅ事後条件までの全遷移を通す選択ユースケースのＫｒｉｐｋｅプロパティを生成する。このＫｒｉｐｋｅプロパティをユースケースの遷移カバレッジ（以下、「ＵＣＴＣ」と略す。）用Ｋｒｉｐｋｅプロパティと称す。
【００４３】
Ｋｒｉｐｋｅプロパティは、『ＡＧ（Ｋｒｉｐｋｅ事前条件−＞！ＥＸ  Ｋｒｉｐｋｅ事後条件）』という制約式で表現される。“ＡＧ”、“ＥＸ”は計算木論理の作用素のセットである。このＫｒｉｐｋｅプロパティの制約式に、Ｋｒｉｐｋｅ事前条件とＫｒｉｐｋｅ事後条件を代入することで、Ｋｒｉｐｋｅプロパティが生成される。
【００４４】
具体的には、ＵＣＳＣ用Ｋｒｉｐｋｅプロパティを生成する場合、Ｋｒｉｐｋｅプロパティの制約式に、全Ｋｒｉｐｋｅ事前条件の論理和とＫｒｉｐｋｅ事後条件を代入する。たとえば、Ｋｒｉｐｋｅ事前条件が状態“Ｋ１ｏｒＫ２”、Ｋｒｉｐｋｅ事後条件が状態“Ｋ３”である場合、ＵＣＳＣ用Ｋｒｉｐｋｅプロパティは、『ＡＧ（Ｋ１ｏｒＫ２）−＞！ＥＸ（Ｋ３）』、すなわち、『ＡＧ（！ｒｅｓｅｔ）−＞！ＥＸ（Ｓ１）』となる。
【００４５】
また、ＵＣＴＣ用Ｋｒｉｐｋｅプロパティを生成する場合、全Ｋｒｉｐｋｅ事前条件の論理和およびＫｒｉｐｋｅ初期状態からの遷移先と、Ｋｒｉｐｋｅ事後条件とを代入する。たとえば、Ｋｒｉｐｋｅ事前条件が状態“Ｋ１ｏｒＫ２”、Ｋｒｉｐｋｅ事後条件が状態“Ｋ３”である場合、ＵＣＴＣ用Ｋｒｉｐｋｅプロパティは、『ＡＧ（！ｒｅｓｅｔ＆Ｋ１＆Ｋ２）−＞！ＥＸ（Ｓ１）』となる。生成されたＫｒｉｐｋｅプロパティは、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶領域に記憶される。
【００４６】
また、生成部４０６は、Ｋｒｉｐｋｅプロパティに基づいて、Ｔｒａｐプロパティを生成する機能を有する。具体的には、たとえば、公知の形式検証ツールにＫｒｉｐｋｅプロパティを与えることで、Ｔｒａｐプロパティが返ってくる。
【００４７】
図６は、ＵＣＳＣ用Ｔｒａｐプロパティ１０５の記述例を示す説明図である。図６に示されたＴｅｓｔ１〜Ｔｅｓｔ３のパスは、ユースケース１の事前条件“Ｓ０”と事後条件“Ｓ１”を含むため、正例のシーケンスである。事前条件“Ｓ０”と事後条件“Ｓ１”のうち少なくともいずれか一方が含まれていない場合は反例のシーケンスとなる。
【００４８】
図７は、ＵＣＴＣ用Ｔｒａｐプロパティ１０６の記述例を示す説明図である。図７に示されたＴｅｓｔ１，Ｔｅｓｔ２のパスは、ユースケース１の事前条件“Ｓ０”と事後条件“Ｓ１”を含むため、正例のシーケンスである。一方、事前条件“Ｓ０”と事後条件“Ｓ１”のうち少なくともいずれか一方が含まれていない場合は反例のシーケンスとなる。Ｔｅｓｔ３のパスは、事後条件“Ｓ１”を含まないため反例のシーケンスとなる。
【００４９】
生成されたＴｒａｐプロパティは、ＲＡＭ３０３、磁気ディスク３０５、光ディスク３０７などの記憶領域に記憶される。なお、ＫｒｉｐｋｅプロパティやＴｒａｐプロパティは、必要に応じて、ディスプレイ３０８へ表示したり、プリンタ３１３から印刷出力したり、外部に送信することができる。
【００５０】
（検証支援装置の検証支援処理手順）
図８は、実施の形態にかかる検証支援装置４００の検証支援処理手順を示すフローチャートである。まず、検証対処のユースケース図１０１を取得し（ステップＳ８０１）、未処理のユースケースがあるか否かを判断する（ステップＳ８０２）。未処理のユースケースがある場合（ステップＳ８０２：Ｙｅｓ）、選択部４０１により未処理のユースケースを１つ選択する（ステップＳ８０３）。
【００５１】
そして、抽出部４０２により選択ユースケースから事前条件および事後条件を抽出する（ステップＳ８０４）。このあと、取得部４０３により選択ユースケースの有限状態機械モデル９００を取得し（ステップＳ８０５）、変換部４０４により、有限状態機械モデル９００をＫｒｉｐｋｅモデル１０３に変換する（ステップＳ８０６）。
【００５２】
そして、特定部４０５により、Ｋｒｉｐｋｅ初期状態、Ｋｒｉｐｋｅ事前条件、およびＫｒｉｐｋｅ事後条件を特定し（ステップＳ８０７）、生成部４０６により選択ユースケースのＫｒｉｐｋｅプロパティを生成する（ステップＳ８０８）。そして、生成されたＫｒｉｐｋｅプロパティを形式検証ツールに与えることにより、選択ユースケースのＴｒａｐプロパティを生成する（ステップＳ８０９）。このあと、ステップＳ８０２に戻る。ステップＳ８０２において、未処理のユースケースがない場合（ステップＳ８０２：Ｎｏ）、一連の検証支援処理を終了する。
【００５３】
なお、上述した有限状態機械モデル９００では、ループの定義について、同じ遷移を複数回通る場合（たとえば、２回ループの例：＜Ｓ０，ｒｅｓｅｔ，Ｓ０，ｒｅｓｅｔ，Ｓ０＞、２回ループではない例：＜Ｓ０，ｒｅｓｅｔ，Ｓ０，！ｒｅｓｅｔ＆ｍｏｄｅ＝０，Ｓ１，ｒｅｓｅｔ，Ｓ０＞）、『ループを認めない』、『ループを1回だけ認める』、『ループを指定した回数まで認める』といった制約を設定することとしてもよい。
【００５４】
このように、従来のＳＢＴ技術における状態カバレッジや遷移カバレッジに対して、ユースケースの事前条件および事後条件を用いるため、ユースケースの事前条件と事後条件との間のパスをカバーするテストを生成できる。またこれにより、テスト項目の品質向上が可能となる。さらに、従来のパスカバレッジに対して、現実のテスト項目数に絞り込める可能性が高くなり、検証期間の短縮化を図ることができる。また、パスカバレッジでしかカバーできないパスの一部もカバーすることができる。以上説明したように、本実施の形態によれば、テスト項目の網羅性および品質の向上を図ることができるという効果を奏する。
【００５５】
なお、本実施の形態で説明した検証支援方法は、予め用意されたプログラムをパーソナル・コンピュータやワークステーション等のコンピュータで実行することにより実現することができる。このプログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤ等のコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。またこのプログラムは、インターネット等のネットワークを介して配布することが可能な媒体であってもよい。
【図面の簡単な説明】
【００５６】
【図１】本開示技術の概要を示す説明図である。
【図２】ユースケース１の内容を示す説明図である。
【図３】実施の形態にかかる検証支援装置のハードウェア構成を示すブロック図である。
【図４】実施の形態にかかる検証支援装置の機能的構成を示すブロック図である。
【図５】有限状態機械モデルからＫｒｉｐｋｅモデルへの変換例を示す説明図である。
【図６】ＵＣＳＣ用Ｔｒａｐプロパティの記述例を示す説明図である。
【図７】ＵＣＴＣ用Ｔｒａｐプロパティの記述例を示す説明図である。
【図８】実施の形態にかかる検証支援装置の検証支援処理手順を示すフローチャートである。
【図９】検証対象についての有限状態機械モデルを示す説明図である。
【図１０】状態カバレッジを示す説明図である。
【図１１】遷移カバレッジを示す説明図である。
【図１２】パスカバレッジを示す説明図である。
【符号の説明】
【００５７】
１０３  Ｋｒｉｐｋｅモデル
１０５  ＵＣＳＣ用Ｔｒａｐプロパティ
１０６  ＵＣＴＣ用Ｔｒａｐプロパティ
４００  検証支援装置
４０１  選択部
４０２  抽出部
４０３  取得部
４０４  変換部
４０５  特定部
４０６  生成部
９００  有限状態機械モデル
【図１】
2010009384.tif 000003
【図２】
2010009384.tif 000004
【図３】
2010009384.tif 000005
【図４】
2010009384.tif 000006
【図５】
2010009384.tif 000007
【図６】
2010009384.tif 000008
【図７】
2010009384.tif 000009
【図８】
2010009384.tif 000010
【図９】
2010009384.tif 000011
【図１０】
2010009384.tif 000012
【図１１】
2010009384.tif 000013
【図１２】
2010009384.tif 000014