(57)【特許請求の範囲】
【請求項１】
検証対象である対象システムの動作を検証するシステムにおいて、
前記対象システムの機能仕様の情報を取得し、当該対象システムが取り得る状態をノードに対応付け、当該対象システムを構成するオブジェクトの状態遷移と当該オブジェクトどうしの相互作用を当該ノード間の接続関係に対応付けた二分木を生成する二分木生成部と、
前記対象システムの動作に基づいて取得される情報から得られる当該対象システムのアプリケーション・モデル上でのイベント列を受け付け、当該イベント列と前記二分木生成部により生成された前記二分木とを照合する照合部と、
を備えるシステム。
【請求項２】
前記二分木生成部は、前記対象システムの機能仕様の情報として、前記オブジェクトの状態遷移図と当該対象システムのユースケースごとのシーケンス図とを取得し、当該状態遷移図から得られる状態遷移の情報と当該シーケンス図から得られる相互作用の情報に基づいて前記二分木を生成する、請求項１に記載のシステム。
【請求項３】
前記二分木生成部は、前記シーケンス図を構成するアクションの列のうち、相互作用を起こさない部分列であって、かつ当該部分列の開始点および終了点における前記対象システムの状態が一致する部分列を重ね合わせて、前記二分木を生成する、請求項２に記載のシステム。
【請求項４】
前記二分木生成部は、前記二分木の開始点における前記対象システムの状態である前提条件に関して、複数の当該前提条件の間の含意関係を表現するグラフを生成し、
前記照合部は、取得した前記イベント列の開始点における前記対象システムの状態に合致する前提条件を、前記グラフから検索し、検索された前提条件を持つ前記二分木を、当該イベント列の照合の対象とする、請求項１に記載のシステム。
【請求項５】
前記照合部は、前記対象システムにおいて発生した複数のイベント列に対応して複数の探索空間を記憶装置上に設定し、当該複数の探索空間において並列に当該イベント列と前記二分木との照合を行う、請求項１に記載のシステム。
【請求項６】
前記照合部は、設定した前記探索空間に対して終了時間を設定し、当該終了時間に達した探索空間に関して、当該探索空間で行われている処理を打ち切り、当該探索空間が使用している前記記憶装置の記憶領域を開放する、請求項５に記載のシステム。
【請求項７】
前記照合部は、前記対象システムの動作のうち検証対象としないイベントを指定するソフトウェア・フィルタを用いて、検索対象となるイベント列を絞り込む、請求項１に記載のシステム。
【請求項８】
前記対象システムに設けられたプローブによって、当該対象システムの動作に伴って得られる情報を、当該対象システムの前記アプリケーション・モデル上でのイベント列に変換し、前記照合部に送信する変換部をさらに備える、請求項１に記載のシステム。
【請求項９】
検証対象である対象システムの動作を検証する方法であって、
前記対象システムの機能仕様の情報として、オブジェクトの状態遷移図と当該対象システムのユースケースごとのシーケンス図とを取得するステップと、
前記状態遷移図から得られる状態遷移の情報と前記シーケンス図から得られる相互作用の情報とに基づいて、前記対象システムが取り得る状態をノードに対応付け、当該対象システムを構成するオブジェクトの状態遷移と当該オブジェクトどうしの相互作用を当該ノード間の接続関係に対応付けた二分木を生成するステップと、
前記対象システムの動作に基づいて取得される情報から得られる当該対象システムのアプリケーション・モデル上でのイベント列を受け付け、当該イベント列と生成された前記二分木とを照合するステップと、
を含む方法。
【請求項１０】
前記二分木を生成するステップでは、前記シーケンス図を構成するアクションの列のうち、相互作用を起こさない部分列であって、かつ当該部分列の開始点および終了点における前記対象システムの状態が一致する部分列を重ね合わせて、前記二分木を生成する、請求項９に記載の方法。
【請求項１１】
前記二分木の開始点における前記対象システムの状態である前提条件に関して、複数の当該前提条件の間の含意関係を表現するグラフを生成するステップと、
取得された前記イベント列の開始点における前記対象システムの状態に合致する前提条件を、前記グラフから検索し、検索された前提条件を持つ前記二分木を、当該イベント列の照合の対象とするステップと、
をさらに含む請求項９に記載の方法。
【請求項１２】
コンピュータを、
対象システムの機能仕様の情報を取得し、当該対象システムが取り得る状態をノードに対応付け、当該対象システムを構成するオブジェクトの状態遷移と当該オブジェクトどうしの相互作用を当該ノード間の接続関係に対応付けた二分木を生成する二分木生成手段と、
前記対象システムの動作に基づいて取得される情報から得られる当該対象システムのアプリケーション・モデル上でのイベント列を受け付け、当該イベント列と前記二分木生成手段により生成された前記二分木とを照合する照合手段として、
動作させるプログラム。
【請求項１３】
前記二分木生成手段の機能として、前記対象システムの機能仕様の情報として、前記オブジェクトの状態遷移図と当該対象システムのユースケースごとのシーケンス図とを取得し、当該状態遷移図から得られる状態遷移の情報と当該シーケンス図から得られる相互作用の情報に基づいて前記二分木を生成する処理を、前記コンピュータに実行させる、請求項１２に記載のプログラム。
【請求項１４】
前記二分木生成手段の機能として、前記シーケンス図を構成するアクションの列のうち、相互作用を起こさない部分列であって、かつ当該部分列の開始点および終了点における前記対象システムの状態が一致する部分列を重ね合わせて、前記二分木を生成する処理を、前記コンピュータに実行させる、請求項１３に記載のプログラム。
【請求項１５】
前記二分木生成手段の機能として、前記二分木の開始点における前記対象システムの状態である前提条件に関して、複数の当該前提条件の間の含意関係を表現するグラフを生成する処理と、
前記照合手段の機能として、取得した前記イベント列の開始点における前記対象システムの状態に合致する前提条件を、前記グラフから検索し、検索された前提条件を持つ前記二分木を、当該イベント列の照合の対象とする処理と、
を前記コンピュータに実行させる、請求項１２に記載のプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、システムの動作を検証するシステムに関し、特にリアルタイム・システムや組み込みシステムの動作の検証を行うシステムおよびその方法に関する。
【背景技術】
【０００２】
処理にリアルタイム（実時間）性が要求されるリアルタイム・システムや各種の機器に内蔵される組み込みシステムの動作を検査するためには、評価ボードや実機のハードウェアを用いソフトウェアを実際に稼動させて、その振る舞いを観測することが不可欠である。システムの振る舞いの観測は、ハードウェアおよびソフトウェアに付加されたプローブ（probe）によって行われる。この種のシステムの動作はリアルタイム性が要求されるため、プローブによる観測および取得データの処理がシステムの動作性能に及ぼす影響（侵襲性：Intrusion）が、可能な限り小さいことが望まれる。
【０００３】
この種の従来技術の一例として、スウェーデンＺｅａｌＣｏｒｅ社のＢｌａｃｋＢｏｘ  Ｔｅｃｈｎｏｌｏｇｙ（例えば、非特許文献１参照）がある。この従来技術は、システムの動作を記録し、記録された動作を再現する技術である。この技術は、システムがクラッシュした場合に、記録されたクラッシュまでのシステムの動作の記録をクラッシュの原因の特定に役立てることを目的としている。この技術では、コード生成技術と連携して、システムのソフトウェアに埋め込んだプローブ・コードによって、その振る舞いを観測する。プローブ・コードによる観測および処理に要するＣＰＵ時間は、システムのプロセッサが提供する計算時間の全体に対して小さく抑えられている（非特許文献２参照）。また、システムの動作自体の情報量は膨大になるが、動作を再現するのに充分な情報のみを記録することで、実際に記録される情報量は現実的な範囲に収められている。
【０００４】
【非特許文献１】Henrik Thane, Daniel Sundmark, 「Debugging Using Time Machines: replay your embedded system's history」, [online], Real-Time & Embedded Computing Conference, p Kap 22, Milan, Italy, November, 2001, [平成19年10月12日検索], インターネット＜URL : http://www.mrtc.mdh.se/index.php?choice=publications&id=0347＞
【非特許文献２】Hans Hansson, 「RTS Debugging」, [online], MALARDALEN REAL-TIME RESEARCH CENTRE, 2003, [平成19年10月11日検索], インターネット＜URL : http://www.artes.uu.se/industry/031111/debugging-ZC-031111.pdf＞
【発明の開示】
【発明が解決しようとする課題】
【０００５】
上述したように、リアルタイム・システムや組み込みシステムの動作の検査では、実際に検査対象のシステムを動作させて、その振る舞いを観測することが必要である。そして、その観測および取得データの処理は、侵襲性が小さいことが望ましい。
ここで、検査対象のシステムに対するバグ修正の観点から、システム動作の検査を必要とする項目は、例えば、機能要件に対する正当性や、性能要件に対する充足性など多岐にわたる。また、どのような検査をおこなうかによって、必要となる情報は異なる。そのため、汎用の目的の観測では効率が悪く、侵襲性を小さく抑えることが困難である。
【０００６】
上記のスウェーデンＺｅａｌＣｏｒｅ社の従来技術は、観測対象のシステムの動作を観測して、その情報を記録する。しかし、その記録は、システムのクラッシュの原因特定を対象としており、システムのバグ修正を要する他の多くの事象に対応していない。
【０００７】
本発明は、以上の課題に鑑みて成されたものであり、その目的は、多様な検査条件を判断しながら、検査対象のシステムの動作を観測し、検証するシステムおよびその検証方法を提供することにある。
また、本発明の他の目的は、システムの動作を検証する際に生じる、検証対象のシステムの動作性能に対する侵襲性を小さく抑えることにある。
【課題を解決するための手段】
【０００８】
上記の目的を達成するため、本発明は、次のようなシステムとして構成される。このシステムは、検証対象である対象システムの動作を検証するシステムであって、二分木生成部と、照合部とを備える。二分木生成部は、対象システムの機能仕様の情報を取得し、この対象システムが取り得る状態をノードに対応付け、かつこの対象システムを構成するオブジェクトの状態遷移とオブジェクトどうしの相互作用をノード間の接続関係に対応付けた二分木を生成する。照合部は、対象システムの動作に基づいて取得される対象システムのアプリケーション・モデル上でのイベント列を受け付け、このイベント列と二分木生成部により生成された二分木とを照合する。
【０００９】
より好ましくは、対象システムの機能仕様の情報は、オブジェクトの状態遷移図および対象システムのユースケースごとのシーケンス図である。二分木生成部は、状態遷移図から得られる状態遷移の情報とシーケンス図から得られる相互作用の情報に基づいて二分木を生成する。
さらに好ましくは、二分木生成部は、シーケンス図を構成するアクションの列のうち、相互作用を起こさない部分列であって、かつこの部分列の開始点および終了点における対象システムの状態が一致する部分列を重ね合わせる。
また、二分木生成部は、二分木の開始点における対象システムの状態である前提条件に関して、複数の前提条件の間の含意関係を表現するグラフを生成する。そして、照合部は、取得したイベント列の開始点における対象システムの状態に合致する前提条件を、グラフから検索し、検索された前提条件を持つ二分木とイベント列とを照合する。
【００１０】
また、より好ましくは、照合部は、対象システムにおいて発生した複数のイベント列に対応して複数の探索空間を記憶装置上に設定し、この複数の探索空間において並列にイベント列と二分木との照合を行う。
そして、照合部は、設定した探索空間に対して終了時間を設定し、この終了時間に達した探索空間に関して、探索空間で行われている処理を打ち切り、探索空間が使用している記憶装置の記憶領域を開放する。
また、照合部は、対象システムの動作のうち検証対象としないイベントを指定するソフトウェア・フィルタを用いて、検索対象となるイベント列を絞り込む。
上記のシステムにおいて、対象システムに設けられたプローブによって、対象システムの動作に伴って得られる情報を、対象システムのアプリケーション・モデル上でのイベント列に変換し、照合部に送信する変換部をさらに備える構成としても良い。
【００１１】
また、本発明は、次のような、検証対象である対象システムの動作を検証する方法としても実現される。この方法は、対象システムの機能仕様の情報として、オブジェクトの状態遷移図と対象システムのユースケースごとのシーケンス図とを取得するステップと、状態遷移図から得られる状態遷移の情報とシーケンス図から得られる相互作用の情報とに基づいて、対象が取り得る状態をノードに対応付け、対象システムを構成するオブジェクトの状態遷移とオブジェクトどうしの相互作用をノード間の接続関係に対応付けた二分木を生成するステップと、対象システムの動作に基づいて取得される対象システムのアプリケーション・モデル上でのイベント列を受け付け、このイベント列と生成された二分木とを照合するステップと、を含む。
【００１２】
さらに本発明は、コンピュータを制御して上記のシステムの機能を実現するプログラム、または上記の方法における各ステップに対応する処理をコンピュータに実行させるプログラムとしても実現される。このプログラムは、磁気ディスクや光ディスク、半導体メモリ、その他の記憶媒体に格納して配布したり、ネットワークを介して配信したりすることにより提供することができる。
【発明の効果】
【００１３】
以上のように構成された本発明によれば、多様な検査条件を判断しながら、検査対象のシステムの動作を観測し、検証することが可能となる。
また、本発明によれば、システムの動作を検証する際に生じる、検証対象のシステムの動作性能に対する侵襲性を小さく抑えることが可能である。
【発明を実施するための最良の形態】
【００１４】
以下、添付図面を参照して、本発明の実施形態について詳細に説明する。
本実施形態では、モデル駆動開発（Model Driven Architecture）により開発されたシステムを検証対象として、アプリケーションがシステムの機能仕様を満足するか否かを検証する。この検証対象のシステム（以下、対象システムと呼ぶ）の機能仕様は、ＵＭＬ（Unified Modeling Language）等によるアプリケーション・モデル（application model）として記述される。対象システムは、このアプリケーション・モデルから自動生成されたＣやＣ＋＋によるコードを稼動させる。
【００１５】
対象システムのアプリケーション・モデルは、複数の状態機械（オブジェクト）によって構成される。ここで、状態機械とは、データや対象機器の構成要素のような、対象システムを構成し、所定の機能を担う小さい単位の要素である（ハードウェアに限定しない）。どのような単位の要素を状態機械とするかについては任意であり、検査の内容等に応じて決定すれば良い。個々の状態機械は状態遷移図（State Transition Diagram）で定義される。この状態遷移図には、ＵＭＬ等で提供される既存のものを用いて良い。
【００１６】
所定の状態機械が所定の状態に到達した時点や所定の状態遷移を生じた時点に付随するアクション（振る舞い）は、状態遷移図の定義とは別個に与えられる。このアクションによって、個々の局面におけるシステムの各構成要素の振る舞いが与えられる。このアクションの中には、メッセージの通信による状態機械間の相互作用も記述される。この相互作用によって、状態機械が連携して全体のシステムとして機能する。このアクションは、対象システムの具体的な処理を記述するアクション記述言語によって表現される。アクション記述言語には、独自の専用言語や既存のプログラミング言語などが用いられる。
【００１７】
このようなモデル駆動開発によって開発されたアプリケーションが機能仕様を満たしていることを検証するためには、個々の状態機械の状態遷移や状態機械間の相互作用が機能仕様どおりであることを検証することが必要である。状態遷移や相互作用をアプリケーション・モデル上のイベントとして抽象化すると、この検証問題は、イベント列が機能仕様で許されるパターンに含まれるかどうかを検査する問題と同等となる。したがって、この検証問題は、文字列のパターン照合問題と類似している。
【００１８】
しかし、リアルタイム・システムや組込みシステムを対象システムとする場合の動的検証は、次の３点において、文字列のパターン照合とは異なる。
第１の相違点は、アプリケーション・モデルから生成されるＣやＣ＋＋コードの実行において、状態遷移や相互作用が生じる頻度は千〜数千マシン・サイクルに一回程度である、という点である。すなわち、本実施形態の動的検証では、文字列全体を与えてパターン照合するのと異なり、離散的に発生する個々のイベントを照合する必要がある。一つのイベントの照合は、千マシン・サイクル程度で完了する必要があり、その頻度に応じた高速化が必要となる。
【００１９】
第２の相違点は、本実施形態の動的検証のためには、対象システムの振る舞いを観測するためのプローブから離れていないボード（評価ボードや実機のボード）上で照合をおこなう必要がある。そのため、検証のためのボードのハードウェアの制約、特にメモリ容量の制約を受ける、という点である。文字列のパターン照合においては、正規表現などで与えられたパターンをオートマトンとして等価な状態遷移表に展開することによって照合処理を高速化することができる。しかし、本実施形態の動的検証では、動作シナリオが多岐に渡る場合があり、パターンに相当する仕様が多くなるので単純にすべてを展開すると膨大なメモリを必要としてしまい、ハードウェアの制約を満たすことが困難になる。
【００２０】
第３の相違点は、システムの動作における各状態機械の振る舞いは、基本的に並列的である。したがって、発生するイベント列は一つのパターンと照合するとは限らない、という点である。すなわち、観測されるイベント列の個々のイベントは、二つまたはそれ以上の機能仕様（パターン）と交互に照合される可能性がある。
【００２１】
本実施形態の検証システムでは、文字列のパターン照合を行うシステムと比較して、上記の第１と第２の相違点に起因して、ある程度の（メモリ容量を大量に消費しない範囲での）高速化が必要となる。また、第３の相違点に起因して、複数のパターン照合を並列に実行する技術が必要となる。これらを満足するため、本実施形態では、状態機械の状態遷移や相互作用を記述するための固有のデータ構造を導入する。このデータ構造は、二分木構造であり、対象システムの稼働前に生成される。以下、このデータ構造を生成し、このデータ構造を用いて検証を行うシステムについて説明する。
【００２２】
＜システム構成＞
図１は、本実施形態による検証システムの機能構成を示す図である。
図１に示す検証システム１００は、抽象二分木生成部１１０と、抽象二分木格納部１２０と、照合部１３０と、ＩＤフィルタ生成部１４０とを備える。本実施形態の検証システム１００の機能は、対象システムの稼働前（または検証開始前）に働く機能と対象システムの稼働時に働く機能に大きく分かれる。図１において、抽象二分木生成部１１０およびＩＤフィルタ生成部１４０は対象システムの稼働前に動作する機能であり、照合部１３０は対象システムの稼働時に動作する機能である。また、図１に示すように、検証システム１００には、対応表格納部２００およびデータ変換部３００が接続されている。
【００２３】
検証システム１００は、対象システムのボード（評価ボードまたは実機のボード）上で構成される。したがって、図１に示す検証システム１００の各機能は、ＳＵＴ（System Under Test）すなわち対象システムのハードウェア資源を用いて実現される。図１において、抽象二分木生成部１１０、照合部１３０およびＩＤフィルタ生成部１４０は、プログラム制御されたＣＰＵ（Central Processing Unit）とＲＡＭ（Random Access Memory）等の記憶手段により実現される。すなわち、プログラムがＲＡＭに読み込まれ、ＣＰＵにより実行されることで、これらの機能が実現される。抽象二分木格納部１２０は、ＲＡＭや磁気ディスク装置等の記憶手段で実現される。
【００２４】
抽象二分木生成部１１０は、状態機械の状態遷移や相互作用を記述するためのデータ構造である二分木（以下、抽象二分木と呼ぶ）を生成する。抽象二分木は、対象システムの稼働前または検証システム１００による検証開始前に生成され、抽象二分木格納部１２０に格納される。抽象二分木の詳細および抽象二分木生成部１１０による抽象二分木の具体的な生成方法については後述する。
【００２５】
抽象二分木格納部１２０は、抽象二分木生成部１１０により生成された抽象二分木を格納する。抽象二分木格納部１２０に格納された抽象二分木は、検証システム１００が対象システムの検証を行う際に照合部１３０により読み出されて使用される。
【００２６】
照合部１３０は、データ変換部３００から取得する対象システムのイベント列と抽象二分木格納部１２０から読み出した抽象二分木とを照合することにより、対象システムの検証を行う。照合部１３０は、イベントが発生するたびに、記憶装置（作業用メモリ）のメモリ領域に新たな探索空間を設定し、新たに発生したイベントに対する抽象二分木を用いた照合を、この新たに設定した探索空間で行う。複数の探索空間を管理することで、複数の照合を並列に実行する。具体的な照合の方法については後述する。
【００２７】
ＩＤフィルタ生成部１４０は、イベント・フィルタ記述と後述するＩＤの対応表とを用いて、照合部１３０の処理に用いられるＩＤフィルタを生成し、照合部１３０に送る。ＩＤフィルタは、対象システムで発生するイベントのうち、検索対象から外すイベント（状態遷移および相互作用）を指定するソフトウェア・フィルタである。ＩＤフィルタの詳細およびＩＤフィルタ生成部１４０によるＩＤフィルタの具体的な生成方法については後述する。
【００２８】
対象システムにおいて、プローブにより取得される情報は、ジャンプや条件分岐が生じた時点でのジャンプ先メモリアドレスなどである。検証システム１００は、この情報を変換して得られる、アプリケーション・モデル上での振る舞いを表すイベント列（以下、モデル・イベント列と呼ぶ）を入力として受け付ける。モデル・イベントは、所定の状態機械の状態遷移イベント（transition event）か、メッセージ送信による相互作用イベント（interaction event）のいずれかである。検証を高速化するために、これらのイベントは、アプリケーション・モデルにおける状態遷移や送信メッセージの名称ではなく、例えば整数値（integer value）によるＩＤで表現される。
【００２９】
対応表格納部２００は、アプリケーション・モデルにおける状態遷移および送信メッセージの名称をＩＤに変換するための対応表（マッピング・テーブル）を保持する。対応表には、アプリケーション・モデルにおける状態機械の状態遷移と状態遷移ＩＤとを対応付けた対応表と、アプリケーション・モデルにおける状態機械間の送信メッセージの名称と相互作用ＩＤとを対応付けた対応表とがある。これらの対応表は、抽象二分木生成部１１０が抽象二分木を生成する際、およびＩＤフィルタ生成部１４０がＩＤフィルタを生成する際に使用される。
【００３０】
データ変換部３００は、対象システムの動作に伴い、対象システムのハードウェアおよびソフトウェアに付加されたプローブ（物理的なプローブおよびプローブ・コード）を介して取得される情報をモデル・イベント列に変換する。このモデル・イベント列における各モデル・イベントは、上述したＩＤで表現されている。データ変換部３００により変換されたモデル・イベント列は、照合対象として照合部１３０に送られる。
【００３１】
＜抽象二分木生成部１１０の動作と抽象二分木の説明＞
抽象二分木生成部１１０は、対象システムの機能仕様の情報を取得して、検証に用いられる抽象二分木を生成する。対象システムの機能仕様は、個々の状態機械の状態遷移図と、アクション記述言語によるアクション記述とにより記述される。アクション記述は、独自言語や既存のプログラミング言語で与えられる。これらの言語は手続き的に表現される場合がほとんどである。そのため、アクション記述自身を検証に用いるのは難しい。そこで、本実施形態では、対象システム全体の振る舞いの機能的正当性を検証するために、アプリケーション・モデルとは別に、相互作用仕様（interaction specification）が入力として与えられる。本実施形態において、この相互作用仕様は、シーケンス図（sequence diagram）の集合として表現される。
【００３２】
図２は、シーケンス図の例を示す図である。
個々のシーケンス図は、所定のユースケース・シナリオ（use-case scenario）における対象システムの振る舞いを定義する。このシーケンス図には、ＵＭＬ等で提供される既存のものを用いて良い。
【００３３】
抽象二分木生成部１１０は、これらのアプリケーション・モデルの状態遷移図と相互作用仕様のシーケンス図に基づいて抽象二分木を生成する。抽象二分木は、シーケンス図の集合を二分木構造に再構成したデータ構造である。この抽象二分木は、対象システムが取り得る個々の状態がノードに対応付けられ、対象システムにおける各状態機械の状態遷移および状態機械間のメッセージのやり取り（相互作用）がノード間の接続関係に対応付けられる。開始点における対応システムの状態が同一であるシーケンス図は、単一のノードをルートとする一つの抽象二分木にまとめられる。
【００３４】
二分木は、高速探索のために一般的に用いられるデータ構造である。二分木では、分岐の条件をどのようにするかで探索効率が大きく異なるため、探索すべき対象に合わせた分岐条件の設定が重要な意味を持つ。上記の抽象二分木を生成するため、本実施形態では、相互作用仕様を記述する際のユースケース・シナリオ群の性質と、アプリケーション・モデルに与えられる個々の状態機械の状態遷移図に着目する。
【００３５】
相互作用仕様は、対象システムの正当な機能的振る舞いを与える複数のユースケース・シナリオの群についてのシーケンス図によって定義される。ここで、複数のユースケース・シナリオは、所定の基本的なシナリオと、そのバリエーションであるシナリオ群とで構成されることが多い。バリエーションは、個々の状態機械において、特定の同じ状態で発生し得る状態遷移が複数あることによって生じる。したがって、抽象二分木を生成する場合の分岐条件としては、可能な状態遷移を複数もつ状態について分岐ノードを作成し、個々のシーケンス図を木に配置するようにする。
【００３６】
ところで、相互作用仕様に記述された対象システムの振る舞いを単純に二分木として表現する場合、システム動作の並行性に起因するイベント列の差異を全て区別すると、メモリ使用量が膨大になってしまう。このような事態を避け、抽象二分木のサイズを現実的な大きさに抑えるため、本実施形態では、相互作用を起こさない状態遷移の部分列で、かつ、その部分列の開始点と終了点における対象システムの状態が一致しているものを重合（aggregate）して抽象化（abstract）する。
【００３７】
図３および図４は、二分木の抽象化の例を示す図である。
図３において、シーケンス図（図３（ａ））からアクションの列（シーケンス）が抽出される（図３（ｂ））。この列のうち、上の三つのアクションに注目すると、この部分列（サブ・シーケンス）は、＜ｘ，ｙ，ｚ＞という状態から＜ｐ，ｑ，ｒ＞という状態へ、ａ、ｂ、ｃという三つのアクションを経て遷移することを意味している（図３（ｃ））。
【００３８】
次に、図４を参照すると、図３（ｃ）に示したものと同様に、開始点の状態が＜ｘ，ｙ，ｚ＞であり、終了点の状態が＜ｐ，ｑ，ｒ＞である部分列が複数存在している（図４（ａ））。すなわち、状態＜ｘ，ｙ，ｚ＞から状態＜ｐ，ｑ，ｒ＞へ遷移する部分列のパターンが複数存在する。これは、状態＜ｘ，ｙ，ｚ＞から状態＜ｐ，ｑ，ｒ＞への遷移を表す部分列において、経路が複数あることを意味している（図４（ｂ））。ここで、図４（ａ）、（ｂ）を詳細に検討すると、三つのアクションａ、ｂ、ｃに関しては、発生する順番に関わらず、この三つのアクションが起きれば、状態＜ｘ，ｙ，ｚ＞から状態＜ｐ，ｑ，ｒ＞へ遷移していることがわかる。また、図４では記載を省略しているが、四つのアクションｄ、ｅ、ｆ、ｇに関しては、ｄと、ｅと、ｆかｇのいずれかの三つのアクションが起きれば、発生した順番に関わらず、状態＜ｘ，ｙ，ｚ＞から状態＜ｐ，ｑ，ｒ＞へ遷移するものとする。そこで、図４（ｂ）の各経路を重ね合わせ、状態＜ｘ，ｙ，ｚ＞から状態＜ｐ，ｑ，ｒ＞への遷移を表す単純な部分列に変換する（図４（ｃ））。
【００３９】
以上のような操作を行うことで、開始点と終了点における対象システムの状態が共通する部分列が重合され（重ね合わされ）、終了点の状態が異なる部分列が分岐されて残っていくことで、図５に示すような、開始点の状態が＜ｘ，ｙ，ｚ＞である抽象二分木が生成される。抽象二分木生成部１１０は、ユースケース・シナリオにおける開始点の対象システムの状態ごとに、図５に示すような抽象二分木を生成する。
【００４０】
なお、図４（ｃ）および図５の表記において、［ａ，ｂ］は「置換（permutation）」（要素ａ、ｂの順番を入れ替え可能）を意味し、｛ｊ｜ｋ｝は「選択（selection）」（要素ｊ、ｋのいずれか一方）を意味し、＜ｘ；ｙ＞は「連結（concatenation）」（要素ｘ、ｙの両方を満たすこと）を意味する。また、図５において、黒い矢印で示した部分列は状態遷移（State transition）を表し、白抜きの矢印で示した部分列は状態機械間の情報のやり取り（Message passing）を表すものとする。
【００４１】
図６および図７は、抽象二分木の生成方法を説明するフローチャートである。
図６に示すように、抽象二分木生成部１１０は、まず開始点の状態が同一であるシーケンス図を集めて、シーケンス図群とする（ステップ６０１）。次に、抽象二分木生成部１１０は、所定のシーケンス図群を選び、そのシーケンス図から所定の列（シーケンス）を抽出する（ステップ６０２）。そして、抽出した列に対して上述した重合処理を行う（ステップ６０３）。抽象二分木生成部１１０は、ステップ６０２で選んだシーケンス図群の全ての列に対して重合処理を実行する。そして、未処理の列が無くなったならば（ステップ６０４）、他のシーケンス図群を選び、ステップ６０２以降の処理を繰り返す。未処理のシーケンス図群が無くなったならば、処理を終了する（ステップ６０５）。
【００４２】
図７は、図６のステップ６０３に示す重合処理の手順を示す。
抽象二分木生成部１１０は、まず、ステップ６０２で選んだ列の中から最初の部分列が状態遷移によって同一の状態に至るような列の一群（サブ・セット）を選択する（ステップ７０１）。そして、選択した一群の列における部分列に対応するアークを生成し、この部分列のパターンと生成したアークとを対応付ける（ステップ７０２）。次に、抽象二分木生成部１１０は、後続するイベント（状態遷移や情報のやり取り）に応じて残りの列の群（サブ・セット）を生成する（ステップ７０３）。そして、ステップ７０３で生成した列の群に対応する分岐ノードと、このノードに接続するアークとを生成する（ステップ７０４）。
【００４３】
この後、抽象二分木生成部１１０は、ステップ７０４で生成したアークに対応する列の一群を抽出する（ステップ７０５）。そして、抽出された列の群に対して以上の重合処理を再帰的に実行する（ステップ７０６）。抽象二分木生成部１１０は、全てのシーケンス図群に対して以上の処理を実行し、未処理のシーケンス図群が無くなったならば、処理を終了する（ステップ７０７）。
【００４４】
以上のようにして部分列の重合を行うことにより、抽象二分木のデータサイズは縮小される。しかし、抽象二分木は、前提条件（assertion）の違いに応じて複数生成され得る。前提条件とは、具体的には個々の抽象二分木により表される機能仕様の開始点における対象システムの状態である。このため、実際に検証を行う際には、イベント列（モデル・イベント列）が発生した際の対象システムの状態に前提条件が合致する抽象二分木を、高速に検索する必要がある。そこで、本実施形態では、抽象二分木の前提条件の関係を表す決定グラフを導入し、この決定グラフを用いて所定の時点における前提条件の成立判断を行う。
【００４５】
決定グラフとは、前提条件の間にある含意関係（implication）を利用して、全ての前提条件を配置したグラフである。例えば、前提条件が＜ｘ，ｙ＞、＜ｙ，ｚ＞、＜ｘ，ｙ，ｚ＞である三つの抽象二分木を考える。この場合、＜ｘ，ｙ＞および＜ｙ，ｚ＞は、＜ｘ，ｙ，ｚ＞を含意する。また、＜ｘ，ｙ＞と＜ｙ，ｚ＞に対しては、共通の前提として＜ｙ＞がある。すなわち、所定のモデル・イベント列が発生した際の対象システムの状態について＜ｙ＞が成立しない場合は、＜ｘ，ｙ＞、＜ｙ，ｚ＞、＜ｘ，ｙ，ｚ＞のいずれも成立しない。また、＜ｘ，ｙ＞が成立しない場合も、＜ｙ，ｚ＞が成立しない場合も＜ｘ，ｙ，ｚ＞は成立しない。言い換えれば、所定のモデル・イベント列が発生した際の対象システムの状態が＜ｙ＞を満たすときだけ、対象システムが＜ｘ，ｙ＞または＜ｙ，ｚ＞を満たすかを判断すれば良い。また、対象システムが＜ｘ，ｙ＞または＜ｙ，ｚ＞を満たすときだけ、対象システムが＜ｘ，ｙ，ｚ＞を満たすかを判断すれば良い。
【００４６】
図８は、上記の前提条件＜ｙ＞、＜ｘ，ｙ＞、＜ｙ，ｚ＞、＜ｘ，ｙ，ｚ＞の関係を表す決定グラフである。この決定グラフをたどることにより、無駄な検索を行うことなく、モデル・イベント列が発生した際の対象システムの状態に合致する前提条件を持つ抽象二分木を検索することができる。抽象二分木生成部１１０は、抽象二分木を生成した後、その前提条件を構造化して決定グラフを生成し、これらのデータ構造（抽象二分木および決定グラフ）を抽象二分木格納部１２０に格納する。
【００４７】
なお、本実施形態では、さらに高速な検証を実現とするため、上述したようにモデル・イベントがＩＤで表現される。抽象二分木生成部１１０は、これに対応するため、対応表格納部２００から状態遷移ＩＤの対応表と相互作用ＩＤの対応表とを取得し、イベントがＩＤで識別可能となるように、入力として与えられた相互作用仕様を変換する。この変換は、抽象二分木が生成される前に、前処理として行われる。
【００４８】
＜照合部１３０の動作の説明＞
対象システムが稼働すると、その振る舞いに応じて、プローブによりデータが取得される。取得されたデータは、データ変換部３００によりアプリケーション・モデルにおけるイベント列に変換され、照合部１３０の入力としてリアルタイムでストリーム入力として与えられる。照合部１３０は、データ変換部３００からモデル・イベント列を取得し、抽象二分木格納部１２０に格納されている抽象二分木と照合することにより、対象システムを検証する。
【００４９】
図９は、データ変換部３００から照合部１３０へ送られるモデル・イベント列のデータ構成例を示す図である。
図９に示すように、モデル・イベント列は、イベントのタスクごとに、「タイムスタンプ」、「状態機械ＩＤ（Instance ID）」、「タスクＩＤ」とイベントのＩＤ（「状態遷移ＩＤ（State Transition ID）」または「相互作用ＩＤ（Message Type ID）」）が並んで構成される。
【００５０】
図１０は、照合部１３０の動作を説明するフローチャートである。
図１０に示すように、照合部１３０は、データ変換部３００からモデル・イベント列を受け付けると（ステップ１００１）、受け付けたモデル・イベント列の開始点における対象システムの状態に前提条件が合致する抽象二分木を選択する（ステップ１００２）。次に、照合部１３０は、作業用メモリに探索空間を設定し、この探索空間に、モデル・イベント列および抽象二分木を記録する（ステップ１００３）。そして、個々のモデル・イベントごとに順次、抽象二分木とのマッチングを行う（ステップ１００４）。そして、このマッチングの結果を検証結果として出力する（ステップ１００５）。
【００５１】
ステップ１００１で受け付けたモデル・イベント列に合致する抽象二分木が存在しない場合、このモデル・イベント列が対象システムの機能仕様を逸脱することを意味する。そこで、照合部１３０は、この逸脱が検出された時点における対象システムの状態やこの状態に至るまでの振る舞いの履歴等を、マッチングの結果と共に検証結果として出力する。ステップ１００１で受け付けたモデル・イベント列に合致する抽象二分木が存在した場合は、対象システムがその機能仕様の範囲内で動作していることを意味するので、特に何も出力する必要はない。
【００５２】
リアルタイム・システムや組込みシステムでは、複数のシステム動作が並行して行われ得る。したがって、複数のイベントが同時に発生し得る。そこで、照合部１３０は、個々のモデル・イベントが発生するたびに、上記の前提条件の決定グラフを用いて成立する前提条件を求める。そして、前提条件の合致する抽象二分木がある場合は、新たな探索空間を設定し、その抽象二分木を用いた照合を行う。このように、照合部１３０は、複数の探索空間を管理することで、並列する照合（検証）を可能にする。
【００５３】
また、リアルタイム・システムや組込みシステムでは、並行動作する所定の機能やコンポーネントの動作が、外部環境やユーザ操作などに起因して停止することが起こり得る。そこで、複数の探索空間を並行に処理する場合、個々の探索空間に対して終了時間（タイムアウト）を設定可能とする。そして、所定の探索空間における処理の停止時間が終了時間を超過した場合、その探索空間での照合処理を打ち切り、探索空間が使用しているメモリ領域を強制的に解放させる。これにより、探索空間が増え続けてメモリ資源を過剰に消費することを避けることができる。照合処理を打ち切った時点で、照合中の抽象二分木の候補が残っていれば、照合は失敗したものとみなす。タイムアウト後に照合を継続する場合、後述する照合開始時点の操作と同様に、照合再開時点でのモデル・イベントの照合を行わずに、前提条件の成立判断を行ってから照合処理を開始する。
【００５４】
上述したように、対応システムが稼働すると、データ変換部３００からのモデル・イベント列は、リアルタイムで照合部１３０に送られる。したがって、対応システムが稼働している最中に照合部１３０による照合処理が開始されると、所定の機能による処理の途中であるために、どの抽象二分木にも合致しない場合が起こり得る。そこで、照合開始時点の操作として、この時点でのモデル・イベントの照合を行わずに、対象システムの状態と合致する前提条件を持つ抽象二分木が出てくるのを待つ。そして、前提条件の成立判断を行った後に照合処理を開始する。これにより、モデル・イベント列に合致する抽象二分木が存在するにも関わらず、前提条件が合致しないために誤った検出結果を出力してしまうことを回避することができる。
【００５５】
検証の目的や内容等に応じて、対象システムを構成する状態機械やシステム動作のうちで、特定のものは検証対象とならない場合がある。そこで、照合処理の高速化と誤判断の防止の目的で、ＩＤフィルタ生成部１４０により生成されるＩＤフィルタを用いる。ＩＤフィルタ生成部１４０は、フィルタリングして検証対象から外すイベントを記載したイベント・フィルタ記述（モデル・レベルのフィルタ）を取得する。そして、対応表格納部２００に格納された対応表に基づき、このイベント・フィルタ記述を、状態遷移ＩＤおよび相互作用ＩＤを記載したＩＤフィルタに変換する。
【００５６】
照合部１３０は、このＩＤフィルタに記載された状態遷移ＩＤおよび相互作用ＩＤを検証対象から外すことで、モデル・イベント列の検証対象を絞り込むことができる。例えば、所定の状態機械を検証対象から外すようにＩＤフィルタが生成されると、この状態機械における状態遷移と、この状態機械に到着するメッセージ・イベントとが検証対象から除かれる。なお、この状態機械から発信されるメッセージ・イベントは、他の状態機械の状態遷移に影響するので、検証対象からは外さない。
【図面の簡単な説明】
【００５７】
【図１】本実施形態による検証システムの機能構成を示す図である。
【図２】本実施形態で用いられるシーケンス図の例を示す図である。
【図３】本実施形態で用いられる抽象二分木の生成過程において、二分木を抽象化する例を示す図であり、シーケンス図から部分列を抽出する工程を示す図である。
【図４】本実施形態で用いられる抽象二分木の生成過程において、二分木を抽象化する例を示す図であり、部分列を重合する工程を示す図である。
【図５】本実施形態で用いられる抽象二分木の構成例を示す図である。
【図６】本実施形態で用いられる抽象二分木の生成方法を説明するフローチャートである。
【図７】図６の重合処理の手順を説明するフローチャートである。
【図８】本実施形態で用いられる決定グラフの構成例を示す図である。
【図９】本実施形態の検証システムに入力されるモデル・イベント列のデータ構成例を示す図である。
【図１０】本実施形態の照合部の動作を説明するフローチャートである。
【符号の説明】
【００５８】
１００…検証システム、１１０…抽象二分木生成部、１２０…抽象二分木格納部、１３０…照合部、１４０…ＩＤフィルタ生成部、２００…対応表格納部、３００…データ変換部
【図１】
0005324792.tif 000002
【図２】
0005324792.tif 000003
【図３】
0005324792.tif 000004
【図４】
0005324792.tif 000005
【図５】
0005324792.tif 000006
【図６】
0005324792.tif 000007
【図７】
0005324792.tif 000008
【図８】
0005324792.tif 000009
【図９】
0005324792.tif 000010
【図１０】
0005324792.tif 000011