(57)【要約】      （修正有）【課題】ハードウエアまたはソフトウエアを含む複数の部品から成るシステムを構築する場合において、隣接する部品同士間の整合性を検証および調整し、システムのテストにおいてテストケースの数の爆発を抑制し適切なテスト工数を見込む設計を行うためのテスト容易化設計装置ならびにその方法を提供する。【解決手段】システム仕様、および部品毎の動作仕様と入力制約を記憶する手段と、動作仕様に示される遷移を網羅する状態遷移パスとそれに対応する出力アクション列を取得する手段と、第１の部品の出力アクション列が接続する第２の部品の入力制約を充足するか否かを検査する手段と、充足されないとき、前記第１の部品の入力制約を強化し、または前記第２の部品の入力制約を緩和する手段と、各部品対間のそれぞれを、前記部品対の一方および他方の部品に対応する出力アクション列が対応する入力制約を充足するよう、整合させる制御部と、を備える。【選択図】図１
2010128583.tif 000002
【特許請求の範囲】
【請求項１】
対象システムを形成する複数の部品間の接続関係、および前記部品毎に前記部品に接続される他の部品または外部との間で入出力されるアクションの内容を記述したシステム仕様を記憶する第１記憶部と、
前記部品毎に、入力アクションの発生による複数の状態間の遷移および前記遷移の際に発生する出力アクションを記述した動作仕様を記憶する第２記憶部と、
前記部品毎に前記入力アクションの発生順序に関する入力制約を記憶する第３記憶部と、
部品の入力制約を満たすように前記部品の動作仕様に示される遷移を網羅する状態遷移パスを特定し、前記状態遷移パスに対応する出力アクション列を取得するアクション列取得部と、
前記システムにおいて互いに接続される部品対を選択する選択部と、
前記部品対の一方または他方である第１の部品に対応する出力アクション列が前記部品対の他方または一方である第２の部品の入力制約を充足するか否かを検査する検査部と、
前記第２の部品の入力制約が充足されないとき、（１）前記第２の部品の入力制約を充足する出力アクション列が取得されるように前記第３記憶部における前記第１の部品の入力制約を強化し、または、（２）前記第１の部品に対応する出力アクション列が充足されるように前記第３記憶部における前記第２の部品の入力制約を緩和する、入力制約調整部と、
前記システムにおいて互いに接続される各部品対間のそれぞれを、前記部品対の一方および他方の部品に対応する出力アクション列が前記部品対の他方および一方の部品に対応する入力制約を充足するよう、整合させるように前記選択部、前記検査部および前記入力制約調整部を制御する制御部と、
を備えたテスト容易化設計装置。
【請求項２】
部品の入力制約に従って前記部品の動作仕様に含まれる遷移を制限した仕様を表す状態遷移機械モデルを生成するモデル生成部をさらに備え、
前記制御部は、前記モデル生成部をさらに制御し、
前記制御部は、
（１）前記選択部により前記対象システムにおける１つの部品Ｚ０を選択し、
（２）前記部品Ｚ０に接続される部品Ｚ０＿ｉを特定し、
（３）前記部品Ｚ０と各部品Ｚ０＿ｉとの間、ならびに、各部品Ｚ０＿ｉのうち互いに接続される部品同士間を前記検査部および前記入力制約調整部により整合させ、各部品Ｚ０＿ｉの状態遷移機械モデルを前記生成部により生成し、各部品Ｚ０＿ｉの状態遷移機械モデルを合成することにより各部品Ｚ０＿ｉの部品集合Ｚ１の動作仕様を生成し、
（４）前記部品集合Ｚ１と前記部品Ｚ０との間を前記検査部および前記入力制約調整部により整合させ、前記部品集合Ｚと前記部品Ｚ０の各々の状態遷移機械モデルを前記生成部により生成し、前記部品集合Ｚと前記部品Ｚ０の各々の状態遷移機械モデルを合成することにより前記部品集合Ｚ１と前記部品Ｚ０とを組み合わせた上位階層部品Ｚ２の動作仕様を生成し、
（５）前記対象システムから前記部品Ｚ０と部品Ｚ０−ｉを除いた残り部品と前記上位階層部品Ｚ２とを含むシステムについて（１）〜（４）を繰り返し、
前記システムに含まれる部品数が１つになったら繰り返しを終了して、最後に生成された上位階層部品Ｚ２の動作仕様である前記システムの動作仕様を前記第２記憶部に格納する
ことを特徴とする請求項１に記載の装置。
【請求項３】
前記検査部は、前記第１の部品に対応する出力アクション列の中から前記第２の部品の入力制約に違反するＮＧアクションを検出し、
前記入力制約調整部は、前記第１の部品の動作仕様に基づき前記ＮＧアクションが出力されるときの遷移元状態および入力アクションを特定し、特定した遷移元状態からの特定した入力アクションによる遷移を禁止するように前記第１の部品の入力制約を修正することを特徴とする請求項１または２に記載の装置。
【請求項４】
前記検査部は、前記第１の部品に対応する出力アクション列の中から前記第２の部品の入力制約に違反するＮＧアクションを検出し、
前記入力制約調整部は、前記第２の部品の動作仕様に基づき前記ＮＧアクションの遷移元状態を特定し、特定した遷移元状態からの前記ＮＧアクションによる遷移が前記第２の部品の動作仕様に存在するかどうかを検査し、存在するときは、前記特定した遷移基状態から前記ＮＧアクションによる遷移を許容するように前記第２の部品の入力制約を修正することを特徴とする請求項１ないし３のいずれか一項に記載の装置。
【請求項５】
前記第２の部品の入力制約が充足されるとき、前記第１の部品に対応する出力アクション列が前記第２の部品の入力制約を充足する限りにおいて、前記第２の部品の動作仕様に含まれる遷移を制限するように前記第２の部品の入力制約を強化する入力制約強化部をさらに備え、
前記制御部は、前記入力制約強化部をさらに制御することを特徴とする請求項１ないし４のいずれか一項に記載の装置。
【請求項６】
各前記部品の入力制約を、各前記部品の動作仕様から抽出するまたは外部の記憶装置から読み出す入力制約抽出部をさらに備え、
前記入力制約抽出部は、抽出または読み出した各前記部品の入力制約を前記第３記憶部に格納することを特徴とする請求項１ないし４のいずれか一項に記載の装置。
【請求項７】
前記制御部は、前記システムの動作仕様から前記システムの入力制約を抽出し、抽出した入力制約を前記第３記憶部に格納することを特徴とする請求項２に記載の装置。
【請求項８】
前記制御部による処理が完了した後前記第３記憶部内の各前記部品またはシステムの入力制約を満たすことを要求するアサーション記述を生成し、生成したアサーション記述を前記システム仕様に追加するアサーション生成部をさらに備えたことを特徴とする請求項７に記載の装置。
【請求項９】
前記アサーション記述の成立性を監視する監視モジュールの仕様と、前記監視モジュールにより異常が検知された場合に前記異常内容に応じた回避処理を行う回避モジュールの仕様とを生成し、前記監視モジュールの仕様と前記回避モジュールの仕様とを前記システム仕様に追加するモジュール生成部をさらに備えたことを特徴とする請求項８に記載の装置。
【請求項１０】
コンピュータにおいて実行するテスト容易化設計方法であって、
対象システムを形成する複数の部品間の接続関係、および前記部品毎に前記部品に接続される他の部品または外部との間で入出力されるアクションの内容を記述したシステム仕様を第１記憶部に記憶する第１記憶ステップと、
前記部品毎に、入力アクションの発生による複数の状態間の遷移および前記遷移の際に発生する出力アクションを記述した動作仕様を第２記憶部に記憶する第２記憶ステップと、
前記部品毎に前記入力アクションの発生順序に関する入力制約を第３記憶部に記憶する第３記憶ステップと、
部品の入力制約を満たすように前記部品の動作仕様に示される遷移を網羅する状態遷移パスを特定し、前記状態遷移パスに対応する出力アクション列を取得するアクション列取得ステップと、
前記システムにおいて互いに接続される部品対を選択する選択ステップと、
前記部品対の一方または他方である第１の部品に対応する出力アクション列が前記部品対の他方または一方である第２の部品の入力制約を充足するか否かを検査する検査ステップと、
前記第２の部品の入力制約が充足されないとき、（１）前記第２の部品の入力制約を充足する出力アクション列が取得されるように前記第３記憶部における前記第１の部品の入力制約を強化し、または、（２）前記第１の部品に対応する出力アクション列が充足されるように前記第３記憶部における前記第２の部品の入力制約を緩和する、入力制約調整ステップと、
前記システムにおいて互いに接続される各部品対間のそれぞれを、前記部品対の一方および他方の部品に対応する出力アクション列が前記部品対の他方および一方の部品に対応する入力制約を充足するよう、整合させるように前記選択ステップ、前記検査ステップおよび前記入力制約調整ステップを制御する制御ステップと、
を前記コンピュータが実行するテスト容易化設計方法。
【請求項１１】
対象システムを形成する複数の部品間の接続関係、および前記部品毎に前記部品に接続される他の部品または外部との間で入出力されるアクションの内容を記述したシステム仕様を第１記憶部に記憶する第１記憶ステップと、
前記部品毎に、入力アクションの発生による複数の状態間の遷移および前記遷移の際に発生する出力アクションを記述した動作仕様を第２記憶部に記憶する第２記憶ステップと、
前記部品毎に前記入力アクションの発生順序に関する入力制約を第３記憶部に記憶する第３記憶ステップと、
部品の入力制約を満たすように前記部品の動作仕様に示される遷移を網羅する状態遷移パスを特定し、前記状態遷移パスに対応する出力アクション列を取得するアクション列取得ステップと、
前記システムにおいて互いに接続される部品対を選択する選択ステップと、
前記部品対の一方または他方である第１の部品に対応する出力アクション列が前記部品対の他方または一方である第２の部品の入力制約を充足するか否かを検査する検査ステップと、
前記第２の部品の入力制約が充足されないとき、（１）前記第２の部品の入力制約を充足する出力アクション列が取得されるように前記第３記憶部における前記第１の部品の入力制約を強化し、または、（２）前記第１の部品に対応する出力アクション列が充足されるように前記第３記憶部における前記第２の部品の入力制約を緩和する、入力制約調整ステップと、
前記システムにおいて互いに接続される各部品対間のそれぞれを、前記部品対の一方および他方の部品に対応する出力アクション列が前記部品対の他方および一方の部品に対応する入力制約を充足するよう、整合させるように前記選択ステップ、前記検査ステップおよび前記入力制約調整ステップを制御する制御ステップと、
をコンピュータに実行させるためのコンピュータプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ハードウエアまたはソフトウエアを含むシステムのテストにおいてテストケースの数の爆発を抑制し適切なテスト工数を見込む設計を行うためのテスト容易化設計装置ならびにその方法およびプログラムに関する。
【背景技術】
【０００２】
ソフトウエアの開発規模が増大すると同時に、短期間開発、シリーズ展開等を行なわなくてはならなく、高品質なソフトウエアを作成することが難しくなってきている。この問題の解決手段の一つとしてソフトウエアを部品化してこれを再利用して設計生産性を高める工夫が行われてきた（非特許文献１参照）。
【０００３】
一方、動作仕様をモデルとして、モデルからテストケースを生成する技術がモデル駆動テスト技術(以下MDT)として開発されてきた。テストケース生成においては、仕様に対して与えられる入力制約によりテストケースの質を制御する。例えば入力制約を強化すれば、テストすべきテストケースは削減され、逆の場合にはテストケースは増える。このようにMDTにおいては入力制約と生成されるテストケースの間の相関関係がある（非特許文献２）。
【非特許文献１】"Interface automata", Alfaro, L. and Henzinger, T.A. ACM SIGSOFT Software Engineering Notes,26:55, 109-120, 2001.
【非特許文献２】"Model-based testing of object-oriented reactive systems with Spec Explorer", Campbell, C. and Grieskamp, W. and Nachmanson, L. and Schulte, W. and Tillmann, N. and Veanes, Microsoft Research MSR-TR-2005-59, May,2005
【発明の開示】
【発明が解決しようとする課題】
【０００４】
従来のソフトウエアの部品化では、部品のインターフェイスに着目し、インターフェイスの性質を定義して、これを用いていわゆる契約ベースの設計を行うことにより、高い品質を保とうとしていた。しかし、インターフェイスのみに着目した技術では、部品同士の結合の補助にはなるが、部品の入力と出力との間の因果関係が不明確なので、部品を全体に組み込んだときの隣接する部品間同士間の動作仕様の整合性を検証したり調整したりすることが困難であった。また部品を組み合わせて初めて発生する動作に関する制約を取り扱うことが困難であった。
【０００５】
一方モデル駆動テストにおいては、仕様を状態遷移機械に一旦変換し状態遷移機械を探索することによりテストケースを生成する。対象システムの規模が大きくなると状態爆発を起こす。特に並列に動作する分散システムにおいては、状態爆発問題は顕著である。このためモデル駆動開発は小規模の部品単位すなわち単体テストにしか適用できなかった。
【０００６】
本発明は、複数の部品から成るシステムを構築する場合において隣接する部品同士間の整合性を検証および調整することを可能としたテスト容易化設計装置ならびにその方法およびプログラムを提供する。
【課題を解決するための手段】
【０００７】
本発明の一態様としてのテスト容易化設計装置は、
対象システムを形成する複数の部品間の接続関係、および前記部品毎に前記部品に接続される他の部品または外部との間で入出力されるアクションの内容を記述したシステム仕様を記憶する第１記憶部と、
前記部品毎に、入力アクションの発生による複数の状態間の遷移および前記遷移の際に発生する出力アクションを記述した動作仕様を記憶する第２記憶部と、
前記部品毎に前記入力アクションの発生順序に関する入力制約を記憶する第３記憶部と、
部品の入力制約を満たすように前記部品の動作仕様に示される遷移を網羅する状態遷移パスを特定し、前記状態遷移パスに対応する出力アクション列を取得するアクション列取得部と、
前記システムにおいて互いに接続される部品対を選択する選択部と、
前記部品対の一方または他方である第１の部品に対応する出力アクション列が前記部品対の他方または一方である第２の部品の入力制約を充足するか否かを検査する検査部と、
前記第２の部品の入力制約が充足されないとき、（１）前記第２の部品の入力制約を充足する出力アクション列が取得されるように前記第３記憶部における前記第１の部品の入力制約を強化し、または、（２）前記第１の部品に対応する出力アクション列が充足されるように前記第３記憶部における前記第２の部品の入力制約を緩和する、入力制約調整部と、
前記システムにおいて互いに接続される各部品対間のそれぞれを、前記部品対の一方および他方の部品に対応する出力アクション列が前記部品対の他方および一方の部品に対応する入力制約を充足するよう、整合させるように前記選択部、前記検査部および前記入力制約調整部を制御する制御部と、
を備える。
【０００８】
本発明の一態様としてのテスト容易化設計方法は、
コンピュータにおいて実行するテスト容易化設計方法であって、
対象システムを形成する複数の部品間の接続関係、および前記部品毎に前記部品に接続される他の部品または外部との間で入出力されるアクションの内容を記述したシステム仕様を第１記憶部に記憶する第１記憶ステップと、
前記部品毎に、入力アクションの発生による複数の状態間の遷移および前記遷移の際に発生する出力アクションを記述した動作仕様を第２記憶部に記憶する第２記憶ステップと、
前記部品毎に前記入力アクションの発生順序に関する入力制約を第３記憶部に記憶する第３記憶ステップと、
部品の入力制約を満たすように前記部品の動作仕様に示される遷移を網羅する状態遷移パスを特定し、前記状態遷移パスに対応する出力アクション列を取得するアクション列取得ステップと、
前記システムにおいて互いに接続される部品対を選択する選択ステップと、
前記部品対の一方または他方である第１の部品に対応する出力アクション列が前記部品対の他方または一方である第２の部品の入力制約を充足するか否かを検査する検査ステップと、
前記第２の部品の入力制約が充足されないとき、（１）前記第２の部品の入力制約を充足する出力アクション列が取得されるように前記第３記憶部における前記第１の部品の入力制約を強化し、または、（２）前記第１の部品に対応する出力アクション列が充足されるように前記第３記憶部における前記第２の部品の入力制約を緩和する、入力制約調整ステップと、
前記システムにおいて互いに接続される各部品対間のそれぞれを、前記部品対の一方および他方の部品に対応する出力アクション列が前記部品対の他方および一方の部品に対応する入力制約を充足するよう、整合させるように前記選択ステップ、前記検査ステップおよび前記入力制約調整ステップを制御する制御ステップと、
を備える。
【０００９】
本発明の一態様としてのコンピュータプログラムは、
対象システムを形成する複数の部品間の接続関係、および前記部品毎に前記部品に接続される他の部品または外部との間で入出力されるアクションの内容を記述したシステム仕様を第１記憶部に記憶する第１記憶ステップと、
前記部品毎に、入力アクションの発生による複数の状態間の遷移および前記遷移の際に発生する出力アクションを記述した動作仕様を第２記憶部に記憶する第２記憶ステップと、
前記部品毎に前記入力アクションの発生順序に関する入力制約を第３記憶部に記憶する第３記憶ステップと、
部品の入力制約を満たすように前記部品の動作仕様に示される遷移を網羅する状態遷移パスを特定し、前記状態遷移パスに対応する出力アクション列を取得するアクション列取得ステップと、
前記システムにおいて互いに接続される部品対を選択する選択ステップと、
前記部品対の一方または他方である第１の部品に対応する出力アクション列が前記部品対の他方または一方である第２の部品の入力制約を充足するか否かを検査する検査ステップと、
前記第２の部品の入力制約が充足されないとき、（１）前記第２の部品の入力制約を充足する出力アクション列が取得されるように前記第３記憶部における前記第１の部品の入力制約を強化し、または、（２）前記第１の部品に対応する出力アクション列が充足されるように前記第３記憶部における前記第２の部品の入力制約を緩和する、入力制約調整ステップと、
前記システムにおいて互いに接続される各部品対間のそれぞれを、前記部品対の一方および他方の部品に対応する出力アクション列が前記部品対の他方および一方の部品に対応する入力制約を充足するよう、整合させるように前記選択ステップ、前記検査ステップおよび前記入力制約調整ステップを制御する制御ステップと、
をコンピュータに実行させる。
【発明の効果】
【００１０】
本発明は、複数の部品から成るシステムを構築する場合において隣接する部品同士間の整合性を検証および調整することを可能となる。
【発明を実施するための最良の形態】
【００１１】
図１は本発明の実施形態としてのテスト容易化設計装置の構成を示すブロック図である。
【００１２】
このテスト容易化設計装置は、対象システムのシステム仕様１０１と、当該対象システムをなす複数の部品のそれぞれについての動作仕様を含む形式仕様１０２とを外部の記憶装置から読み出し、入力として受け取る。
【００１３】
図２はシステム仕様１０１に記述された対象システムの一例としてのクルーズコントロールシステムを示す構成図である。クルーズコントロールシステムは、クルーズ制御部 (Cruise Controller)５１とエンジン制御部５２ (Engine Controller)５２とブレーキ制御部(Brake Controller)５３とで構成される。
【００１４】
クルーズ制御部５１は、エンジン制御部５２より、エンジン起動(eon)、エンジン停止(eoff)、アクセルオン(accel)の各アクションを、またブレーキ制御部５３より、ブレーキオン(brakeon)、ブレーキオフ(brakeoff)の各アクションを受信する。クルーズ制御部５１は、受信（入力）されたアクションに基づき内部で計算を行ってスロットル値(Throttle)を外部に出力し、エンジン制御部５２に対しては、クルーズ開始(activate)、クルーズ停止(deactivate)アクションを出力する。またクルーズ制御部５１は、クルーズコントロールシステム外部より、クルーズ制御起動(Cruise)、クルーズ復帰(Resume)、クルーズ設定解除(RDS)アクションを受信する。
【００１５】
エンジン制御部５２は、クルーズコントロールシステム外部より、エンジン起動(EngineOn)、エンジン停止(EngineOff)、アクセルオン(AccelOn)の各アクションを受信して、内部で計算を行い、クルーズ制御部５１に対してエンジン起動(eon)、エンジン停止(eoff)、アクセルオン(accel)の各アクションを出力する。
【００１６】
ブレーキ制御部５３は、クルーズコントロールシステム外部よりブレーキの押下(BrakePushed)、ブレーキ開放(BrakeRelease)の各アクションを受信し、クルーズ制御部５１に対してブレーキオン(brakeon)、ブレーキオフ(brakeoff)の各アクションを出力する。
【００１７】
図３はクルーズ制御部５１の動作仕様を状態遷移表形式で表したものである。
【００１８】
クルーズ制御部５１は、ローカル変数tgtSpeedSet={true,false}(tgtSpeedSetは値trueまたはfalseを取る)をもち、ローカル変数の初期値はtgtSpeedSet=falseであるとする。
【００１９】
クルーズ制御部５１の初期状態はstate=IdolModeであり、クルーズ制御部５１は、初期状態以外に、以下の５種類の状態(state)をもつ。
IdolMode, InitialMode, AccingMode, CruiseMode, CruiseOffMode,
【００２０】
"出力アクション"は、外部モジュール（エンジン制御部５２）への出力アクション activate, deactivateと、ローカル変数tgtSpeedSetへの値の設定とを含む。
【００２１】
クルーズ制御部５１は、図３の状態遷移表として記載された動作仕様に従い、外部からの入力アクションに応じて状態の遷移を行い、遷移に応じてアクションを出力する。図３の状態遷移表では、状態遷移の仕様を
＜元状態、ガード条件、入力アクション、出力アクション、次状態＞
の組合せにより表現している。state="元状態"であるときに、"ガード条件"が成立し
かつ"入力アクション"が発生すれば、"出力アクション"を出力し、"次状態"に遷移する。
【００２２】
例えば、クルーズ制御部５１がAccingMode状態であり、かつローカル変数tgtSpeedSetの値がtrueであるときに、Resumeアクションを受信したならば、activateアクションを外部（エンジン制御部５２）に出力して、CruiseMode状態に遷移する。
【００２３】
クルーズ制御部５１と同様に、エンジン制御部５２の動作仕様を表す状態遷移表を図５に、ブレーキ制御部５３の動作仕様を表す状態遷移表を図６に示す。
【００２４】
なお、本発明が取り扱う動作仕様の表現形式は、状態遷移表形式に限定されるものではなく、本発明は、状態遷移表と同等の表現能力をもつ形式を全て対象とする。例えば、図４は、図３の状態遷移表（動作仕様）を、状態をノード、遷移をノード間のエッジとする遷移図形式で表現したものである。ノードには番号が0〜7までの番号が振ってある。状態(0,1,2,3,5)は、図３に示される各状態に一致する。状態4,6,7は、出力アクションを明示的に遷移表示するための便宜上追加された状態である。また“？”と“！”は入力アクションと出力アクションを区別するための記号であり、文字列の最後に“？”が付くアクションは入力アクション、“！”が付くアクションは出力アクションを示す。
【００２５】
＜入力制約抽出部１１＞
入力制約抽出部１１は、各部品の動作仕様から当該部品の入力制約を抽出する。入力制約抽出部１１は、形式仕様１０２に部品の入力制約が含まれているときは、形式仕様１０２から当該部品の入力制約を抽出する。
【００２６】
ここで部品の入力制約とは、部品の仕様における入力の間に成立する制約である。例えば、入力制約としては、入力変数の値の幅や、入力アクション間に成立するアクション出現順序の制約(req の後にackがくる等)がある。本実施形態で扱う入力制約は、主に入力アクション間の出現順序制約である。入力アクション間の出現順序の制約は、動作仕様が状態遷移表として与えられている場合は、状態遷移表から出力アクションを削除することによって得ることができる。例えば、入力制約抽出部１１は、図３の状態遷移表から出力アクションを削除することで、表１に示すような入力制約を得ることができる。なお動作仕様から抽出される入力制約と同一の入力制約を、動作仕様とは別個に形式仕様１０２に含めておき、これを抽出するようにしてもよい。また動作仕様から抽出される入力制約と異なる入力制約を形式仕様１０２に含め、これを抽出してもよい。
【表１】
2010128583.tif 000003
【００２７】
ここで事前条件を定義する。事前条件とは、状態遷移表において、入力アクションからみて遷移が可能な前状態のことである。例えば表１の状態遷移表において、brakeonアクションの事前条件は{CruiseOffMode,CruiseMode}である。
【００２８】
なお本発明における入力制約は、上述のように状態遷移表から出力アクションを削除して得られるもの、または事前条件として与えられるものに制限されるものではない。すなわち状態遷移表とは独立に入力アクションの順序を制限することも可能である。例えば入力アクションの出現順番を、正規表現や時相論理等の論理式により表現する等である。このような入力制約を形式仕様１０２に含めて、本装置に入力するようにしてもよい。
【００２９】
入力制約抽出部１１は、クルーズ制御部５１と同様にエンジン制御部５２およびブレーキ制御部５３についても入力制約を抽出する。エンジン制御部５２の動作仕様から抽出した入力制約の例を表２に示す。
【表２】
2010128583.tif 000004
【００３０】
表２の入力制約は、図５に示したエンジン制御部５２の状態遷移表から出力アクションを削除したものに対し、さらに別途形式仕様１０２に含めて与えられた入力制約を加味したものとなっている。当該別途の入力制約は、「NormalMode時の入力アクションにdeactiveを受け付けない」というものであり、図５に示したエンジン制御部５２の動作仕様から出力アクションを削除したものと比較すると、状態=NormalMode時に入力アクション=deactiveを受け付ける行が表２には欠けていることが理解される。これはdeactiveアクションの事前条件からNormalModeが削除されている（制約が強化されている）ことに対応する。
【００３１】
＜テストケース生成部１２＞
テストケース生成部（アクション列取得部、モデル生成部）１２は、部品の動作仕様と、当該部品の入力制約とから、モデル駆動テスト技術に基づき、複数の入力アクション列（個別テストケース）を生成する。
【００３２】
ここで、モデル駆動テスト(Model Driven Test)技術とは動作仕様をモデルと見立て、モデルからテストケースを生成する技術のことである。テストケース生成技術としてはたとえば非特許文献２のものを用いることができる。このテストケース生成技術の動作について簡単に説明すると以下の通りである。
【００３３】
動作仕様において、状態をノード、遷移をエッジと見立てると状態遷移表はグラフ（状態遷移機械モデル）になる。
【００３４】
生成されるテストケースは複数のアクション列からなるとともに、これらのアクション列に従って状態遷移機械モデルの遷移を実行したとき、遷移網羅率（実行された遷移/遷移図に含まれる全ての遷移 ×100）が100%になるような性質を持っている。遷移を全て実行するように初期状態から入力アクションの一筆書きの遷移パスを計算することにより、複数のアクション列を含むテストケースは得られる。
【００３５】
グラフ上で最短の一筆書きを計算するには、例えば中国人郵便配達人問題(Chinese Postman Problem)等のグラフ理論のアルゴリズムを用いる。一筆書き計算は対象となるグラフが強連結構造であることを前提にしているので、もともとの状態遷移表に対応するグラフ（状態遷移機械モデル）が強連結構造で無い場合には、強連結構造になるようにグラフに初期状態に戻るエッジを適切に追加する。
【００３６】
一旦一筆書きのパスが求まると、追加したエッジおよび初期状態に戻る遷移の箇所で一筆書きを分割する。これにより状態遷移系に対して遷移網羅率が100%となるような複数の入力アクション列を計算する。
【００３７】
図１２は、テストケース生成部１２の処理手順を示すフローチャートである。
【００３８】
まずステップＳ１１では、状態遷移表（動作仕様）と入力制約から状態遷移機械モデルを生成する。生成された状態遷移機械モデルは、入力制約に従って状態遷移表（動作仕様）に制限を加えた限定動作仕様ということもできる。テストケース生成部１２は、状態遷移機械モデルを生成するモデル生成部を備える。なおモデル生成部は、テストケース生成部１２だけでなく、後述する他の要素（たとえば品質仕様整合性検査部１５，入力制約計算部１６、緩和条件計算部１７、強化条件計算部１８、上位階層用品質仕様生成部２０、条件伝播部２２）が備えていても良い。
【００３９】
続いて同ステップＳ１１では、生成した状態遷移機械モデルに基づき、初期状態から開始して初期状態に戻る一筆書き遷移列である入力アクション列の集合を生成する。
【００４０】
次に、ステップＳ１２において、得られた複数の入力アクション列のそれぞれについて状態遷移機械モデルを辿ることで出力アクション列を得る。この出力アクション列を期待値と呼ぶ。
【００４１】
次に、ステップ１３において、各入力アクション列と、各入力アクション列のそれぞれから得られた期待値（出力アクション列）とを対応づけることにより、複数の個別テストケースを生成する。これら複数の個別テストケースの集合はテストケースに相当する。
【００４２】
以下本処理手順について具体的に示す。
【００４３】
ステップＳ１１では、まず状態遷移表と入力制約とから状態遷移機械モデルを生成する。状態遷移表と入力制約とから生成された状態遷移機械モデルはたとえば本発明の限定動作仕様に相当する。状態遷移機械モデルは、状態遷移表に基づき、入力制約に記載される入力アクションの制限に従って、正味の状態間の遷移を計算し、状態をノード、遷移をエッジと見立てて作成したグラフによる動作仕様である。正味の状態とは、状態とローカル変数との組のことである。なお入力制約が状態遷移表から抽出されたもののみであるときは状態遷移表のみから状態遷移機械モデルを生成してもよい。
【００４４】
図３のクルーズ制御部５１の状態遷移表では、状態(state)とローカル変数(tgtSpeedSet)の組合せ
<state tgtSpeedSet>
を正味の状態とし、正味の状態間の遷移を計算する。
【００４５】
ここで以下の説明で用いる状態遷移機械モデルにおいては、便宜上、出力アクションを明示的に図に表記する。このために、状態遷移表の“状態”として、出力アクション用の特別な、状態を追加し、状態と遷移関係とを拡張する。
【００４６】
すなわち、「元状態→（入力アクション/出力アクション）→遷移状態」
であった遷移関係を、
「元状態→（入力アクション）→出力アクション用状態→（出力アクション）→遷移先状態」のように拡張する。
【００４７】
なお、当然ながら、出力アクション用の特別の状態を追加することなく、通常通りに状態遷移機械モデルを生成することも可能である。
【００４８】
以上に基づき、テストケース生成部１２は、クルーズ制御部５１、エンジン制御部５２およびブレーキ制御部５３についてそれぞれ状態遷移機械モデルを生成する。
【００４９】
図７に、クルーズ制御部１２の状態遷移機械モデル(FSM1)を示す。
【００５０】
状態=OutActMode,OutDeactMode,OutDeactAccelModeの３つの状態が出力アクション用の状態として追加されている。
【００５１】
図８にエンジン制御部５２の状態遷移機械モデル(FSM2)を示す。
【００５２】
状態=OutEonMode,OutEoffMode,OutAccelCruiseMode,OutAccelNormalModeの４つの出力アクション用の状態が追加されている。
【００５３】
図９に、ブレーキ制御部５３の状態遷移機械モデル(FSM3)を示す。
【００５４】
続いて、同ステップＳ１１において、テストケース生成部１２は、状態遷移機械モデルに基づき、初期状態から開始して初期状態に戻る一筆書き遷移列を計算する。状態遷移機械モデルに含まれる全ての遷移を満足するように計算すると、結果として、初期状態から開始して初期状態に戻る一筆書き遷移列が複数得られる。本例では、上述した通り、状態遷移機械モデルが出力アクション用の特別な状態を含むため、この複数の遷移列はそれぞれ、入力アクション列と、出力アクション列（期待値）とを含む（したがって各遷移列はそれぞれ個別テストケースに相当する）。すなわち、本例では、出力アクションを明示的な遷移として表示するようにしているので、状態遷移機械モデルに基づき初期状態から開始して初期状態に戻る一筆書き遷移を計算すると、入力アクションと出力アクションが遷移順に混在したアクション列（個別テストケース）が得られる。このため本例ではステップＳ１１において上記ステップＳ１２、Ｓ１３が同時に行われることとなる。
【００５５】
下記の表３はクルーズ制御部５１について図７の状態遷移機械モデルから生成したテストケース（複数の個別テストケース）を示す。"TESTSEGMENT数字-CC"とは個別テストケースにつけた識別名称でありTESTSEGMENT0-CC〜TESTSEGMENT５-CCまでの６個の個別テストケースが示される。各個別テストケースでは、入力アクションと出力アクションが遷移順に混在している。各個別テストケースからそれぞれ出力アクション列を取り除いたものが入力アクション列に相当し、逆に入力アクション列を取り除いたものが出力アクション列に相当する。入力アクションと出力アクションが遷移順に混在した個別テストケースから、入力アクション列と出力アクション列とに分離し、これらを対応付けて管理したものを個別テストケースとして管理してもよい。
【００５６】
説明の便宜上、入力アクション列"TESTSEGMENT数字-CC"と称するときは、個別テストケース"TESTSEGMENT数字-CC"から出力アクション列を除いたものを指すこととする。全ての入力アクション列TESTSEGMENT0-CC〜TESTSEGMENT５-CCは、eon()で始まりeoff()で終了する。これら6個の入力アクション列に沿ってクルーズ制御部５１をテストし、出力アクションを確認すれば、遷移網羅率100%のテストの実行が保証されることになる。
【表３】
2010128583.tif 000005
2010128583.tif 000006
【００５７】
表４に、エンジン制御部５２の状態遷移機械モデル（図８参照）から生成されたテストケース（複数の個別テストケース）の例を示す。
【表４】
2010128583.tif 000007
【００５８】
＜品質仕様生成部１３＞
品質仕様生成部１３は、部品毎に、入力制約と動作仕様とテストケースとを対応づけた品質仕様を品質仕様DB１４に格納する。品質仕様DB１４は部品名をキー(Key)として品質情報を格納・参照できる。また品質仕様生成部１３は、本装置に入力されたシステム仕様１０１を記憶する。品質仕様生成部１３は、システム仕様を記憶する第１記憶部、動作仕様を記憶する第２記憶部、入力制約を記憶する第３記憶部、テストケースを記憶する第４記憶部を備える。
【００５９】
＜品質仕様整合性検査部１５＞
品質仕様整合性検査部（検査部、選択部）１５は、システム仕様１０１における部品間の接続関係から、互いに接続される部品同士の品質仕様を品質仕様DB１４から得て、部品同士間の品質仕様の整合性を検査する。品質仕様整合性検査部１５は、互いに接続される部品同士（部品対）を選択する選択部を備えている。部品同士間の整合性検査は、部品同士のうちの一方である第１の部品の、他方の部品である第２の部品に対する充足性検査と、第２の部品の第１の部品に対する充足性検査とを含む。第１の部品の第２の部品に対する充足性検査は、第１の部品のテストケースが第２の部品の入力制約を充足するか否かの検査であり、第２の部品の第１の部品に対する充足性検査は、第２の部品のテストケースが第１の部品の入力制約を充足するか否かの検査である。
【００６０】
本実施形態では、クルーズ制御部５１とエンジン制御部５２とが接続しているので、エンジン制御部５２のテストケースの、クルーズ制御部５１の入力制約に対する充足性、及び、逆にクルーズ制御部５１のテストケースの、エンジン制御部５２の入力制約に対する充足性をそれぞれ検査する。同様に、クルーズ制御部５１とブレーキ制御部５３とが接続しているので、ブレーキ制御部５３のテストケースの、クルーズ制御部５１の入力制約に対する充足性、及び、逆にクルーズ制御部５１のテストケースの、ブレーキ制御部５３の入力制約に対する充足性をそれぞれ検査する。
【００６１】
図１３は、品質仕様整合性検査部１５の処理手順を示すフローチャートである。このフローチャートでは、部品Ａと部品Ｂが接続しているとし、部品Ａの部品Ｂに対する充足性検査（部品Ａのテストケースが部品Ｂの入力制約を充足するか否かを検査）の手順を示している。部品Ｂの部品Ａに対する充足性検査の手順も同様にして行えばよい。
【００６２】
ステップＳ２１では、部品Ａのテストケースから、部品Ｂの入力（または部品Ｂとの入出力）に関係のあるアクション列Ｔを得る。
【００６３】
ステップＳ２２では、アクション列Ｔを、部品Ｂの入力制約（または部品Ｂの入力制約と動作仕様から得られる状態遷移機械モデル）に従って遷移させる。遷移の際、部品Ａ以外からの入力アクションに関しては、これを無視して遷移を行う。部品Ｂの入力制約（または部品Ｂの上記状態遷移機械モデル）により受理されないアクションがアクション列Ｔに発見されるまで遷移を続ける。
【００６４】
ステップＳ２３では、不整合が発見されたアクションに印(NG)をつける。
【００６５】
以下、具体例を示す。
【００６６】
まず、ステップＳ２１において、エンジン制御部５２のテストケース(TESTSEGMENT0-EC,1-EC)（表４参照）と、エンジン制御部５２に接続するクルーズ制御部５１の入力制約（表１）（または入力制約と動作仕様）とを品質仕様ＤＢ１４から読み込み、エンジン制御部５２のテストケースから、クルーズ制御部５１の入力（または入出力）に関係のあるアクション列Ｔを得る。エンジン制御部５２のテストケースTESTSEGMENT0-ECの例では、クルーズ制御部５１の入力に関係のあるアクション列Ｔを計算すると、
Ｔ＝“eon, accel, eoff”
を得る。
【００６７】
次に、ステップＳ２２において、アクション列Ｔを、クルーズ制御部５１の入力制約に沿って遷移させ、遷移のトレースを行う（図４参照）。遷移のトレースにおいては、クルーズ制御部５１と関係のない入力アクション（たとえばブレーキ制御部５３からクルーズ制御部５１への入力アクション）に関わる遷移があれば、これを補完（あるものとして）進むこととする。アクション列Ｔに従って遷移のトレースを行うと、最後のアクション=eoffのところで遷移先が見つからないのでＮＧ印をつける。遷移のトレースの結果を以下に示す。ここでXXXはエンジン制御には関係のないアクションを表している。
IdolMode→(eon)→InitialMode→(XXX)→CruiseOffMode→(accel)→AccingMode→ (XXX)→CruiseMode→(eoff)NG
【００６８】
なお、ステップＳ２１においてクルーズ制御部５１の入出力に関係のあるアクション列Ｔを計算すると、Ｔ＝“eon, accel, activate, eoff”となり、
続いて、ステップＳ２２においてアクション列Ｔを、クルーズ制御部５１の入力制約と動作仕様とから得られる状態遷移機械グラフに沿って遷移させると以下のトレース結果が得られる。
IdolMode→(eon)→InitialMode→(XXX)→CruiseOffMode→(accel)→AccingMode→ (activate)→CruiseMode→(eoff)NG
【００６９】
アクション列ＴにおけるＮＧを上記テストケースTESTSEGMENT1-ECに対応させると以下の表５に示すようになり、当該テストケースに不整合が存在することがわかる。
【表５】
2010128583.tif 000008
【００７０】
なお、本発明における整合性検査は上記説明内容に制限されるものではない。例えば、入力制約が時相論理式や正規表現に代表される論理式で記述される場合は、部品Aのテストケース（トレース列）と部品Bの入力制約との間で、トレース列の入力制約（論理式）に対する充足性検査等により、整合性検査を行うようにしてもよい。
【００７１】
＜入力制約計算部１６＞
入力制約計算部（入力制約調整部）１６は、品質仕様整合性検査部１５において互いに接続する部品同士間で不整合を検出した場合に、一方の部品の入力制約を強化することにより他方の部品との間の不整合を解消する。なお、テストケース生成技術においては、入力制約を強化するとテストケースが減少することにつながる。
【００７２】
図１４は入力制約計算部１６の処理手順を示すフローチャートである。
【００７３】
ステップＳ３１では、個々の個別テストケースに対して不整合状態(NG)が起こるＮＧアクションを記録する（表５参照）。
【００７４】
ステップＳ３２では、NGアクションが記録された個別テストケースに含まれるアクション列に従って、入力制約と動作仕様から生成される状態遷移機械モデルの初期状態から遷移を起こさせ、NGアクションに至る遷移を特定し、状態遷移機械モデル上の該当するＮＧ遷移ポイント（状態、アクション）を記録する。ＮＧ遷移ポイントのアクションは基本的に上記ＮＧアクションであり、状態はＮＧアクションの前状態である。ただし状態遷移機械モデルが出力アクション用の状態を含むものであり、かつ、ＮＧアクションの前状態が、出力アクション用の状態であるときは、ＮＧアクションに対して遷移をさかのぼり、最初に見つかる非出力アクション用の状態およびアクションを特定し、特定した状態およびアクションの組をＮＧ遷移ポイントとする。
【００７５】
ステップＳ３３では、見つかった全てのＮＧ遷移ポイント（状態s1、アクションa1）について、アクションa1に対する事前条件から状態s1を削除するように入力制約を修正する。
【００７６】
ステップＳ３４では、修正された入力制約と、動作仕様とから状態遷移機械モデルを再生成し、再生成した状態遷移機械モデルに対して再度、テストケース生成を行い、不整合が無くなったかどうかを検査する。新たな不整合が見つかれば（Ｓ３５のＹＥＳ）ステップＳ３１からの手順を繰り返す。ステップＳ３１〜Ｓ３４を不整合が無くなるまで（Ｓ３５のＮＯ）繰り返す。
【００７７】
ステップＳ３６では、最終的に得られた、入力制約およびテストケースを品質仕様更新部１９に渡す。品質仕様更新部１９では、受け取ったデータを元に品質仕様DB１４の内容を更新する。
【００７８】
以下具体例を示す。
【００７９】
本実施形態では、エンジン制御部５２から得られた個別テストケースの不整合（表５の不整合１）を解消する。すなわちクルーズ制御部５１への入力に対して不整合な個別テストケースが生成されないように、エンジン制御部５２側の入力制約を修正する。
【００８０】
まず、ステップＳ３１で、表５の不整合1を解消するために、表５のＮＧアクションを記録する。
【００８１】
次に、ステップＳ３２において、表５の個別テストケース(TESTSEGMENT1-EC)を、エンジン制御部５２の状態遷移機械モデル（図８参照）を辿って、順に遷移させると、図１０に示すように、ＮＧアクションに至る遷移が見つかる。
【００８２】
図１０では状態=OutEoffModeであるときにeoff()出力アクションを出力する箇所がＮＧポイントとして得られる。ただし状態=OutEoffModeは出力アクション用の状態であるため、非出力アクション用の状態に達するまで遷移を逆に辿り、これにより状態= CruiseModeのときに外部からEngineOffアクションが呼ばれることが不整合の原因であることが判明する。
【００８３】
そこで、(状態,アクション)=(CruiseMode, EngineOff)
をNG遷移ポイントとして記憶する。
【００８４】
次にステップＳ３３では、記憶されたＮＧ遷移ポイントに対応する状態を、ＮＧ遷移ポイントに示されるアクションの事前条件から削除する。エンジン制御部５２の入力制約（表２参照）によると、EnginOffの事前条件は{NormalMode,CruiseMode}の２つである。ここではＮＧ遷移ポイントに対応する事前条件=CruiseModeを{NormalMode,CruiseMode}から削除するように入力制約を修正する。
【００８５】
この事前条件の削除は、表２の入力制約では、
行＝「CruiseMode,-,EngineOff,IdolMode」
の削除に対応する。
【００８６】
次にステップＳ３４では、修正された入力制約と、動作仕様に基づき、状態遷移機械モデルを再生成し、再生成された状態遷移機械モデルからテストケースを生成する。これにより、表６に示すようなテストケース（１つの個別テストケース）が得られる。
【表６】
2010128583.tif 000009
【００８７】
クルーズ制御部５１の入力制約に対する充足性を検査すると（Ｓ３５）、今度はＮＧとなるアクションが含まれず、よって、不整合1が解消されていることがわかる（ＹＥＳ）。
【００８８】
ステップＳ３６では、修正された入力制約と、修正されたテストケース（表６）を品質仕様更新部１９に渡す。品質仕様更新部１９では、渡されたデータを元に品質仕様DB１４の内容を更新する。
【００８９】
＜緩和条件計算部１７＞
緩和条件計算部（入力制約調整部）１７は、品質仕様整合性検査部１５において互いに接続する部品同士間で品質仕様の間に不整合が検出した場合に、一方の部品である第１の部品のテストケースが充足されるように他方の部品である第２の部品の入力制約を緩和することによりこれらの部品の間の不整合を解消する。なお、テストケース生成技術においては、入力制約を緩和するとテストケースが増えることにつながる。
【００９０】
図１５は、緩和条件計算部１７の処理手順を示すフローチャートである。このフローチャートでは、前段の品質仕様整合性検査部１５で部品Aのテストケースが、部品Aと接続する部品Bの入力制約を充足しないことにより部品Ａ，Ｂ間に不整合が検出された場合の緩和条件計算部１７の処理を示す。
【００９１】
ステップＳ４１では部品AのテストケースTにおける各個別テストケースから、部品Bの入力（または入出力）に関わる部分列Cをそれぞれ得る。
【００９２】
ステップＳ４２では部分列Cに従って、部品Bの入力制約または、部品Ｂの入力制約および動作仕様から得られる状態遷移機械モデルに対して、初期状態を起点として遷移を起こさせる
ステップＳ４３では、遷移できない入力アクションEに到達まで部分列Ｃの遷移を続け、遷移できない入力アクションＥの元状態Fを記録する。あるいは、入力アクションＥの直前のアクションの遷移先状態を記録する。
【００９３】
ステップＳ４４では、部品Ｂの状態遷移表で状態Fのときに、当該アクションＥに対して遷移可能かどうかを調べる。遷移可能でないならば（ＮＯ）、条件の緩和は出来ないことを表示し処理を終了する。遷移可能であるならば（ＹＥＳ）、部品Ｂの状態遷移表で遷移先の状態Ｄを取得する（Ｓ４５）。
【００９４】
ステップＳ４６では、入力アクションEに対する事前条件に状態Fを追加するように部品Ｂの入力制約を修正する。この際、状態Ｆの遷移先は、上記状態Dに設定する。この後、緩和された入力制約と、当該入力制約を反映した状態遷移機械モデルから得られるテストケースとを品質仕様更新部１９へ渡し、品質仕様更新部１９は受け取ったデータに基づき品質仕様ＤＢ１４を更新する。
【００９５】
以下具体例を示す。ここではクルーズ制御部５１のテストケース(表３)における個別テストケースTESTSEGMENT0-CCを例題とする。この個別テストケースTESTSEGMENT0-CCを別途、表７に示す。
【表７】
2010128583.tif 000010
【００９６】
まず前段の品質仕様整合性検査部１５で表7の個別テストケースと、エンジン制御部５２の状態遷移機械モデル（表２の入力制約と、動作仕様に基づいて生成されたもの）との整合性を検査しており、deactivate()を呼ぶ箇所で、該当する遷移がエンジン制御部５２の状態遷移表に遷移がないため、このアクションがＮＧアクションであることが検出されているとする。すなわち、以下のように、品質仕様整合性検査部１５で不整合２（表8）が得られているとする。
【表８】
2010128583.tif 000011
【００９７】
ステップＳ４１では、この個別テストケースから、エンジン制御部５２の入出力に係わる部分列eon(), deactivate(), eoff()を得る。
【００９８】
ステップＳ４２、Ｓ４３では、図８に示したエンジン制御部５２の状態遷移機械モデル（状態遷移表（図５）と入力制約（表２）から生成されたもの）を、上記部分列（eon(), deactivate(), eoff()）のアクションを順を追ってトレースすると、状態=NormalModeにてアクション"deactive"が遷移できないことがわかる。したがって、元状態＝NormalModeを記録する。アクション"deactive"は、上記アクションＥに相当する。
【００９９】
ステップＳ４４では、エンジン制御部５２の状態遷移表（図５）では、状態=NormalModeにてアクションdeactiveに対する遷移が存在するかどうかを検査し、ここでは存在するため、遷移先であるNormalModeを得る（Ｓ４５）。この状態NormalModeは状態Ｄに相当する。
【０１００】
ステップＳ４６では、アクションdeactivate()に対する事前条件である状態={CruiseMode}に対してNormalModeを追加するように入力制約（表２）を修正する。すなわち入力制約（表２）に以下の新たな遷移を追加する。遷移先としてはステップＳ４５で得られた状態Ｄ=NormalModeを入れる。
追加される遷移＝「NormalMode, -, deactivate, -, NormalMode!」
【０１０１】
上記処理により修正（緩和）された入力制約を表９に示す。下から４行目に遷移が追加されている。
【表９】
2010128583.tif 000012
【０１０２】
品質仕様整合性検査部１５においてクルーズ制御部５１のテストケース（表7）は、修正されたエンジン制御部５２の入力制約（表9）に整合するため（該テストケースにおけるエンジン制御部５２の入力に係わるアクションdeactiveの前状態であるNormalModeに、エンジン制御と関係のない入力アクションを補完して初期状態から到達可能である）、上記「不整合２」が解消されたことが分かる。
【０１０３】
＜強化条件計算部１８＞
強化条件計算部（入力制約強化部）１８は、品質仕様整合性検査部１５において不整合が検出されない部品同士に関し、一方の部品の入力制約を、他方の部品のテストケースが充足される範囲において、強化する（すなわち一方の部品の動作仕様に含まれる遷移を抑制するように一方の部品の入力制約を強化修正する）。なお、入力制約を強化するという点で強化条件計算部１８の処理は、入力制約計算部１６の処理と同様であるが、処理を行う状況が、後者が不整合が検出された場合であるのに対し、前者がそうでない場合である点において異なっている。
【０１０４】
図１６は、強化条件計算部１８の処理手順を示すフローチャートである。前段の品質仕様整合性検査部１５では、部品Aの動作トレース（テストケース）が、部品Aと接続する部品Bの入力制約を満足することにより、不整合が検出されなかった場合の強化条件計算部１８の処理を示す。
【０１０５】
ステップＳ５１では、部品AのテストケースTにおける各個別テストケースから、部品Bの入力に関わる部分列Cを得る。
【０１０６】
ステップＳ５２では、部品Bの入力制約φ_Bを強化し、部分列Cに対して入力制約φ_Bの充足性を計算する。本ステップＳ５２の詳細手順の一例を以下に［Ｓ５２−１］〜［Ｓ５２−４］として示す。ここでは、入力制約φ_Bは、部品Bの動作仕様から生成される状態遷移機械モデルを入力アクションの受理不受理を判定するオートマトンとして用いる。
［Ｓ５２−１］部品Bの入力制約φ_Bから状態遷移機械モデルM_Bを生成する。
［Ｓ５２−２］部品ＡのテストケースTにおける各個別テストケースを状態遷移機械モデルM_Bに受理させる。
［Ｓ５２−３］状態遷移機械モデルM_Bで実行されなかった遷移と状態を除去して新たな状態機械遷移モデルM_B'を得る
［Ｓ５２−４］新たな状態遷移機械モデルM_B'を入力制約φ＿Ｂに反映させることにより、入力制約φ＿Ｂから不要な事前条件を削除する。すなわち、入力制約φ＿Ｂを強化する。
【０１０７】
ステップＳ５３では、充足性が保証される間は（ＹＥＳ）、ステップＳ５２の入力制約φ_Bの強化を繰り返し、充足性が保証されなくなったら（ＮＯ）ステップＳ５４へ進む。
【０１０８】
ステップＳ５４では、充足性が保証される最強の入力制約φ_Bを、強化条件として取得する。この後、取得された最強の入力制約φ_Bと、動作仕様とから得られる状態遷移機械モデルから生成されるテストケースと、当該最強の入力制約φ_Bを、品質仕様更新部１９に送り、品質仕様更新部１９では受け取ったデータに基づき品質仕様ＤＢ１４を更新する。
【０１０９】
以下強化条件計算部１８の処理の具体例を示す。
【０１１０】
ここでは、前提としてクルーズ制御部５１に関する入力制約は、表１の入力制約から
行＝「CruiseOffMode、-、brakeon、InitialMode 」
を削除したものであるとし、またエンジン制御部５２に関する入力制約は、＜条件緩和部１７＞の説明で示した、修正された入力制約（表9）であるとして説明を行う。
【０１１１】
ステップＳ５１では、上記のように行＝「CruiseOffMode、-、brakeon、InitialMode 」が削除された入力制約と、動作仕様とから得られる状態遷移機械モデルに従って、クルーズ制御部５１のテストケースを計算すると、６つの個別テストケース（アクション列）TESTSEGMENT0-CC〜TESTSEGMENT5-CCを得る。各アクション列TESTSEGMENT0-CC〜TESTSEGMENT5-CCからエンジン制御部５２の入力に係わる出力アクションのみをそれぞれ抽出すると以下の部分列TESTSEGMENT1-CC、TESTSEGMENT3-CC、TESTSEGMENT4-CC〜TESTSEGMENT5-CCを得る。ただし、アクション列TESTSEGMENT0-CCと、TESTSEGMENT2-CCについては、エンジン制御部５２の入力に係わる出力アクションは含まれなかったため、表記を省略する。
【表１０】
2010128583.tif 000013
【０１１２】
ステップＳ５２では、表9の入力制約と、動作仕様とに基づく状態遷移機械モデルに対して、表10に示される各部分列をそれぞれ遷移させる。より詳細には、クルーズ制御部５１からの出力アクション（すなわちエンジン制御部５２への入力アクション）に限定した入力制約を以下の表11のように抽出し、表11の入力制約に従って、表10の各部分列を遷移させる。
【表１１】
2010128583.tif 000014
【０１１３】
表11の入力制約に対して、表10の各部分列を遷移させると、前状態= 0のときにdeactivateが呼ばれる遷移が余分である（実行されなかった）ことがわかる。そこで、この遷移をもともとの入力制約（表9）より削除する。
【０１１４】
該当する遷移は以下の行である。
「NormalMode,-, deactive, NormalMode」
このようにして、不要な入力制約を削除して条件強化を行うことができる。
【０１１５】
＜品質仕様更新部１９＞
品質仕様更新部１９は、既に説明した通り、入力制約計算部１６、緩和条件計算部１７、強化条件計算部１８で修正された入力制約と、この修正された入力制約と動作仕様とに基づく状態遷移機械モデルから生成されたテストケースとに基づき、品質仕様DB１４の内容を更新する。
【０１１６】
＜上位階層用品質仕様計算部２０＞
上位階層用品質仕様計算部（制御部）２０は、下位の部品を組合せた上位階層部品（以下単に上位階層と称する）の品質仕様を、下位の部品の品質仕様に基づき計算する。たとえば図２のクルーズコントロールシステムでは、クルーズ制御部５１、エンジン制御部５２およびブレーキ制御部５３の３つの部品（下位部品）が組み合わせられてクルーズコントロールシステムという上位階層が形成されており、上位階層用品質仕様計算部２０は、これら３つの部品の品質仕様から、クルーズコントロールシステムの品質仕様を計算する。
【０１１７】
図１７は、上位階層用品質仕様計算部２０の処理手順を示すフローチャートである。
【０１１８】
ステップＳ６１では、上位階層Xに含まれる下位部品の品質仕様を品質仕様DB１４より得る。
【０１１９】
ステップＳ６２では、上位階層Xに含まれる部品Z_0を１つ選択する。
【０１２０】
ステップＳ６３では、部品Z_0に接続する部品Z_0_i(i=0,...,n)を特定する。
【０１２１】
ステップＳ６４では、部品Z_0と部品Z_0_i(i=0,...n)のそれぞれとの間で品質仕様の整合性を検査し、不整合が発見された場合は、入力制約計算あるいは緩和条件計算を行うことにより不整合を解消する。上位階層用品質仕様計算部２０は、互いに接続される部品群、または互いに接続される部品対、またはこれらの両方を選択する選択部を備えていている。
【０１２２】
ステップＳ６５では、各部品Z_0_iにおいて２つの部品間に接続があるかどうかを検査し、接続がある場合にはステップＳ６４と同様にして、整合性の検査と、不整合の解消とを行う。
【０１２３】
ステップＳ６６では、部品Z_0_iについて逐次的(i=0からnまで順番に)に状態遷移機械モデル（入力制約と動作仕様とから生成される）の直積を計算し、これにより、部品Z_0_i(i=0,...,n)を合わせた部品集合Z_1についての動作仕様（状態遷移機械モデル）を得る。これを式によって示すと以下の通りである。(X)は直積を表す記号である。またR_0_i(i=0,..,n)は計算の便宜のための中間変数である。
R_0_0= Z_0_0
R_0_i = R_0_{i-1}  (X) Z_0_i,  (i=1,...n)
Z_1 = R_0_n
【０１２４】
ステップＳ６７では、部品集合Z_1と部品Z_0との間で整合性を検査し、不整合が発見された場合は、不整合の解消を行う。なお整合性の検査の際、部品集合Z_1の入力制約は、ステップＳ６６で得た動作仕様（状態遷移機械モデル）から抽出することによって得られる。
【０１２５】
ステップＳ６８では、部品集合Z_1と部品Z_0とを合わせた上位階層Z_2の動作仕様を計算し、動作仕様から入力制約を抽出する。
【０１２６】
ステップＳ６９では、上位階層Z_2に接続する部品が存在するかどうかを検査し、存在しない場合（全ての部品に対する操作を行った場合）は（ＮＯ）、上位階層Z_2の動作仕様を上位階層Xの動作仕様、上位階層Z_2の入力制約を上位階層Xの入力制約とする（Ｓ７１）。そして該上位階層Ｘの動作仕様および入力制約を、これらに基づく状態遷移機械グラフから得られるテストケースと対応付けて、上位階層用品質仕様として、品質仕様DB１４に登録する（Ｓ７１）。上位階層Z_2と接続する部品が存在する場合は（ＹＥＳ）、上位階層Z_2と接続する部品Z_2_i(i=0,...,m)を取得し（Ｓ７０）、ステップＳ６４以降の各ステップを繰り返す。
【０１２７】
以下、上位階層用品質仕様計算部２０の処理の具体例を示す。
【０１２８】
本実施形態では、図２のようにクルーズ制御部５１が、エンジン制御部５２とブレーキ制御部５３とそれぞれ接続され、上位階層としてのクルーズコントロールシステムが構成されている。
【０１２９】
ステップＳ６１では、クルーズコントロールシステムを上位階層Xとして選択し、上位階層Xに含まれる各部品（下位部品）の品質仕様を品質仕様DB１４から得る。
【０１３０】
ステップＳ６２では、上位階層Xに含まれる部品Z0として、クルーズ制御部５１を選択する。
【０１３１】
ステップＳ６３では、クルーズ制御部５１と接続される部品として、エンジン制御部５２、ブレーキ制御部５３を取得する。すなわち部品Z_0_i(i=0,1)を得る。部品Z_0_0はエンジン制御部５２、部品Z_0_1はブレーキ制御部５３であるとする。
【０１３２】
ステップＳ６４では、ブレーキ制御部５３（部品Z_0_1）とクルーズ制御部５１（部品Z0）との間の整合性、及びエンジン制御部５２（部品Z_0_0）とクルーズ制御部５１（部品Z0）との間の整合性を、品質仕様整合性検査部１５により検査する。不整合が発見されれば入力制約計算部１６および緩和条件計算部１７によりその不整合を解消する。この処理は既に説明した通りであるため説明を省略する。
【０１３３】
ステップＳ６５では、エンジン制御部５２（部品Z_0_0）とブレーキ制御部５３（部品Z_0_1）とが接続されているか否かを確認し、ここでは接続されていない（すなわち互いに独立して動作する）判断し、ステップＳ６６に進む。
【０１３４】
ステップＳ６６では、エンジン制御部５２（部品Z_0_0）のFSM2とブレーキ制御部５３（部品Z_0_1）のFSM3との直積を計算する。これによりエンジン制御部５２（部品Z_0_0）とブレーキ制御部５３（部品Z_0_1）とを合わせた部品集合Z_1の状態遷移機械モデルFSM4を得る。
【０１３５】
図１１は、状態遷移機械モデルFSM4の動作を状態遷移表（エンジン制御部×ブレーキ制御部）の形式で表したものである。
【０１３６】
状態遷移機械モデルFSM4の状態は、エンジン制御部５２とブレーキ制御部５３の状態の組合せ（エンジン制御部５２の状態、ブレーキ制御部５３の状態）である。表記の簡単のため状態名は略記されている。すなわちエンジン制御部５２の状態に関しては、（I:IdolMode, N:NormalMode, C:CruiseMode）に従って略記され、ブレーキ制御部５３の状態に関しては、(ON:BrakeOnMode,OFF:BrakeOffMode)に従って略記されている。
【０１３７】
以下の表12は、図１１の状態遷移表より抽出した入力制約を表す。
【表１２】
2010128583.tif 000015
【０１３８】
ステップＳ６７では、部品集合Z_1（エンジン制御部５２およびブレーキ制御部５３）と、部品Z_0（クルーズ制御部５１）との間で整合性を検査する。
【０１３９】
表13は、テストケース生成部１２により状態遷移機械モデルFSM4から生成したテストケースを示す。このテストケースは複数の個別テストケースを含み、各個別テストケースはそれぞれ入力アクションと出力アクション（期待値）とからなる。
【表１３】
2010128583.tif 000016
【０１４０】
表13のテストケースに含まれる各個別テストケースを、クルーズ制御部５１の入力制約（表１）と比較することにより、表13のTESTSEGMENT0-ＢＥについて、以下のＮＧアクションが特定される。すなわち、３番目のアクションであるactivate()がＮＧアクションとして特定される。
TESTSEGMENT0-ＢＥ
ebc0.EngineOn()
ebc0.eon()
ebc0.activate()        ＮＧアクション
ebc0.BrakeReleased()
ebc0.brakeoff()
ebc0.AccelOn()
………………. 以下略
【０１４１】
不整合が発見されたため、この不整合の解消を行う。ここでは入力制約計算部１６を用いて不整合を解消する例を示す。上記NGアクションの前状態は(N,ON)であるので、activateアクションの事前条件から(N,ON)を削除するように、上記表12に示した、FSM４の入力制約を修正する。
【０１４２】
修正された入力制約と、動作仕様から生成されるFSM４から再度、テストケース生成部１２を用いてテストケース生成を行うと以下のテストケースを得る。
TESTSEGMENT0-ＥＢ
ebc0.EngineOn()
ebc0.eon()
ebc0.AccelOn()  ＮＧアクション
ebc0.accel()
ebc0.BrakeReleased()
ebc0.brakeoff()
ebc0.activate()
ebc0.BrakePushed()
ebc0.brakeon()
ebc0.AccelOn()
ebc0.accel()
ebc0.BrakeReleased()
ebc0.brakeoff()
ebc0.deactivate()
ebc0.AccelOn()
ebc0.accel()
ebc0.activate()
ebc0.AccelOn()
……………………..以下略
【０１４３】
４番目のaccelアクションが最初にＮＧアクションとして特定されるが、accelは出力アクションであるので、テストケースを前方に辿って、直前のAccelOnアクションが実際のＮＧアクションとなる。このときの元状態は(N,ON)であるので、AccelOnアクションの事前条件から(N,ON)を削除するように、入力制約を再度修正する。
【０１４４】
このように、入力制約の修正、テストケースの生成、クルーズ制御部５１の入力制約に対する充足性検査を、整合性が確保されるまで繰り返し行う。また同様にして、部品集合Z_1（エンジン制御部５２およびブレーキ制御部５３）の入力制約に対する部品Z_0（クルーズ制御部５１）のテストケースの充足性検査についても同様に整合性が確保されるまで繰り返し行う。このようにして最終的に表14に示すような入力制約を得る。
【表１４】
2010128583.tif 000017
【０１４５】
ここで、入力アクションAccelOnに着目すると、事前条件が{(N,OFF),(C,OFF)}に絞り込まれていることがわかる。これはAccelOnアクションは、ブレーキがOFFのとき（すなわちBrakeReleasedアクションの後に）に、外部から呼ばれなくてはならないという、入力制約が新たに発生していることを表している。
【０１４６】
すなわち、FSM２とFSM３を組合せたFSM４と、クルーズ制御部５１の入力制約とを付き合わせることにより、本来は独立並行動作のためにお互いに順序制約がなかった、BrakeReleasedアクションと、AccelOnアクションの間に、新たな順序制約が得られることがわかる。
【０１４７】
FSM4の出力制約である制約１を、FSM4の入力制約に読みかえると以下の制約２が得られる。
"AccelOnは必ずBrakeReleasedが呼ばれてBrakePushedが呼ばれる前に呼ばれる"（制約２）
【０１４８】
ステップＳ６８では、部品集合Z_1と部品Z_0を組み合わせた上位階層Z2の動作仕様と入力制約を計算する。
【０１４９】
ここでは、ステップＳ６７にてFSM4とクルーズ制御部５１の入力制約との間の不整合が解消された後における、FSM4とクルーズ制御部５１の動作仕様（FSM）から、部品集合Z_1と部品Z_0を組み合わせた上位階層Z2の動作仕様を計算する。この計算では、部品集合Z1と部品Z0との間で入出力されるアクションに関して、空振り（片方から出力される時に、もう片方が入力可能状態にない）が生じないように、動作の組合せを計算する。最初に部品集合Z1および部品Z0のFSMの直積を計算し、計算された直積から空振りが発生する状態Sを特定し、Sに到達可能な遷移を逆に辿って、Sに到達可能な遷移を枝狩りする。この詳細な手順についてはたとえば特許文献２のcomposition演算の説明に記載されている。このようにFSMが得られたら、このFSMに対応する動作仕様を取得するとともに、この動作仕様から入力制約を抽出する。
【０１５０】
ステップＳ６９では、上位階層Z2に接続される部品は存在しないと判断し（ＮＯ）、ステップＳ６８で得た動作仕様および入力制約を、上位階層Ｘ＝クルーズコントロールシステムの動作仕様および入力制約として、この動作仕様（および入力制約）に基づくテストケースとともに品質仕様DB１４に登録する（Ｓ７１）。
【０１５１】
このようにして、下位階層の部品の品質仕様（入力制約、動作仕様、テストケース）が与えられたこれらを組み合わせて、上位階層の品質仕様を計算することができる。
【０１５２】
＜条件伝播部２２＞
条件伝播部（制御部）２２は、システム仕様１０１に記述される部品の接続関係に従い、品質仕様品質仕様整合性検査部１５、入力制約計算部１６、緩和条件計算部１７、強化条件計算部１８、上位階層用品質仕様計算部２０等を用いて、システム全体で品質仕様の整合性を確保する。
【０１５３】
図１８は、条件伝播部２２の処理手順を示すフローチャートである。以下では本処理手順について図１９に示すシステムを例として説明を行う。
【０１５４】
ステップＳ８１では、条件伝播の対象とする範囲Xを指定する。ここでは図１９のように部品A,B,C,D,E,Fを含む範囲を指定する。
【０１５５】
ステップＳ８２では、指定した範囲Xに含まれる部品の集合Sを得る。ここでは、S={A,B,C,D,E,F}を得る。
【０１５６】
ステップＳ８３では、集合Sから任意の部品p∈Sを選択し、部品pと、部品pに接続する下位部品とからなる部分集合S’⊆Sを得る。ここでは、S={A,B,C,D,E,F}の中の部品Bを選択し、部品Bと、部品Bに接続関係のある下位部品Aとからなる部分集合S’={A,B}を得る。
【０１５７】
ステップＳ８４では、部分集合S’に対して上位階層用品質仕様計算部２０により上位階層用品質仕様計算を行い、これにより部分集合S’に対応する上位階層Zの品質仕様（動作仕様と入力制約とテストケース）を計算する。ここでは部分集合S’ ={A,B}に対応する上位階層（ここではABと命名する）の品質仕様を計算する。
【０１５８】
ステップＳ８５では、S =(S - S’)∩{Z}とし、ステップＳ８３〜Ｓ８５を、集合Sに含まれる要素数が１つになるまで繰り返す（Ｓ８６のＮＯ）。ここではS={AB,C,D,E,F}であり、以降、１回目の繰り返しのステップＳ８３では、S’={AB,C,D}を取得し、続くステップＳ８４において、S’に対応する上位階層（ここではABCDと命名する）の品質仕様を計算し、続くステップＳ８５においてS={ABCD,E,F}を得る。同様にして、２回目の繰り返しのステップＳ８３では、S’={ABCD,E,F}を取得し、続くステップＳ８４においてS’に対応する上位階層ABCDEFの品質仕様を計算し、続くステップＳ８５においてS={ABCDEF}を得る。集合Sに含まれる要素数が１つであるため（Ｓ８６のＹＥＳ）、本処理を終了する。
【０１５９】
＜テスト容易化指標計算部２１＞
テスト容易化指標計算部２１は、対象システムを構成する各部品の品質仕様と、部品間の接続情報を記述したシステム仕様１０１から、各接続される部品間についてテスト容易化指標を計算する。テスト容易化指標は品質仕様整合性検査部１５の整合性計算の結果に基づいて算出され、２つの部品をＡ、Ｂとすると、以下のように(">","=","<")の３種類存在する。表15では互いに接続される部品Ａ、Ｂについて、部品Ａのテストケースと部品Ｂの入力制約とを対象にした場合のテスト容易化指標の例が示される。部品Ｂのテストケースと部品Ａの入力制約とを対象にした場合は、表15におけるテスト容易化指標の各種類の定義説明をＡとＢとを入れ替えて読めばよい。
【表１５】
2010128583.tif 000018
【０１６０】
テスト容易化指標計算部２１は、各接続される部品間について求めたテスト容易化指標を種類別に集計して、表示または出力する。集計結果はたとえば以下のような形式で表示または出力される。
【表１６】
2010128583.tif 000019
【０１６１】
これによりユーザはシステム全体でのテスト容易化指標の割合を確認することできる。たとえば条件伝播部２２の前にテスト容易化指標計算部２１による処理を行い、その結果、A">"Bが存在しなければ、条件伝播部２２による処理を省略することもできる。あるいはテスト容易化指標計算部２１は、条件伝播部２２からの要請に応じて、要請された範囲に含まれる部品について処理を行って処理結果を応答し、条件伝播部２２は、受け取った処理結果を利用して処理を進めるようにしてもよい。たとえばA">"Bが存在しなくなれば当該範囲について不整合は無くなったと判断するようにしてもよい。
【０１６２】
テスト容易化指標計算部２１の処理手順では、まず［１］対象システムにおいて接続する部品間のテスト容易化指標（">","=","<")を計算する。［２］次に、求めたテスト容易化指標を種類別に集計し、集計した結果を出力または表示する。
【０１６３】
以下テスト容易化指標計算部２１の処理手順について、図２のクルーズコントロールシステムを例にして説明を行う。クルーズ制御部５１の動作仕様が図３の状態遷移表、エンジン制御部５２の動作仕様が図５の状態遷移表、ブレーキ制御部５３の動作仕様が図６の状態遷移表で与えられているとする。
【０１６４】
手順［１］において、＜品質仕様整合性検査部１５＞で説明したように、クルーズ制御部５１とエンジン制御部５２の間ではクルーズ制御部５１のテストケースの中にエンジン制御部５２の動作では受理できないテストケースが存在する。この場合、これら２つの部品の間のテスト容易化指標を計算すると以下のようになる。まずクルーズ制御部５１のテストケースとエンジン制御部５２の入力制約とを対象にした場合のテスト容易化指標は以下のようになる。
クルーズ制御部５１">"エンジン制御部５２
エンジン制御部５２のテストケースとクルーズ制御部５１の入力制約とを対象にした場合も同様にしてテスト容易化指標を計算する。
【０１６５】
また、クルーズ制御部５１とブレーキ制御部５３の間のテスト容易化指標を計算すると以下のようになる。まずクルーズ制御部５１のテストケースとブレーキ制御部５３の入力制約とを対象にした場合のテスト容易化指標は以下のようになる。
クルーズ制御部５１">"ブレーキ制御部５３
ブレーキ制御部５３のテストケースとクルーズ制御部５１の入力制約とを対象にした場合も同様にしてテスト容易化指標を計算する。
【０１６６】
手順［２］ではこのようにして求めたテスト容易化指標（ここでは４つ）を種類別に集計して表示または出力する。
【０１６７】
＜アサーション生成部２３＞
アサーション生成部２３は品質情報DB１４に格納されている部品毎の入力制約に対して、個々の入力制約を満たすことを要求するアサーション記述を生成する。アサーションの記述方式は任意の記述方式を用いることができるが、一例として以下の文献３にあるLTLやPSL等を用いることができる。
［文献３］
アサーションベース設計  原書2版
Harry D.Foster・Adam C.Krolnik・David J. Lacey  著
東野  輝夫・岡野  浩三・中田  明夫  監訳
丸善書店
【０１６８】
＜監視・回避仕様生成部２４＞
監視・回避仕様生成部２４は、アサーション生成部２３が生成したアサーションが成立することを監視する監視モジュールの仕様を生成し、生成された監視モジュール仕様および上記アサーション記述をシステム仕様１０１に埋め込む。また監視モジュールが異常を検知した場合に回避処理を行う回避モジュールの仕様を生成し、これもシステム仕様１０１に埋め込む。監視モジュール仕様および回避モジュール仕様の生成ならびにシステム仕様１０１への埋込に関しては、任意の方法を用いることができるが、一例として、以下の文献４に挙げられる技術を用いることができる。
［文献４］
"Towards Model-Based Failure-Management for Automotive Software",
Ermagan, V. and Mizutani, J. and Oguchi, K. and Weir, D.,
Proceedings of the 4th International Workshop on Software Engineering for
Automotive Systems,2007
【０１６９】
このようにして監視・回避仕様生成部２４によりアサーション記述、監視モジュール仕様、回避モジュール仕様が埋め込まれることにより高信頼化システム仕様１０４が生成される。この高信頼化システム仕様１０４および品質仕様ＤＢ１４を用いて、高信頼度のテストを行うことできる。たとえば部品毎またはシステム、のアサーション記述に違反する入力アクションがあった場合はこれを検出して、入力アクションの入力を防ぐ（不整合の発生を防ぐ）とともに、違反に応じた回避処理を行うことができる。
【０１７０】
以上のように、本発明の実施の形態によれば、部品を組み合わせてソフトウエア、ハードウエア、あるいはソフトウエアとハードウエアを組み合わせたシステム、を構築する場合に、部分最適な整合性検証ではなくて、全体最適な整合性検証を実現できる。
【０１７１】
また、複数の部品からなるシステムにおける各隣接する部品同士間について、一方および他方の部品のテストケースが他方および一方の部品の入力制約を充足するか否かを検査することにより、各隣接する部品同士間についての整合性を検証できる。この方法によれば、新たに部品が追加されても、隣接部品との整合性を容易に検証できる。
【０１７２】
また、不整合が見つかった場合は、不整合を起こさないように一方の入力制約を強化したり他方の入力制約を緩和したりすることで、不整合を修正することができる。入力制約の強化および緩和を適切に選択しながら、各隣接する部品同士間についてそれぞれ不整合が存在しないようにすることで、システム全体で不整合を無くすことができる。これらによって不必要にテストケースが増大するのを防止する効果も得られる。
【０１７３】
また、不整合が存在しない部品間については一方の部品のテストケースが充足される限りにおいて他方の部品の入力制約を強化することによりテストケースを減少させることができる。
【０１７４】
また、本実施の形態によれば、複数部品の組み合わせた上位階層に対する動作仕様および入力制約を、各下位部品の品質仕様から生成できるため、部品を組み合わせて初めて発生する動作に関する制約も取り扱うことが可能になる。また上位階層と、当該上位階層に接続される部品との整合性検査および不整合解消も可能になる。
【０１７５】
なお、このテスト容易化設計装置は、例えば、汎用のコンピュータ装置を基本ハードウエアとして用いることでも実現することが可能である。すなわち、入力制約抽出部、テストケース生成部（アクション列取得部、モデル生成部）、品質仕様生成部、品質仕様整合性検査部（検査部、選択部）、入力制約計算部（入力制約調整部）、緩和条件計算部（入力制約調整部）、強化条件計算部（入力制約強化部）、品質仕様更新部、上位階層用品質仕様計算部（制御部、選択部）、テスト容易化指標計算部、条件伝播部（制御部）、アサーション生成部、監視および回避仕様生成部（仕様生成部）は、上記のコンピュータ装置に搭載されたプロセッサにプログラムを実行させることにより実現することができる。このとき、テスト容易化設計装置は、上記のプログラムをコンピュータ装置にあらかじめインストールすることで実現してもよいし、ＣＤ−ＲＯＭなどの記憶媒体に記憶して、あるいはネットワークを介して上記のプログラムを配布して、このプログラムをコンピュータ装置に適宜インストールすることで実現してもよい。また、品質仕様ＤＢ（第１記憶部、第２記憶部、第３記憶部等）は、上記のコンピュータ装置に内蔵あるいは外付けされたメモリ、ハードディスクもしくはＣＤ−Ｒ、ＣＤ−ＲＷ、ＤＶＤ−ＲＡＭ、ＤＶＤ−Ｒなどの記憶媒体などを適宜利用して実現することができる。
【図面の簡単な説明】
【０１７６】
【図１】本発明の実施形態としてのテスト容易化設計装置の構成を示すブロック図。
【図２】システム仕様に記述されたクルーズコントロールシステムの構成図。
【図３】クルーズ制御部の動作仕様を状態遷移表形式で表した図。
【図４】図３の状態遷移表（動作仕様）を遷移図形式で表現した図。
【図５】エンジン制御部の動作仕様を状態遷移表形式で表した図。
【図６】ブレーキ制御部の動作仕様を状態遷移表形式で表した図。
【図７】クルーズ制御部の状態遷移機械モデルを示す図。
【図８】エンジン制御部の状態遷移機械モデルを示す図。
【図９】ブレーキ制御部の状態遷移機械モデルを示す図。
【図１０】ＮＧ遷移ポイントを説明する図。
【図１１】（エンジン制御部×ブレーキ制御部）の動作を状態遷移表の形式で表した図。
【図１２】テストケース生成部の処理手順を示すフローチャート。
【図１３】品質仕様整合性検査部の処理手順を示すフローチャート。
【図１４】入力制約計算部の処理手順を示すフローチャート。
【図１５】緩和条件計算部の処理手順を示すフローチャート。
【図１６】強化条件計算部の処理手順を示すフローチャート。
【図１７】上位階層用品質仕様計算部の処理手順を示すフローチャート。
【図１８】条件伝播部の処理手順を示すフローチャート。
【図１９】図１８の処理手順を説明するために例示したシステムを示す図。
【符号の説明】
【０１７７】
１０１：システム仕様
１０２：形式仕様（動作仕様、入力制約）
１０３：テスト容易化判定基準
１０４：高信頼化システム仕様
１１：入力制約抽出部
１２：テストケース生成部（アクション列取得部、モデル生成部）
１３：品質仕様生成部
１４：品質仕様ＤＢ（第１記憶部、第２記憶部、第３記憶部）
１５：品質仕様整合性検査部（検査部、選択部）
１６：入力制約計算部（入力制約調整部）
１７：緩和条件計算部（入力制約調整部）
１８：強化条件計算部（入力制約強化部）
１９：品質仕様更新部
２０：上位階層用品質仕様計算部（制御部、選択部）
２１：テスト容易化指標計算部
２２：条件伝播部（制御部）
２３：アサーション生成部
２４：監視および回避仕様生成部（仕様生成部）
【図１】
2010128583.tif 000020
【図２】
2010128583.tif 000021
【図３】
2010128583.tif 000022
【図４】
2010128583.tif 000023
【図５】
2010128583.tif 000024
【図６】
2010128583.tif 000025
【図７】
2010128583.tif 000026
【図８】
2010128583.tif 000027
【図９】
2010128583.tif 000028
【図１０】
2010128583.tif 000029
【図１１】
2010128583.tif 000030
【図１２】
2010128583.tif 000031
【図１３】
2010128583.tif 000032
【図１４】
2010128583.tif 000033
【図１５】
2010128583.tif 000034
【図１６】
2010128583.tif 000035
【図１７】
2010128583.tif 000036
【図１８】
2010128583.tif 000037
【図１９】
2010128583.tif 000038