(57)【特許請求の範囲】
【請求項１】
ステートチャートから複数の出力検査ベクトルを作成する方法であって、前記ステートチャートは、システム実行デバイスにより実行されるシステム機能の要件を指定し、かつ、複数の状態と、複数の変数と、複数の遷移とを備えており、前記複数の遷移の内少なくとも１つの遷移は、前記複数の変数の内少なくとも１つの変数に関して表現された条件を含んでおり、前記方法は、
プロセッサ、及び、データ・ストレージを準備するステップを含み、当該データ・ストレージが、当該プロセッサによって実行可能な機械語の命令を格納するものであり、当該機械語の命令の実行が、以下の方法、即ち、
前記ステートチャートを通じた順方向伝搬パスを用いて、複数の順方向到達可能遷移環境を生成するステップであって、複数の順方向到達可能遷移環境における各順方向到達可能遷移環境が、順方向伝搬パス中に、順方向に伝搬された順方向到達可能遷移に対して生成されるものと、
前記順方向伝搬パス中に、遷移が到達不可能であることを判定するステップと、
前記順方向伝搬パス中に、遷移が到達不可能であるという前記判定に応じて、前記ステートチャートを通じた逆方向伝搬パスを介して、複数の逆方向到達可能遷移環境を生成するステップであって、前記複数の逆方向到達可能遷移環境における各逆方向到達可能遷移環境が、前記逆方向伝搬パス中に伝搬された、逆方向到達可能遷移に対して生成されるものと、
前記順方向伝搬パス及び前記逆方向伝搬パス中に、遷移が到達不可能と判定するステップと、
前記順方向伝搬パス中及び前記逆方向伝搬パス中の双方において、遷移が到達不可能という前記判定に応じて、順方向伝搬及び逆方向伝搬のパスによって、不十分な数の遷移が到達されるまで、順方向伝搬と逆方向伝搬との交互のパスを実行するステップと、
前記複数の順方向到達可能遷移環境、及び、前記複数の逆方向到達可能遷移環境から、複数の出力検査ベクトルを生成するステップと、
前記複数の出力検査ベクトルを出力するステップと、
を実行させるためのものである、
方法。
【請求項２】
請求項１記載の方法において、該方法は更に、
前記複数の出力検査ベクトルにおける少なくとも１つの出力検査ベクトルに基づいて検査を実行するステップ
を備えていることを特徴とする方法。
【請求項３】
前記複数の遷移における各遷移に対して、少なくとも１つの出力検査ベクトルが生成される、請求項１に記載の方法。
【請求項４】
プロセッサと、
データ・ストレージと、
前記データ・ストレージに格納され、前記プロセッサによって実行可能な機械語命令と、
を備えた検査生成器であって、
前記プロセッサによって実行可能な機械語命令が、以下の機能、即ち、
前記ステートチャートを通じた順方向伝搬パスを用いて、複数の順方向到達可能遷移環境を生成するステップであって、複数の順方向到達可能環境における各順方向到達可能遷移環境が、順方向伝搬パス中に、順方向に伝搬された順方向到達可能遷移に対して生成されるものと、
前記順方向伝搬パス中に、遷移が到達されていないことを判定するステップと、
前記順方向伝搬パス中に、遷移が到達されていないという前記判定に応じて、前記ステートチャートを通じた逆方向伝搬パスを介して、複数の逆方向到達可能遷移環境を生成するステップであって、前記複数の逆方向到達可能遷移環境における各逆方向到達可能遷移環境が、前記逆方向伝搬パス中に伝搬された、逆方向到達可能遷移に対して生成されるものと、
前記順方向伝搬パス及び前記逆方向伝搬パス中に、遷移が到達不可能と判定するステップと、
前記順方向伝搬パス中及び前記逆方向伝搬パス中の双方において、遷移が到達不可能という前記判定に応じて、順方向伝搬及び逆方向伝搬のパスによって、不十分な数の遷移が到達されるまで、順方向伝搬と逆方向伝搬との交互のパスを実行するステップと、
前記複数の順方向到達可能遷移環境、及び、前記複数の逆方向到達可能遷移環境から、複数の出力検査ベクトルを生成するステップと、
前記複数の出力検査ベクトルを出力するステップと、
を実行するためのものである、検査生成器。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、一般的には、コンピュータ・ソフトウェアの検証に関し、更に特定すれば、ステートチャート（状態図）を用いた自動検査生成に関する。
なお、本出願は、２００７年１１月２６日に出願した米国特許出願第１１／９４５，０２１号"Requirements-Based Test Generation"（要件に基づく検査生成）に関係があり、その内容全体が、ここで引用したことにより、本願にも含まれるものとする。
【背景技術】
【０００２】
アルゴリズム実装の検証は、特にそれを証明する必要がある宇宙航空用途では過度なコストがかかっている。検証の手間及びコストの殆どは、ソフトウェア実装をその設計仕様と突き合わせて検査する際に生じ、この検証プロセスを自動化することによって、本明細書において記載する検査生成装置は、システム開発及び保証（証明）のコスト及びサイクル時間を大幅に削減することができる。
【０００３】
この検査生成の自動化は、ソフトウェア設計をステートチャートとして取り込むことが業界に普及しており慣例となっていることから可能となる。ＦＡＡが用いるＤＯ−１７８Ｂ検定規格は、コードの振る舞い(comport)を、対応するステートチャートの中に具体化した設計仕様及び下位要件によって実現した業界要件の一例である。統一モデリング言語（ＵＭＬ）仕様書には、ステートチャートの仕様を決めるための規格が含まれている。Object Management Group (OMG), OMG Unified Modeling Language Specification（オブジェクト管理グループ（ＯＭＧ）、ＯＭＧ統一モデリング言語仕様書）, version 1.5, March 1, 2003, Chapter 3, Part 9, pages 3-135〜3-154を参照のこと。ステートチャート及び同様の有限オートマトンのその他の方法及び記述も、ソフトウェア設計及び／又は要件を記述するために用いられており、とりわけ、ハレル・ステートチャート、ステート線図（状態線図）、及び有限ステート・マシーン（状態機械）が含まれる。
【先行技術文献】
【非特許文献】
【０００４】
【非特許文献１】Object Management Group (OMG), OMG Unified Modeling Language Specification（オブジェクト管理グループ（ＯＭＧ）、ＯＭＧ統一モデリング言語仕様書）
【発明の概要】
【発明が解決しようとする課題】
【０００５】
これらのステートチャートを用いて検査を生成するための現行の商用市販ツール及び技法は、構造的コードだけに適用可能である。更に、市販のツールは、ステートチャートから検査を生成するための時間を大幅に費やしてしまう。
【課題を解決するための手段】
【０００６】
本発明の第１実施形態は、ステートチャートから複数の出力検査ベクトルを作成する方法を提供する。ステートチャートは、システム実行デバイスが実行するシステム機能の要件を指定する。ステートチャートは、複数の状態と、複数の変数と、複数の遷移とを含んでいる。複数の遷移の内少なくとも１つの遷移は、複数の変数の内少なくとも１つの変数に関して表現された条件を含む。複数の遷移を順方向に伝搬するために、ステートチャートを通じての順方向伝搬パスを実行する。順方向伝搬パスの間に順方向に伝搬する遷移毎に、順方向到達遷移環境を生成する。生成した順方向到達遷移環境に基づいて、複数の出力検査ベクトルにおいて、少なくとも１つの出力検査ベクトルを作成する。
【０００７】
本発明の第２実施形態は、検査生成装置を提供する。検査生成装置は、プロセッサと、データ・ストレージと、データ・ストレージに格納されプロセッサによって実行可能な機械語命令（ＭＬＩ）とを備えている。検査生成装置は、ステートチャートを受信する。検査生成装置は、ステートチャートを通る順方向伝搬パスを用いて、複数の順方向到達可能遷移環境を生成する。検査生成装置は、順方向伝搬パスの間に伝搬した順方向到達可能遷移に対して、複数の順方向到達可能遷移環境において各順方向到達可能遷移環境を生成する。検査生成装置は、順方向伝搬パスの間に到達しなかった遷移があったか否か判断する。この判断に応答して、検査生成装置は、ステートチャートを通る逆方向伝搬パスによって、複数の逆方向到達可能遷移環境を生成することができる。検査生成装置は、逆方向伝搬パスの間に伝搬した逆方向到達可能遷移に対して、複数の逆方向到達可能遷移環境において各逆方向到達可能遷移環境を生成する。検査生成装置は、複数の順方向到達可能遷移環境及び複数の逆方向到達可能遷移環境から、複数の出力検査ベクトルを生成する。検査生成装置は、複数の出力検査ベクトルを出力する。
【０００８】
本発明の第３実施形態は、ステートチャートを通る逆方向伝搬パスを実行する方法を提供する。ステートチャートは、システム実行デバイスが実行するシステム機能の要件を指定する。ステートチャートは、複数の状態と、複数の変数と、複数の遷移とを備えている。複数の遷移の内少なくとも１つの遷移は、複数の変数の内少なくとも１つに関して表現した条件を含む。不達遷移リストから、候補逆方向到達可能遷移（ＣＢＲＴ）を読み出す。関連するタイムステップ−シーケンス・オブジェクト（ＡＴＳＯ）を生成する。ＡＴＳＯは、ＣＢＲＴと関連付けられている。読み出したＡＴＳＯの完全−制約式を満たすか否か判断する。読み出したＡＴＳＯの完全−制約式を満たすという判断に応答して、ＣＢＲＴ環境を逆方向到達遷移として更新する。
なお、本明細書では、実施形態の様々な例について、図面を参照しながら説明する。図面においては、同様の参照番号は同様のものを示すこととする。
【図面の簡単な説明】
【０００９】
【図１】本発明の実施形態によるシステム開発プロセスの一例のフローチャートである。
【図２】本発明の実施形態によるステートチャートの一例である。
【図３】本発明の実施形態による、接合部を有するステートチャートの一例である。
【図４】本発明の実施形態による、計算機の一例である。
【図５】本発明の実施形態による、ある環境についてのデータ構造の一例の模式図である。
【図６】本発明の実施形態にしたがって、ステートチャートに対して検査ベクトルを生成する方法の一例のフローチャートである。
【図７】本発明の実施形態にしたがって、順方向伝搬パスを実行する方法の一例のフローチャートである。
【図８】本発明の実施形態にしたがって、逆方向伝搬パスを実行する方法の一例のフローチャートである。
【図９】本発明の実施形態による方法の一例のフローチャートである。
【図１０】本発明の実施形態による、図３に示したステートチャートに対する複数の出力検査ベクトルの人間が読み取り可能な形態の一例である。
【発明を実施するための形態】
【００１０】
本発明は、ステートチャートを用いて設計し、コンピュータ・ソフトウェア、ファームウェア、及びハードウェアの組み合わせで実現するシステムの開発及び検証に関する。尚、本明細書において記載するこの構成及びその他の構成は、一例として記載するに過ぎないことは言うまでもない。他の構成や要素（例えば、機械、インターフェース、機能、順序、機能の集合体等）も代わりに用いることができ、いくつかの要素は纏めて省略してもよいことは、当業者には明らかであろう。更に、本明細書において記載する要素の多くは、機能的実体であり、離散コンポーネント又は分散コンポーネントとして、あるいは他のコンポーネントと一緒に、適した組み合わせ及び場所であれば、任意に実現することができる。本明細書において記載する種々の機能は、１つ以上の実体（エンティティ）によって実行する場合、ハードウェア、ファームウェア、及び／又はソフトウェアによって実行することができる。種々の機能は、メモリに格納した命令をプロセッサが実行することによって遂行することができる。
【００１１】
全体像
本発明は、ソフトウェア及びハードウェアの組み合わせで最終的に実現するシステムについて要件を指定するステートチャートを用いた検証に関する。本発明は、システム機能を実行するシステム・パフォーマンス・デバイス（例えば、コンピュータ・プロセッサ）の挙動の要件を指定するステートチャート上で動作する。システム機能の例は、航空機、電動車両、又はその他の機械的デバイスの一部であるセンサ（例えば、空気流量センサ、温度センサ、及び燃料流量センサ）を制御し、衛星信号のような種々の入力をナビゲーション・システムの一部として分析し、航空機の制御面又はその他の部分を動作させ、そして、ユーザ入力及び／又は出力を処理することである。多くのその他のシステム機能も可能である。
【００１２】
ステートチャートとは、決定論的有限オートマトン（ＤＦＡ）のグラフ又は線図とすることができる。したがって、ステートチャートは、複数の状態を備えており、その各々が、システム機能を実行するシステム実行デバイスの条件を記述する。また、ステートチャートは複数の遷移も備えており、その各々はソース（原始）状態からデスティネーション（宛先）状態への経路を示す。各遷移は、１つ以上の条件を備えることができる。条件とは、その遷移を越える前に満たさなければならない必要条件である。したがって、条件は、システム実行デバイスの挙動の要件をモデル化することができる。例えば、ステートチャートは「入力待機」状態及び「入力受信」状態を有することができる。「入力待機」状態と「入力受信」状態との間の遷移は、「空でない入力バッファ」のような条件を有することができる。「入力待機」状態から「入力受信」状態への遷移を越えることができる前に、「空でない入力バッファ」という条件を満たさなければならない。
【００１３】
各状態は、１つ以上のステートチャート定義変数を指定する。変数は、値を格納するためにステートチャートの中で用いられる。例えば、ステートチャートの変数「ｘ」は、整数値「３」等の値を格納することができる。ステートチャートは、１つ以上のステートチャート入力変数、即ち、システム機能を実行する前にデバイスに供給する値、及び１つ以上のステートチャート出力変数、即ち、システム機能を実行した後にシステムが出力する値を備える。各条件は、ステートチャート定義変数、ステートチャート入力変数、及び／又はステートチャート出力変数に関して表現することができる。
【００１４】
目的は、システム実行デバイスの実行により、ステートチャートの中に具体化されている要件を満たすことを検証することである。この目的を達成するために、検査生成装置を用いるとよい。好ましくは、ＮＪ、MorristownのHoneywell International, Incが供給するHoneywell Integrated Lifecycle Tools and Environment (HiLiTE) コンピュータ・ソフトウェア・パッケージである。
【００１５】
検査生成装置は、検査ベクトルを生成することにより、ＤＯ−１７８Ｂの目的を満たすことを促進する。検査生成装置は、ステートチャートにおいて具体化される要件に該当する(cover)複数の出力検査ベクトルを生成する。ステートチャート入力変数の順方向伝搬をステートチャートの遷移と共に用いる第１パスを実行する。第１パスの間に横断する遷移毎に、順方向到達可能遷移環境が生成される。
【００１６】
第１パスがいずれかの遷移を横断できなかった場合、ステートチャートを通る逆方向伝搬パスを実行して、複数の遷移を逆方向に伝搬させる。逆方向伝搬パスは、逆方向伝搬パスの間に伝搬する遷移毎に、逆方向到達可能遷移環境が生成される。次いで、生成した順方向到達可能遷移環境及び逆方向到達可能遷移環境から、複数の出力検査ベクトルが生成される。
【００１７】
順方向伝搬パス及び逆方向伝搬パスを組み合わせて実行することもできる。順方向伝搬パス、逆方向伝搬パス、又は順方向伝搬パス及び逆方向伝搬パスの組み合わせの１回以上の繰り返しを実行することもできる。順方向伝搬パス、逆方向伝搬パス、又は順方向伝搬パス及び逆方向伝搬パスの組み合わせの繰り返しは、（ａ）モデルにける全ての遷移を伝搬するまで、（ｂ）順方向伝搬経路及び逆方向伝搬経路双方によって新たな検査が生成されなくなるまで、又は（ｃ）固定回数の繰り返しを実行し終えるまで（例えば、順方向伝搬パス及び逆方向伝搬パスの組み合わせの組み合わせの１回の繰り返し）実行することができる。
【００１８】
検査ドライバ又は検査ハーネスのような、自動検査システムは、これらの検査ベクトルを用いて、ステートチャートに具体化した要件を検証することができる。要件は、システム実行デバイスを検査する検査ドライバによって検証することができる。アプリケーション開発者は、ＤＯ−１７８Ｂの目的を満たすために、現在ではコストのかかる検査手順や手動検査生成を用いているが、このプロセスの自動化は、検証に必要な時間やリソースを劇的に削減することができる。あるいは、検査ベクトルから、人が読み取ることができる検査を生成し、検査者がシステム実行デバイスを検査してもよい。
【００１９】
順方向伝搬及び逆方向伝搬を一緒に用いると、様々な利点が得られる。順方向伝搬パスは、逆方向伝搬パスよりも実行に要する時間が短くて済む。更に、順方向伝搬パスは、多くのステートチャートにおいて完全なカバレッジ(coverage)（即ち、全ての遷移に対して検査ベクトルを生成する）が得られる。次いで、順方向伝搬パスの間に到達しなかった遷移に対して検査ベクトルを生成するために、逆方向伝搬パスを用い、多くのステートチャートに対して順方向伝搬パスのみの場合よりも、更に完全なカバレッジを確保する。順方向伝搬及び逆方向伝搬の双方を用いると、（ａ）順方向伝搬のみを用いる場合よりも多い数のステートチャートについて完全なカバレッジを確保し、（ｂ）逆方向伝搬のみの場合よりも速く検査ベクトルを生成することによって、システム実行デバイスの検証をし易くすることができる。より短い時間でより多くのステートチャートに対して完全なカバレッジを確保することにより、システム実行デバイスの要件全ての完全なカバレッジを必要とする検証の手間が省ける。
【００２０】
完全なカバレッジを得ることと共に、順方向伝搬及び逆方向伝搬を用いると、順方向伝搬及び／又は逆方向伝搬によって到達する遷移の数、実現不可能な保護条件（即ち、１＞２の任意の値の選択によっても満たすことができない条件）、０による除算の潜在的可能性というような危うい演算、状態による変数の範囲制約、並びに逆方向到達可能遷移に到達する前に横断した遷移に関する情報というような、ステートチャートの詳細な分析を行うことができる。
【００２１】
また、検査生成装置は、モデルのステートチャート指針に対する順応性を判定するために、ステートチャートのチェックを行うこともできる。例えば、ステートチャートの指針が、ステートチャートにおける各状態Ｓが少なくとも１つの「出立」遷移（即ち、状態Ｓにおいて始まる、２つの状態間の遷移）を有することを必要とする場合、検査生成装置は、ステートチャートにおける各状態がステートチャート指針を遵守しているか否か判断する。
【００２２】
システム開発プロセス全体の一例
図１は、本発明の実施形態によるシステム開発プロセスの一例のフローチャートである。ブロック１００において、開発者は課題（例えば、航空機の特定の形式の操舵制御システムの必要性）を特定し、その課題を解決するために上位機能要件を指定する。上位機能要件は、課題に対する解決策を１つ以上のシステム機能に分割することができる。
【００２３】
これに応じて、開発者は、恐らくは開発者のチームとの共同作業において、ブロック１１０において１つ以上のシステム設計モデルの設計を進める。ブロック１１０の結果、ブロック１００において指定された課題を部分的に又は全面的に解決するシステム機能を実行するためのシステム実行デバイス（又は複数のデバイス）を記述するシステム設計モデルが得られる。システム実行デバイスは、１つ以上のコンピュータ・プロセッサ上で実行するコンピュータ・ソフトウェアとして表現することができる。システム設計モデルは、ステートチャートとして表現することもできる。
【００２４】
ブロック１２０において、開発者によって手動で、又はステートチャートを実現することが可能なコンピュータ・プログラムによって自動的に、システム設計モデルを表すステートチャートから、コードを生成することができる。Simulink（登録商標）コンピュータ・プログラムを、恐らくはStateflow（登録商標）コンピュータ・プログラムと組み合わせて用いると、ステートチャートを実現することができる。ＭＡ、NatickのMathWorks, Inｃ.は、Simulink（登録商標）及びStateflow（登録商標）コンピュータ・プログラムの双方を生産する。ステートチャートは、他のコンピュータ・プログラムを用いることによってというように、他の方法でも実現することができる。
【００２５】
ブロック１３０において、通常は航空制御システムに対するＦＡＡ指令ＤＯ−１７８Ｂ規格のような、業界標準目的に応じて、ステートチャートを検証する。証明目的の厳しさのために、ブロック１３０は時間及びシステム・リソースの双方について費用が嵩む傾向がある。ＤＯ−１７８Ｂ規格では、完全なカバレッジを要求し、検査事例のランダム又は疑似ランダム生成を完全には認識しない。既存の検査生成プログラムは完全な検査事例集合を生成できないので、開発者及び検査者は、コードがＤＯ−１７８Ｂ規格を満たすことを証明する検査事例を手動で生成することを強いられる。完全なシステム検査を遂行した後でなければ、ブロック１４０においてシステム実行デバイスを検証することができない。最後に、ブロック１５０において、証明されたシステム実行デバイスを工業的に展開する。例えば、操舵制御システムを航空機のアヴィオニクスに組み込むことができる。
【００２６】
ステートチャートの例
ステートチャートは、一般に、センサ・コントローラ、飛行制御、エンジン制御、及び操舵システムのような、システム実行デバイスの一部に必要な特定的な挙動セマンティクスを定義するために用いられる。これらの挙動セマンティクスは、繰り返し、１つ以上の時間ステップにおいて、システムの動作寿命の間実行するように設計しなければならない。検査事例生成の目的は、システム実行デバイスが、１つ以上のシステム設計モデルによって指定されたアルゴリズムが正しく実施されるかどうかを検証することである。
【００２７】
図２は、本発明の実施形態によるステートチャート２００の一例である。図示のように、ステートチャートは複数の状態を備えており、その各々がシステムのモードを記述する。更に、ステートチャートは、状態間での複数の遷移と、複数の遷移に対応する複数の条件とを備えている。図２が示すステートチャート２００は、初期状態２１０及び２３６、StartState状態２１６、SecondState状態２２０、ParentState状態２３０、ChildState1状態２４０、Childstate2状態２５０、ChildState3状態２６０、ChildState4状態２７０、及び最終状態２８０を有する。状態には、名称が付けられるか、番号が付けられるか、又は名称及び番号の双方が付けられている。図２に示すように、状態には名称が付けられており、状態の名称は、斜字体フォントのStartStateで示されている。
【００２８】
状態は、１つ以上の「入口アクション」及び１つ以上の「出口アクション」を有することができる。入口アクションとは、システム実行デバイスが状態に入るときに実行する動作である。図２は、状態の入口アクションを、項「entry:」の後ろかつ項「exit:」又は項「during」の前に来るように図示している。例えば、ChildState3状態２６０は、「oState=3；」の入口アクションを実行する。出口アクションは、状態を離れるときに行われる動作である。図２は、項「exit:」に続くように、状態の出口アクションを示している。例えば、ChildState3状態２６０は、「oState=oState+1」の出口アクションを有する。条件及び／又は遷移アクションは、遷移上のアクションとして指定することができる（以下で説明する）。
【００２９】
また、状態は、イベントに応答して横断する出立遷移がない場合、オブジェクトによって実行する「最中アクション」(during actions)を有することもできる。図２は、ある状態の最中アクションを、項「during:」の後ろかつ項「exit:」の前に来るように示している。例えば、ChildState4状態２７０は、「count=count+1」の最中アクションを有する。
【００３０】
１つ以上の「イベント」が、システム実行デバイスに対して行われてもよい。イベントとは、システム実行デバイスにとって注目すべき出来事である。イベントは、状態間の遷移及びアクションをトリガすることができる。例えば、図２におけるステートチャートは、SecondState状態２２０がアクティブである間に、遷移２２２をトリガするか又は遷移２２６をトリガすることによって、イベントに応答することができる。イベントは、同期（即ち、指定時刻に行われる）又は非同期（即ち、指定時刻には行われない）のいずれかに分類することができる。非同期イベントを「信号」とも称する。
【００３１】
例えば、システム実行デバイスがセンサからの入力を待機しており、入力を待機している間に、システム実行デバイスが、１分のタイマ満了時にメッセージを送ると仮定する。１分タイマの満了は、同期イベントである。しかしながら、システム実行デバイスが最終的にセンサから入力を受信した場合、センサからの入力受信は非同期イベントであり、したがって信号と呼ぶことができる。信号は、誤り事例（即ち、無効入力データ又はソフトウェア内部において期待されていない条件によって発生したハードウェア異常又はソフトウェア「例外」）、及び入力／出力動作（即ち、センサ・データ、キー押圧、データのパケット、マウス・クリック、又は画面上における文字表示による通知を受信する））のような種々のイベントをモデル化するために用いることができる。他のイベントも信号としてモデル化することもできる。
【００３２】
イベントは、イベント・タイプを有することもできる。イベント・タイプは、イベントのソース、優先順位、又はタイミングというような、イベントの意味的固有性(semantic property)を示す。例えば、イベント・タイプは、「５」の値が、空気圧力センサからのセンサ読み取り値から来たこと、室内圧力読み取り値の５点メモリ上の「５」の優先順位、又は最後の読み取りが５秒前に行われたことを示す。
【００３３】
状態は、「親状態」又は「複合状態」として知られるものでもよい。親状態は、２つ以上の並列な又は相互に排他的な副状態、即ち、「子状態」を備えることもある。図２は、ParentState状態２３０を複合状態として示す。ParentState状態２３０は、４つの副状態、ChildState1状態２４０、ChildState2状態２５０、ChildState3状態２６０、及びChildState4状態２７０を備えている。ある状態に入るとき（例えば、子状態）、その状態及びその状態の親状態は全てアクティブになる。状態から出るとき（例えば、親状態）、その状態及びその状態の子状態は全てインアクティブになる。
【００３４】
２つの特殊状態を定義することもできる。初期状態とは、ステートチャート又は複合状態の入口（又は最初の）状態である。最終状態とは、ステートチャートの出口（又は最後の）状態である。ステートチャートに対して初期状態を定義すると、そのステートチャートを通る全ての経路は初期状態において始まらなければならない。複合状態に対して初期状態を定義すると、その複合状態に入る全ての経路は、当該複合状態に対して定義した初期状態において開始しなければならない。ステートチャートに対して最終状態を定義すると、そのステートチャートから出る全ての経路は最終状態において終了しなければならない。図２は、ステートチャート２２０の初期状態として定義した初期状態２１０と、ParentState状態２３０の複合状態に対する初期状態として定義した初期状態２１４と、最終状態２８０とを示す。
【００３５】
図２は、初期状態２１０及び２３６を実線の円で示し、最終状態２８０を、細い輪で囲んだ実線の円で示している。尚、初期状態２１０はステートチャートの初期状態であり、一方、初期状態２３６は複合状態（ParentState状態２３０）の初期状態である。初期状態及び／又は最終状態を含む状態の他の図示も可能である。多数の初期状態及び／又は多数の最終状態を定義することもできる。図２は、２つの初期状態２１０及び２３６の例を示している。
【００３６】
１つ以上の変数を定義して、ステートチャートにおいて用いると、システム実行デバイスによって実行するシステム機能のモデリングをし易くすることができる。変数は、値を格納すると定義することができる。一般に、変数は、整数型、実数型、文字型、ブール型、文字群に対する文字列型（例えば、「abc」は３つの文字の文字列である）、整数又は実数群に対するアレイ型等というような、タイプを有するように定義することができる。変数には値を割り当てることができる。即ち、変数は所与の量又は属性で指定することができる。例えば、図２は、ChildState3状態２６０において「oState=3;」の割り当てを示し、これは、「oState」変数に対して「３」の値を指定している。変数のタイプは、変数に割り当てることができる値を制限することができる。例えば、「Cash」と称する変数の値は実数型であると仮定する。すると、「Cash=40.00;」という割り当ては、変数Cashのタイプに応じて有効であるが、「Cash='abc';」という割り当ては、Cashのタイプに応じて無効となる。何故なら、「abc」は実数ではないからである。変数の値には単位を付随させることもできる。例えば、３の値は、３ミリ秒、３メートル、又は３リットルを表すことができる。
【００３７】
第１変数、値、又はその組み合わせが、第２変数、値、又はその組み合わせよりも大きいこと、以上であること、未満であること、以下であること、等しいこと、等しくないことを判定するというようなことのために、変数について比較を行うことができる。比較は、条件を示すために用いることもできる。例えば、条件２５４は、countが１よりも大きいか否か判定するための変数「count」と値「１」との比較を示す。別の一例として、条件２６４は、in1が０に等しくないか否か判定するための変数「in1」と値「０」との比較を示す。
【００３８】
比較は、あるイベントがある種のタイプであるか否か、イベントがあるイベント・クラスであるか否か、又はあるイベントの値が所与のイベント・タイプに対して有効か否か判定するというようなことのために、イベント・タイプについて行うこともできる。例えば、検査生成装置がイベント・タイプ「キーボード入力」及び「５」の値が発生したと判断した場合、イベント・タイプを（ａ）「キーボード入力」のイベント・タイプ、（ｂ）「ユーザ入力」、「ユーザ入力／出力動作」、又は（ｃ）「キーボード入力」のイベント・タイプに基づく有効な入力タイプと比較して、一致が得られる。同じ例について、イベント・タイプを（ａ）「表示動作完了」又は「ネットワーク入力」のイベント・タイプ、あるいは（ｂ）「センサ入力」又は「圧力読み取り値」のようなイベントのクラスと比較して、一致が得られない。
【００３９】
変数は、これらがステートチャートにおいてどこで用いられるかに応じて分類することができる。１つ以上の「ステートチャート入力変数」は、ステートチャートに入る前及び／又はいずれかの又はあらゆるイベントのブロードキャスト（即ち、イベントの通知）の間に定義すること、及び／又は設定することができ、１つ以上の「ステートチャート出力変数」は、任意のイベントの効果を決定した後に調べることができ、更に１つ以上の「ステートチャート定義変数」はステートチャートの任意の状態において指定することができる。例えば、図２は、条件２３４がステートチャート入力変数として定義された、「in2」と称する変数を含むことを示す。所与のステートチャートのステートチャートステートチャート入力変数の値は、ユーザ入力、所与のステートチャートと調和する１つ以上の他のステートチャート、格納値、又はその他の何らかの情報源というような、別のソースから来てもよい。ステートチャート入力変数は、値が特に指定されていない場合には、デフォルト値を有することもできる。尚、所与のステートチャートのステートチャート出力変数は、所与のステートチャートのステートチャート入力変数の全て、一部を含むことができ、全く含まないこともある。
【００４０】
言い換えると、ステートチャートによって指定されるシステム設計モデルが「システム機能を実行するために「ブラック・ボックス」システム実行デバイスを記述し、イベントが、当該ブラック・ボックスに対して、タイプによって分類することができる発生(occurrence)を示す場合、ステートチャート入力変数は、いずれのイベントの発生時又は発生前にでも指定され、ブラック・ボックス内においてステートチャート定義変数を用いてシステム機能を実行し、ブラック・ボックスを実行し、発生したあらゆるイベントの効果を処理した後に、ステートチャート出力変数を調べる。
【００４１】
全ての変数は、ステートチャート内部における「範囲」即ち可視性(visibility)を有する。ステートチャート入力変数及びステートチャート出力変数の範囲は、ステートチャートのレベルに位置する。ステートチャート定義変数は、ステートチャートのレベルでの範囲を有することができ、あるいはいずれかの状態又は副状態のレベルでの範囲を有することもできる。
【００４２】
ステートチャートは、複数の遷移を備えており、その各々は「ソース状態」から「宛先」状態への経路を示す。遷移の方向はソース状態から宛先状態（即ち、矢印の方向）となる。遷移をソース状態から宛先状態に横断する場合、遷移を順方向に横断すると言い、遷移を宛先状態からソース状態に横断する場合、遷移を逆方向に横断すると言う。
【００４３】
本明細書において記載するステートチャートでは、遷移は「単一方向性」即ち一方向であり、したがって、状態間において「双方向性」即ち二方向遷移をモデル化するには、２つの単一方向性遷移（１つはソースからデスティネーションへ、もう１つはデスティネーションからソースへ）を用いる。遷移２２２は、SecondState状態２２０に矢尻がある矢印として示されており、SecondState２２０が遷移２２２のソース状態であることを示し、ParentState状態２３０に矢印の鋭端があり、ParentState状態２３０が遷移２２２のデスティネーション状態であることを示す。しかしながら、双方向遷移があるステートチャートを有することも可能である。他の遷移の図示も可能である。
【００４４】
遷移は、（１）ある状態がアクティブになったとき、（２）あるイベントが発生したとき、（３）あるイベント・タイプを有する（又はあるイベント・タイプのクラスに該当する）イベントが発生したとき、及び／又は（４）ある条件を満たしたときに、「発生」(fire)した（即ち、ファイアーした又は横断した）と言われる。条件とは、比較のように、遷移を横断する前に満たさなければならない要件である。条件は、ステートチャート定義変数、ステートチャート入力変数、ステートチャート出力変数、及び／又はイベント・タイプに関して表現することができる。したがって、条件は、システム実行デバイスの挙動の要件をモデル化することができる。図２は、遷移２２２を示し、「in1!=0」の条件２２４が、遷移２２４を横断できるようになる前に変数「in1」が０に等しくないと判断するという要件として作用する。また、条件を「保護」(guard)又は「保護条件」と呼ぶ場合もある。図２は、条件２５４及び２６４を示し、ChildState1状態２４０のソース状態を離れる遷移に対する保護条件として作用する。
【００４５】
遷移は条件を有さなくてもよく、したがって、遷移の条件がない場合でも横断できる場合もある。図２は、条件のない遷移２７２を示し、したがって、条件を全く満たすことなく、横断することができる。条件のない遷移は、一旦遷移のソース状態に達し、イベントが発生すれば横断することができる。例えば、図２は、一旦ChildState1状態２４０に達すると、その後ChildState4状態２７０に達するイベントが発生したときに横断することができる。
【００４６】
条件が未定義変数（即ち、ステートチャート定義変数、ステートチャート入力変数、又はステートチャート出力変数のいずれでもない変数）を利用する場合、ステートチャートの中に「仕様誤り」がある場合もある。仕様誤りには種々のタイプがある。
【００４７】
遷移には優先順位を付けるとよい。例えば、状態Childstate1２４０は３つの出力遷移２５４、２６２、及び２７２を有する。これらの遷移全ての条件が真である場合、優先順位が高い遷移が生じて、優先順位が低い遷移は生じない。優先順位は、優先順位規則を用いて割り当てるとよい。優先順位規則の一例は、ある状態を中心に時計回り方向に移動することによって優先順位を遷移に割り当て、最高の優先順位の遷移を１２：００の時計の針の位置とするとよい。したがって、遷移２５４の優先順位は、遷移２６２よりも高い。他の多くの優先順位規則も可能である。優先順位は、明示的に規定してもよい。例えば、遷移２５４が最低の優先順位を有し、遷移２６２が中間の優先順位を有し、遷移２７２が最高の優先順位を有する。優先順位は、数値による格付けを用いて規定してもよく、その場合、数値が小さい程又は大きい程、高い優先順位を意味し、あるいは分類用語（高、中間、又は低）を用いて、あるいは他の手段によって規定してもよい。
【００４８】
「伝搬」という用語は、本明細書において用いる場合、ステートチャート内において「しかるべき方向」に所与の遷移を横断させて、所与の遷移を横断するときに到達したいずれの変数又はそれ以前に到達したいずれの変数のいずれの値をも前方に搬送し、前方に搬送した値に基づいて所与の遷移のいずれの条件をも満たすことを意味する。「順方向伝搬」という用語は、しかるべき伝搬方向が所与の状態（例えば、初期状態）から順方向であることを意味する。逆に、「逆方向伝搬」という用語は、所与の状態（例えば、所与の遷移の宛先状態）から逆方向であることを意味する。
【００４９】
「到達可能な遷移」とは、遷移のいずれの（保護）条件をも満たしつつ、所与の到達状態からしかるべき方向に伝搬することができる遷移のことである。順方向到達可能遷移とは、所与の到達状態から順方向に伝搬することができる遷移である。同様に、逆方向到達可能遷移とは、所与の到達状態から逆方向に伝搬することができる遷移である。
【００５０】
経路は、ステートチャート全体で取ることができる。ステートチャートを通る経路は、開始状態において開始し、１つ以上の遷移を横断し、終了状態において終了する。例えば、SecondState状態２２０の開始状態からChildState3状態２６０への経路は、遷移２２２、２３２、及び２６２を横断することを伴うと考えられる。経路は開いていても閉じていてもよい。開いた経路とは、開始状態が終了状態とは同じでない経路である。逆に、閉じた経路とは、開始状態が終了状態と同じ経路である。例えば、SecondState状態２２０からSecondState状態２２０へ、遷移２２６を経由する閉じた経路がある。ステートチャートはサイクルを有することもできる。サイクルとは、状態の繰り返しが許される、ステートチャートを通る閉じた経路である。
【００５１】
図３は、本発明の実施形態による、接合部３１０を有するステートチャート３００の一例である。図３が示すステートチャート３００には、State1状態３３０、State1_1状態３３２、State1_1_1状態３３４、State2状態３４０、State2_1状態３４２、State2_2状態３４４、State3状態３５０、State4状態３６０、及びState5状態３７０、ステートチャート入力変数in1、並びにステートチャート出力変数out1がある。図３は、ステートチャート３００の中にある状態の名称を斜字体フォントで示している。
【００５２】
ステートチャートは、１つ以上の接合部を備えることができる。接合部によって、仲介状態を横断せずに、遷移を１つの経路に纏めることが可能となる。図３は、接合部３１０に入る遷移３２０、状態３３０〜３７０のような、仲介状態を横断せずに、接合部３１０から出立する遷移３２２及び３２４を示す。図３は、接合部３１０を、ステートチャート３００における小さな楕円として示している。接合部の他の図示も可能である。
【００５３】
「遷移セグメント」とは、接合部に入る遷移又は接合部から出る遷移である。図３は、接合部３１０に入る遷移セグメント３２０と、接合部３１０から出る遷移セグメント３２２及び３２４を示す。接合部は、入来する遷移セグメントを出立する遷移セグメントと論理的に接合することができる。図３は、遷移セグメント３２０及び３２４を、State4状態３６０からState2状態３４０への１つの論理遷移に論理的に接合する接合部３１０を示す。また、同じ接合３１０が、遷移セグメント３２０〜３２２を、State4状態３６０からState4状態３６０への１つの論理遷移に論理的に接合する。接合部を含むステートチャートは、遷移セグメント間にサイクルが存在する場合には、無限の論理遷移を有する場合もある。
【００５４】
複合状態に対する初期状態も、接合部として機能する場合がある。図２に示すように、初期状態２３６は、遷移２２２のような、複合状態に入る遷移と、遷移２３２のような初期状態から離れる複合状態内の遷移との間における接合部として機能する。
【００５５】
計算機の一例
図４は、本発明の実施形態による計算機４００の一例のブロック図であり、演算装置４１０、データ・ストレージ４２０、ユーザ・インターフェース４３０、及びネットワーク通信インターフェース４４０を備えている。計算機４００は、デスクトップ・コンピュータ、ラップトップ又はノートブック・コンピュータ、パーソナル・データ・アシスタント（ＰＤＡ）、移動体電話機、あるいは本明細書において記載する方法６００及び／又は本明細書において記載する検査生成装置及び／又は検査ドライバの機能性の少なくとも一部を実現するコンピュータ命令を実行可能な演算装置を搭載している同様のデバイスであればいずれでもよい。
【００５６】
演算装置４１０は、１つ以上の中央演算装置コンピュータ・プロセッサ、移動体プロセッサ、ディジタル信号プロセッサ（ＤＳＰ）、マイクロプロセッサ、コンピュータ・チップ、及び現在知られている又は今後開発される同様の演算装置を含むことができ、機械語命令を実行し、データを処理することができる。
【００５７】
データ・ストレージ４２０は、１つ以上の記憶装置を備えることができる。データ・ストレージ４２０は、リード・オンリ・メモリ（ＲＯＭ）、ランダム・アクセス・メモリ（ＲＡＭ）、リムーバブル・ディスク・ドライブ・メモリ、ハード・ディスク・メモリ、磁気テープ・メモリ、フラッシュ・メモリ、ならびに現在知られている同様の記憶装置及び今後開発される同様の記憶装置を含むことができる。データ・ストレージ４２０は、少なくとも、１つ以上のステートチャート４２２、データ構造４２４、及び機械語命令４２６を収容するのに十分な記憶容量を備えている。データ構造４２４は、任意の環境において、リスト、状態及び／又は遷移の印(marking)、ベクトル（マルチステップ・ベクトル及び出力検査ベクトルを含む）、人間読み取り可能形態、印、ならびに本明細書において記載する検査生成装置、本明細書において記載する検査ドライバの機能の一部又は全部を実行するため、及び／又は方法６００、７００、８００及び／又は９００に記述されている手順の一部又は全部を実行するために必要な、本明細書において記載するあらゆるデータ構造をも備えている。データ・ストレージ４２０に収容される機械語命令４２６は、本明細書において記載する検査生成装置、本明細書において記載する検査ドライバの機能の一部又は全部を実行するため、及び／又は方法６００、７００、８００及び／又は９００に記述されている手順の一部又は全部を実行するために演算装置４１０によって実行可能な命令を含む。
【００５８】
ユーザ・インターフェース４３０は、入力ユニット４３２及び／又は出力ユニット４３４を備えることができる。入力ユニット４３２は、計算機４３０のユーザからユーザ入力を受け取ることができる。入力ユニット４３２は、キーボード、キーパッド、タッチ・スクリーン、コンピュータ・マウス、トラック・ボール、ジョイスティック、及び／又は、計算機４３０のユーザからユーザ入力を受け取ることが可能な、現在知られている又は今後開発されるその他の同様のデバイスを備えることができる。出力ユニット４３４は、計算機４３０のユーザに出力を供給することができる。出力ユニット４３４は、１つ以上の陰極線管（ＣＲＴ）、液晶ディスプレイ（ＬＣＤ）、発光ダイオード（ＬＥＤ）、ディジタル光処理（ＤＬＰ）技術を用いたディスプレイ、プリンタ、光バルブ、及び／又は、グラフィック情報、テキスト情報、及び／又は数値情報を計算機４００のユーザに表示可能な、現在知られている又は今後開発される同様のデバイスを備えることができる。
【００５９】
ネットワーク通信インターフェース４４０は、データを送出及び受信するように構成されており、有線通信インターフェース及び／又は無線通信インターフェースを含むことができる。有線通信インターフェースが設けられている場合、ワイヤ、ケーブル、光ファイバ・リンク又はワイド・エリア・ネットワーク（ＷＡＮ）、ローカル・エリア・ネットワーク（ＬＡＮ）、インターネットのような１つ以上の公衆データ・ネットワーク、１つ以上の個人データ・ネットワーク、又はこのようなネットワークのあらゆる組み合わせへの同様な物理的接続を備えることができる。無線通信インターフェースが設けられている場合、ＷＡＮ、ＬＡＮ、１つ以上の公衆データ・ネットワーク（例えば、インターネット）、１つ以上の個人データ・ネットワーク、あるいは公衆及び個人データ・ネットワークのあらゆる組み合わせに対する、ＩＥＥＥ８０２．１１（例えば、Ｗｉ−Ｆｉ）インターフェースのような、エア・インターフェースを利用することができる。
【００６０】
環境に対するデータ構造の一例
図５は、本発明の実施形態による、環境５００に対するデータ構造の一例の模式図である。環境５００は、１組のアクティブ状態、１組の現在値、及び／又はステートチャートの「スナップショット」を記録するためのマルチステップ・ベクトルを備えることができる。ステートチャートのスナップショットとは、ステートチャートにおける対象の状態に到達するために必要な全ての値、及びその対象の状態に到達するために取る経路の集合体である。図５が示す環境５００は、１組のアクティブ状態５１０、１組の現在値５２０、及びマルチステップ・ベクトル５３０を示す。１組のアクティブ状態５１０は、現在アクティブである１つ以上の状態を備えることができる。１組の現在値５２０は、１つ以上のステートチャート入力、ステートチャート出力、及び／又はステートチャート定義変数に対する値を備えることができる。１つ以上のステートチャート入力、ステートチャート出力、及び／又はステートチャート定義変数に対する値の各々は、１つ以上のスカラー値、１つ以上の値の範囲、及び／又はスカラー値と値の範囲との組み合わせを含むことができる。
【００６１】
マルチステップ・ベクトルは、ステートチャート全体にわたるステップの整列リストを表すことができ、各ステップはアクティブ状態及び値を有する。ステップの整列リストを表すために、マルチステップ・ベクトルは、ステートチャートを通過する経路を記録するために、過去状態リスト、過去遷移リスト、及び／又は１組の既定状態(previous state)を備えることができる。図５が示すマルチステップ・ベクトル５３０は、過去状態リスト５３２、過去遷移リスト５３４、及び１組の既定状態５３６を有する。過去状態リスト５３２は、ステートチャートを通過する経路において以前に到達した１つ以上の状態を含むことができる。過去状態リスト５３２が空である場合、環境５００によって表される経路はこれまでにいずれの状態にも到達していないという可能性がある。即ち、環境５００は初期状態を表す。過去遷移リスト５３４は、ステートチャートを通過する経路において以前に横断した１つ以上の遷移を含むことができる。過去遷移リスト５３４が空である場合、環境５００によって表される経路は、これまでにいずれの遷移も横断していないという可能性がある。即ち、環境５００は初期状態を表す。
【００６２】
１組の既定値５３６は、１つ以上の変数の各々について、１つ以上の変数値を含むことができる。１組の既定値は、ステートチャート入力、ステートチャート出力、及び／又はステートチャート定義変数に対する変数値を含むことができる。１つ以上のステートチャート入力、ステートチャート出力、及び／又はステートチャート定義変数の変数値の各々は、１つ以上のスカラー値、１つ以上の値の範囲、及び／又はスカラー値と値の範囲との組み合わせを含むことができる。１組の既定値５３６における各変数値には、期間(duration)を関連付けることができる。変数値と期間との間の関連は、変数が、期間によって示される数の後続イベントの間変数値を有することを示すことができる。
【００６３】
「ドント・ケア」(don't care)値は、変数のいずれかの可能な値が、アクティブ状態に達する際に伝搬した遷移に対して全ての条件を満たすために用いることができる場合に、その変数に対して指定することができる。具体的には、ドント・ケア値を用いることができるのは、（ａ）ステートチャート入力変数又はステートチャート定義変数が、アクティブ状態に達する前に、現在のタイムステップにおいて読み取られていない場合、（ｂ）アクティブ状態に達する前に、ステートチャート出力変数が設定されていない場合、（ｃ）アクティブ状態に達する前に、ステートチャート出力変数が、「ドント・ケア」値を有するステートチャート入力変数又はステートチャート定義変数に設定されている場合、又は（ｄ）アクティブ状態に達する前に、「ドント・ケア」値を有するステートチャート入力値又はステートチャート定義値によって呼び出された関数によって戻された値に、ステートチャート出力変数が設定されている場合である。あるいは、１組の現在値５２０及び／又は１組の既定値５３６は、読み出された変数及び／又は設定された変数のみを指定し、アクティブ状態に達したときに、それらの値を指定してもよい。
【００６４】
ステートチャート入力変数の値は、次のイベントのファイアー直前に、「ドント・ケア」に戻るが、ステートチャート出力変数及びステートチャート定義変数は、該当する入口(entry)、出口(exit)、最中(during)、又は遷移アクション（例えば、output1=3）によって具体的に新しい値を割り当てられるのでなければ、イベントを跨ってそれらの値を保持する。
【００６５】
表１は、ステートチャートにおける値の記録の一例を提示する。この例では、「TempIn」と称するステートチャート入力変数が、ステートチャートのState1に入る直前に「３７」の値に最初に設定され、ステートチャートは「Local1」と称するステートチャート定義変数も備えていると仮定する。最初のタイムステップ（即ち、１つのイベントのファイアー直後）の期間中、TempInの値は３７であり、Local1の値は、以下の表１の行１に示すように「ドント・ケア」となる。次に、ステートチャートを通過するファイアー経路がState1からState2に移り、そこでLocal1が「ＡＢＣ」の値に設定されると仮定する。次の４つのイベントのファイアーに応答して、この例ではいずれの遷移もファイアーされず、TempIn及びLocal1の値は変化しない。したがって、表１の行２は、TempInの値が「ドント・ケア」であり、Local1が「ＡＢＣ」である、５の期間を示す。次に、TempInが、次のイベントの直前に「４０」の値に設定され、これによってState2からState3への遷移が生ずる。State3では、Local1が「ＤＥＦ」の値に設定される。行３は、一旦State3に入った変数の値を示す。次のイベントの間遷移はファイアーしないので、TempInは「ドント・ケア」値を有し、Local1は「ＤＥＦ」を保持する。これは、行４に示す通りである。
【００６６】
【表１】
0005495615.tif 000002
【００６７】
変数の値は、スカラー値（例えば、Ａ＝４）として、値の範囲として、又はスカラー値と値の範囲との組み合わせとして指定することができる。値の範囲は、「［ａ、ｂ］」というように書くことができ、大括弧を用いて範囲を書く場合、終点値「ａ」及び「ｂ」も含む。例えば、「Ａ＝［６、９］」は、Ａが６〜９の範囲内であればいずれの値でもよいことの表現であり、値６及び９も含む。「Ａ＝４，［６、９］」という式は、スカラー値と値の範囲との組み合わせの一例であり、Ａは、４又は６〜９の、それらを含む範囲における値のいずれかであればよいことを述べている。
【００６８】
範囲が終点値を含まない場合、その範囲は「（ａ、ｂ）」のように、括弧を用いて書くことができる。例えば、「Ａ＝（６、９）」は、Ａが６〜９の間であればいずれの値でもよいが、６や９は含まないことの式である。いずれの数も無限大を超えることはできないので、無限大という値を伴う範囲は、通例、無限大を伴う範囲の部分に対して括弧を用いて書かれる。例えば、「Ａ＝［０、∞］」は、Ａが０以上であればいずれの値でもよいことの式であり、「Ｂ＝（−∞、∞）」は、Ｂが無限大でなければいずれの値でもよいことの式である。
【００６９】
検査生成装置は、順方向及び逆方向伝搬パスの間、区間計算(interval mathematics)や範囲分析を用いることができる。範囲分析の使用によって、ステートチャートを区間に基づいて等価クラスに分割することを可能にすることにより、更に高いセマンティック・レベルにおけるステートチャートの調査が可能となる。例えば、ステートチャートにおいて変数Ａを１に設定する場合、全ての「下流」状態には、Ａ＝１という制約が生ずる。別の例では、ステートチャートにおいて、別の変数Ｂが０よりも大きいか否か判定を行うために検査を行った場合、この制約は、２つの範囲に関して考えることができる。つまり、Ｂが０未満である範囲、即ち、Ｂ＝（−∞、０）、及びＢが０よりも大きい範囲、即ち、Ｂ＝（０、∞）である。
【００７０】
範囲に対して演算を実行することにより、可能性のある又は実際の０による除算、アンダーフロー、及びオーバーフローの誤りのような誤りを自動的に捕らえることによって、ステートチャートから得られたソース・コードのデバッグ処理を支援する。範囲の使用により、横断することが不可能な遷移の判定を支援することができる。例えば、変数Ｃの範囲が［２、４］であり、一方状態Ｓがアクティブであり、状態Ｓからの出立遷移に「Ｃ＞５」という条件がある場合、Ｃの範囲内にあるいずれの値でも条件を満たすことができないので、遷移を横断することは不可能である。更に、Ｃが範囲［２、４］にあると判定することによって、Ｃの値に対して３つの等価クラスを作成することができる。つまり、Ｃが（−∞、２）となる等価クラス、Ｃが［２、４］となる等価クラス、及びＣが（４、∞）となる等価クラスである。
【００７１】
等価クラス推論、及び区間計算の使用により、検査生成の性能を著しく向上させることができる。区間計算の使用により、数学的、論理的、関係的演算子を通じて組み合わされた多数の変数から成る複雑な条件も効率的に分析することが可能となる。"Interval Arithmetic and Automatic Error Analysis in Digital Computing"（ディジタル計算における区間計算及び自動誤り分析）と題するR. E. Mooreの学位論文では、どのようにして算術演算子を区間（即ち、範囲）に応用して、結果的に得られる範囲を計算するかが説明されている。この論文の内容は、ここで引用したことにより、本願にも含まれるものとする。R. E. Mooreの "Interval Arithmetic and Automatic Error Analysis in Digital Computing"（ディジタル計算における区間計算及び自動誤り分析）(Department of Mathematics, Stanford University) (Nov. 1962)は、http://interval.louisiana.edu/Moores early papers/disert.pdfにおいて入手することができる。
【００７２】
検査ベクトル生成方法
図６は、本発明の実施形態にしたがって、ステートチャートに対して検査ベクトルを生成する方法６００の一例のフローチャートである。方法６００は、本発明の範囲及び主旨から逸脱することなく、検査生成装置、検査ドライバ、検査生成装置と検査ドライバとの組み合わせ、及び／又は本明細書において記載されない１つ以上のその他のエンティティによって実行することができる。
【００７３】
尚、このフローチャートにおける各ブロック、及び本明細書において呈示するその他のフローチャートの中にある各ブロックは、モジュール、セグメント、又はコンピュータ・プログラム・コードの一部を表す場合もあり、特定の論理機能又はプロセスにおけるステップを実現するための１つ以上の実行可能命令を含むことは言うまでもない。実施形態例の範囲には、代替実施態様も含まれ、その場合、機能は、伴う機能性に応じて、実質的に同時又は逆の順序を含む、図示又は論述するのとは異なる順序で実行してもよい。これは、記載する実施形態の技術分野に相応に習熟している者には言外であろう。即ち、本明細書において記載する順方向伝搬パスは、本明細書において記載する逆方向伝搬パスとは独立して実行することができる。
【００７４】
図６に移り、ブロック６１０において、検査生成装置は入力ステートチャートを受信する。入力ステートチャートは、システム設計モデルを備えることができる。入力ステートチャートは、ネットワーク通信インターフェース４４０のような、通信インターフェースを通じて受信することもできる。入力ステートチャートは、ユーザ・インターフェース４３０を通じて受信することもできる。入力ステートチャートは、Simulink（登録商標）コンピュータ・パッケージ又はMicrosoft Office Visio（登録商標）ソフトウェア・パッケージが提供するグラフィカル・ユーザ・インターフェース（ＧＵＩ）を用いて作成することもできる。入力ステートチャートは、複数の状態及び複数の遷移を備えることができる。複数の状態における１つ以上の状態は、初期状態として特定することができ、複数の状態における１つ以上の状態は最終状態として特定することができる。複数の遷移における各遷移は、該遷移と関連付けられた１つ以上の条件を有することができる。
【００７５】
ブロック６２０において、検査生成装置を初期化することができる。検査生成装置の初期化は、入力ステートチャートにおける全ての状態及び全ての遷移を未達とすることを含む。また、環境、環境リスト、タイムステップ−シーケンス−データ・オブジェクト、シーケンス・リスト、及び／又は未達遷移リストというような、追加のデータ構造も同様に初期化することができる。環境リストは、初期化して空にすることができ、未達遷移リストは、初期化して、ステートチャートにおける遷移毎に生成した環境を含ませることができる。検査生成装置を初期化するユーザ入力を要求することもできる。例えば、最大深さ値を初期化するユーザ入力を要求することができる。
【００７６】
即ち、環境５００のような環境は、ステートチャートにおける遷移毎に生成することができ、１組のアクティブ状態５１０は初期状態ではヌルにすることができ、１組の現在値５２０はステートチャート入力、ステートチャート出力、及び／又はステートチャート定義変数毎に「ドント・ケア」値を示すことができ、過去状態リスト５３２及び過去遷移リスト５３４は、空に設定することができる。１組の既定値５３６は、ステートチャート入力変数、ステートチャート出力変数、及び／又はステートチャート定義変数毎に、「ドント・ケア」値を示すことができる。
【００７７】
ブロック６３０において、検査生成装置は、順方向伝搬パスを実行すべきか否か判断することができる。順方向伝搬パスを実行すべき場合、検査生成装置はブロック６４０に移る。順方向伝搬パスを実行すべきでない場合、検査生成装置はブロック６６０に移る。
ブロック６４０に達すると、検査生成装置は順方向伝搬パスを実行することができる。順方向伝搬パスは、本明細書に記載する方法７００の手順の一部又は全部を含むことができる。
【００７８】
図７は、本発明の実施形態にしたがって順方向伝搬パスを実行する方法７００の一例を示す。方法７００は、ブロック７１０において開始する。
ブロック７１０において、検査生成装置は、ステートチャートの各初期状態を環境リストに追加することができる。検査生成装置は、環境リストにおけるステートチャートの初期状態毎に、環境５００を生成し格納することができる。１組のアクティブ状態５１０は、検査生成装置によって現在調べられている状態を含むことができ、初期状態の場合、１組のアクティブ状態５１０は初期状態であればよい。１組の現在値５２０は、アクティブ状態において及び／又はアクティブ状態に入る遷移又はそこから出る遷移によって読み取られた又は設定された１つ以上のステートチャート入力変数、ステートチャート出力変数、及び／又はステートチャート定義変数の各々に対して値を含むことができる。初期状態の場合、マルチステップ・ベクトル５３０の過去状態リスト５３２及びマルチステップ・ベクトル５３０の過去遷移リスト５３４を空に設定すればよい。
【００７９】
１組の現在値５１０及び／又は１組の過去値５３６は、ステートチャート入力変数及びステートチャート出力変数のいずれか又は全てに関連がある値及び／又は範囲を含むことができる。
ブロック７２０において、検査生成装置は横断技法（例えば、深さ−第１又は幅−第１検索）を用いて、環境リストから環境を選択することができる。現環境（ＣＥ）ポインタを、選択した環境を参照するように設定する。環境リストの編成は、用いる横断技法（即ち、深さ−第１検索横断技法は、環境リストをスタックとして編成することができる）によって変化する場合もある。一旦環境を選択したなら、選択した環境に「調査済み」という印を付けるとよい。
【００８０】
ブロック７３０において、検査生成装置は、アクティブ状態集合を決定することができる。アクティブ状態集合は、選択した環境の１組のアクティブ状態５１０をコピーすることによって決定することができる。
ブロック７４０において、検査生成装置は、現在のアクティブ状態をアクティブ状態集合から除去することができる。この状態を現アクティブ状態と見なす。現アクティブ状態のアクティブ状態集合からの選択は、ランダムであってもよく、あるいは順序付けてもよい。順序付けの例では、親の前に全ての子の状態を選択する、又はその逆を含む。別の順序付けも可能である。
【００８１】
ブロック７５０において、検査生成装置は、ソース状態が現アクティブ状態である「未調査」遷移の位置を突き止めることができる。即ち、検査生成装置は、順方向到達遷移の候補（ＣＦＲＴ）を突き止める。遷移を「未調査」であると判断できるのは、その遷移が「到達済み」とも「未達」とも判断されていない場合である。検査生成装置は、到達遷移リスト及び未達遷移リストの双方を維持することにより、遷移が未調査であると判断することができる。遷移を未検査遷移であると判断できるのは、その遷移が到達遷移リストにも未達遷移リストにもない場合である。あるいは、検査生成装置は、遷移を到達済み、未達、又は未検査として追跡するために、遷移毎にインディケータを用いることもできる。
【００８２】
本発明の別の実施形態では、未達状態リスト及び到達状態リストを用いて、未達遷移リスト及び到達遷移リストの機能をそれぞれ実行することもできる。検査生成装置は、到達状態リスト及び未達状態リスト双方を維持することによって、状態が未調査であると判断することができる。状態を未調査状態であると判断できるのは、その状態が到達状態リストにも未達状態リストにもない場合である。
検査生成装置は、選択した環境に基づいて、候補環境を生成することができる。例えば、検査生成装置は、ＣＥポインタを通じて、選択した環境をコピーすることによって、候補環境を生成することができる。候補環境を生成する他の方法も可能である。
【００８３】
ブロック７６０において、検査生成装置は、ＣＦＲＴを順方向に伝搬できると判断することができる。以下の３つの条件が全て真である場合に、ＣＦＲＴを順方向に伝搬することができる。
（１）ＣＦＲＴのソース状態がアクティブ状態集合の中にある。
（２）候補環境の１組の現在値に格納されているステートチャート入力変数、ステートチャート出力変数、及び／又はステートチャート定義変数の値を、候補環境において読み取られていないあらゆるステートチャート入力変数のあらゆる正当な値と組み合わせて用いて、並列状態、親状態、又は子状態からの遷移を含む、ＣＦＲＴの優先順位が高いほうの遷移全ての条件を、無効にすることができる。
（３）候補環境の１組の現在値に格納されているステートチャート入力変数、ステートチャート出力変数、及び／又はステートチャート定義変数の値を、候補環境において読み取られていないあらゆるステートチャート入力変数のあらゆる正当な値と組み合わせて用いて、ＣＦＲＴと関連のある全ての条件を満たすことができる。
「組み合わせ制約」という用語は、本明細書において用いる場合、前述の条件（２）及び（３）の合体を記述するために用いられる。
【００８４】
検査生成装置は、以下の手順の１つ以上を実行することによって、ＣＦＲＴを順方向に伝搬することができると判断することができる。
（ａ）検査生成装置は、候補環境に格納されている値に基づいて、ＣＦＲＴの組み合わせ制約を満たすことができると判断することができる。
（ｂ）検査生成装置は、候補環境のアクティブ状態に格納されている１つ以上のステートチャート入力変数の制約及び／又は「更なる制約」に基づいて、ＣＦＲＴの組み合わせ制約を満たすことができると判断することができる。また、候補環境のアクティブ状態における１つ以上のステートチャート入力変数を更新して、関連のある制約値又は更なる制約値を反映することもできる。
【００８５】
区間計算又は区間ロジックを用いて区間を縮小することによって、値を抑制することができる。更に抑制した後の、抑制値全体がなおも元の値以内に含まれる限り、値を更に小さい区間又は１つの値に更に抑制することもできる。したがって、単一値はそれ以上抑制することはできない。「ドント・ケア」値は、未抑制値として扱うことができる。尚、区間及び／又は単一値のみを含むように、値を更に抑制することもできる。
例えば、変数ｘに対する「ドント・ケア」値は、条件ｘ＞１００を可能にするように、区間（１００、無限大）に抑制することができる。次いで、ｘに対する区間（１００、無限大）は、条件２００≦ｘ≦３００を可能にするために、［２００、３００］に更に抑制し、ｘ＝３６５という条件を可能にするために１つの値３６５に抑制することができ、あるいは（（２００≦ｘ≦３００）又は（ｘ＝＝３６５））という条件を可能にするために、［２００、３００］及び３６５の組み合わせに抑制することもできる。
【００８６】
（ｃ）検査生成装置は、候補環境における１つ以上の状態における可能なアクションに基づいて、ＣＦＲＴの組み合わせ制約を満たすことができることを判断することができる。例えば、検査生成装置は、組み合わせ制約を満たすことができるかことを判断するために、状態の最中アクション(during action)を実行するように、あるイベントをファイアーした後もアクティブ状態にあり続けることができる。また、ＣＦＲＴを候補環境における１つ以上のアクティブな状態において横断させるために取られた可能なアクションを反映するために、候補環境を更新することもできる。可能なアクションには、所与の環境及び／又は検査生成装置が維持するその他の環境にイベントをブロードキャストすることを含むことができる。
（ｄ）手順（ｂ）に記載したようなステートチャート入力変数値の変更、及び手順（ｃ）に記載したような１つ以上の状態において可能なアクションを行うことを組み合わせて用いると、ＣＦＲＴの組み合わせ制約を満たすこと、つまりＣＦＲＴを順方向に伝搬できることを判断する。
それ以外の場合、検査生成装置は、ＣＦＲＴを順方向に伝搬することができないと判断する。
【００８７】
ＣＦＲＴを順方向に伝搬することができない場合、検査生成装置はブロック７６２に移る。ＣＦＲＴを順方向に伝搬することができる場合、検査生成装置はブロック７６４に移る。
ブロック７６２において、検査生成装置は、ＣＦＲＴを順方向に伝搬することができない、つまりＣＦＲＴは順方向到達遷移ではないと判断する。ＣＦＲＴを伝搬することができるか否か判断するために、検査生成装置は、組み合わせ制約を分析して、この組み合わせ制約が「実現可能」か又は「実現不能」か判断することができる。実現可能な制約とは、選択した値又は１組の値によって満たすことができる制約であり、例えば、制約（ｘ＞１００）は、ｘを１００よりも大きく選択すれば満たすことができる。実現不能な制約とは、実現不可能な制約、例えば（（ｘ＝＝１）ＡＮＤ（ｘ＝＝２））である。組み合わせ制約が実現不可能な場合、検査生成装置は、仕様誤りを報告することができる。次いで、検査生成装置はブロック６８０に移る。仕様誤りを報告しない場合、候補環境を破棄することができる。
【００８８】
ブロック７６４において、検査生成装置は、ＣＦＲＴを順方向に伝搬する、つまりＣＦＲＴは順方向到達遷移であると判断する。候補環境が以前に未達遷移リストから除去されていなかった場合、候補環境を未達遷移リストから除去する。
検査生成装置は、候補環境における１組のアクティブ状態５１０から、現在のアクティブ状態を除去し、ＣＦＲＴの宛先状態を、候補環境における１組のアクティブ状態５１０に追加する。検査生成装置は、現在のアクティブ状態を候補環境の過去状態リスト５３２に追加する。候補環境の過去遷移リスト５３４を更新して、ＣＦＲＴを含ませることができる。検査生成装置は、候補環境における１組の現在値５２０を、候補環境の１組の既定値５３６にコピーすることができる。次いで、検査生成装置は、宛先状態におけるアクションに基づいて、候補環境における願材の１組の値５２０を更新する。検査生成装置は、候補環境を環境リストに追加することができる。
【００８９】
ブロック７７０において、検査生成装置は、ソース状態が現アクティブ状態である未調査遷移が未だあるか否かを判断する。現在のアクティブ状態からのいずれかの遷移が未調査である場合、検査生成装置はブロック７５０に戻る。現在のアクティブ状態からの遷移全てを調査し終えていた場合、検査生成装置はブロック７８０に移る。
ブロック７８０において、検査生成装置は、アクティブ状態集合、及び／又は遷移が未調査である候補環境に未だアクティブ状態があるか否か判断する。また、検査生成装置は、アクティブ状態がないか候補環境も調べることができる。候補環境において、及び／又は遷移が未調査であるアクティブ状態において未だアクティブ状態がある場合、検査生成装置はブロック７４０に移ることができる。遷移が未調査である候補環境の中にアクティブ状態がない場合、検査生成装置はブロック７９０に移る。
【００９０】
ブロック７９０において、検査生成装置は、環境リストの中に、調べるべき環境が未だあるか否か判断する。環境リストにおける環境全てを調べたと判断する１つの技法は、環境リストにおける全ての環境に調査済みの印が付けられていると判断することである。しかし、他の技法も可能である。環境リストにおける全ての環境を調べ終えていた場合、検査生成装置は順方向伝搬パスが完了したと判断することができる。環境リストにおける全ての環境を調べ終えていない場合、検査生成装置はブロック７２０に移る。
【００９１】
図２のステートチャートを用いた順方向伝搬パスの一例として、ブロック７２０において、検査生成装置は、初期状態２１０に対する環境を生成し、その環境を環境リストに追加することによって、ステートチャート２００の初期状態２１０を環境リストに追加する。
例えば、ブロック７２０において、検査生成装置は、１組のアクティブ状態５１０を初期状態２１０に設定し、ステートチャート２００における全てのステートチャート入力変数、ステートチャート出力変数、及びステートチャート定義変数について、１組の現在値５２０及び１組の過去値５３６を「ドント・ケア」値に設定し、マルチステップ・ベクトル５３０の過去状態リスト５３２及びマルチステップ・ベクトル５３０の過去遷移リスト５３４を空に設定することによって、初期状態２１０の環境５００を生成する。
【００９２】
ブロック７２０において、環境リストから初期状態２１０の環境を選択し、選択した環境を参照するようにＣＥポインタを設定し、ブロック７３０において、初期状態２１０を用いて設定したアクティブ状態を決定し、ブロック７４０において、その初期状態２１０をアクティブ状態集合から除去したと仮定する。
ブロック７５０において、遷移２１２をＣＦＲＴとして識別する。何故なら、遷移２１２は、ステートチャート２００において、そのソース状態が初期状態２１０である唯一の遷移であるからである。検査生成装置は、選択した環境を、恐らくはＣＥポインタを通じて、コピーすることによって、候補環境（遷移２１２に対する）を生成する。
【００９３】
ブロック７６０において、遷移２１２を横断するために満たすべき条件がなく、これよりも優先順位が高い遷移がないので、ＣＦＲＴ（遷移２１２）を順方向に伝搬することができる。ブロック７６４において、最初にＣＦＲＴのソース状態をマルチステップ・ベクトル５３０の過去状態リスト５３２にコピーし、１組のアクティブ状態５２０をＣＦＲＴの宛先状態に等しく設定することによって、候補環境を更新することができる。１組のアクティブ状態５１０から初期状態２１０を除去し、StartState状態２１６を１組のアクティブ状態５１０に追加し、初期状態２１０をマルチステップ・ベクトル５３０の過去状態リスト５３２に追加し、遷移２１２を過去遷移リスト５３４に追加し、選択した環境からの１組の現在値５２０を候補環境の１組の過去値５３６にコピーすることによって、候補環境を更新することもできる。選択した環境の１組の現在値５２０は、「oState=0」及び「count=0」の入口アクションのような、StartState状態２１６における入口アクションによって更新することができる。
【００９４】
ブロック７７０において、検査生成装置は、初期状態２１０からの全ての遷移（例えば、遷移２１２）を調べ終えたか否か判断する。つまり、未調査遷移がなく、検査生成装置はブロック７８０に移る。ブロック７８０において、検査生成装置は、アクティブ状態集合及び／又は候補環境において未だアクティブ状態がある（例えば、StartState状態２１６）と判断し、ブロック７４０に戻る。
【００９５】
順方向伝搬パスの間に最初に到達したときに、遷移に到達又は未達という印を付けるので、各遷移は、順方向伝搬パスの間に１回しか横断することができない。順方向伝搬パスの間各遷移を１回だけ横断する場合、ステートチャートにおけるサイクルの伝搬は、多くても１回繰り返すだけであると考えられる。したがって、順方向伝搬パスは、例えば、遷移を横断することができる前に、経路においてある回数のサイクルが発生することを指定する条件のために、ステートチャートにおけるある遷移には到達できない場合がある。
【００９６】
一例として、条件２５４は、変数「count」が１を超える場合でないと遷移２５２を横断できないことを示す。ステートチャート２００を調べると、変数「count」は遷移２２６の遷移アクションによって増分することができる。図２は、遷移２２６の遷移アクション２８８が「/count=count+1;」であることを示す。したがって、「count」を１よりも大きくするためには、つまり条件２５４を満たすためには、遷移２２６の横断を伴う少なくとも２回のサイクルという要件がある（即ち、「count」は、StartState状態２１６への入口アクションとして０に初期化されるので、最初のサイクルが遷移アクション２２８を実行すると「count」を１に増分させ、２回目のサイクルが遷移アクション２２８を実行すると「count」を２に増分させ、こうして条件２５４を満たす）。順方向伝搬パスは、ステートチャートのある回数のサイクルを要求する条件がある遷移は、順方向に伝搬できないと判断する。例えば、条件２５４は順方向に伝搬することができない。何故なら、環境リストには、SecondState状態２２０を離れる前に、遷移２２６を２回ファイアーする環境がないからである。
【００９７】
図６に戻って、ブロック６５０において、検査生成装置は、未達の遷移があるか否か判断する。検査生成装置は、未達遷移リストが空でないことを判断することによって、未達遷移があることを判断することができる。未達の遷移がない場合（即ち、未達遷移リストが空である場合）、逆方向伝搬パスを実行せずに、検査生成装置はブロック６９０に移る。未達の遷移がある場合、検査生成装置はブロック６６０に移る。
ブロック６６０に達すると、検査生成装置は逆方向伝搬パスを実行する。逆方向伝搬パスは、本明細書に記載する方法８００の手順の一部又は全部を備えている。
【００９８】
図８は、本発明の実施形態にしたがって、逆方向伝搬パスを実行する方法８００の一例のフローチャートである。
方法８００は、ブロック８１０において開始する。ブロック８１０において、検査生成装置は、未達の遷移があるか否か判断する。検査生成装置は、未達遷移リストが空でないと判断することにより、未達遷移があると判断することができる。未達の遷移がない場合（即ち、未達遷移リストが空である場合）、逆方向伝搬パスは完了する。未達遷移がある場合、検査生成装置はブロック８１４に移る。
【００９９】
ブロック８１４において、検査生成装置は、未達遷移リストの中に未調査遷移があるか否か判断する。検査生成装置は、順方向伝搬パス及び逆方向伝搬パス双方に、共通の未達遷移リストを用いることができる。したがって、検査生成装置は、順方向伝搬パスと逆方向伝搬パスとの間において、共通の未達遷移リストを通じて結果を伝達することができる。順方向経路パス間で結果を伝達する別の技法は、順方向伝搬パス及び逆方向伝搬パスの双方に共通の環境リストを用いることである。尚、共通未達遷移リスト及び共通環境リストの双方を、順方向伝搬パス及び逆方向伝搬パスの双方に用いてもよい。
【０１００】
次いで、順方向伝搬パスとは別個に逆方向伝搬パスを利用する１つの技法は、ブロック８１４において未達遷移リストを作成し、入力ステートチャートの遷移全てを含むように未達遷移リストを初期化することである。また、ブロック８１４において、環境リストの作成も含めて、逆方向伝搬パスの初期化も余分に実行してもよい。
検査生成装置は、調査済み遷移リスト上にない遷移が、未達遷移リスト上未だあるか否か判断することによって、未達遷移リストの中に、未調査遷移があるか否か判断することができる。未調査遷移がある場合、検査生成装置はブロック８２０に移る。未検査遷移がない場合、逆方向伝搬パスは完了する。
【０１０１】
ブロック８２０において、検査生成装置は、未達遷移リストから候補逆方向到達可能遷移（ＣＢＲＴ）を読み出す。検査生成装置は、未達遷移リストからＣＢＲＴ環境を読み出すことによって、ＣＢＲＴを読み出すことができる。ＣＢＲＴ環境は、ＣＢＲＴポインタを、読み出したＣＢＲＴ環境を参照するように設定することによって、読み出すことができる。別の読み出し技法も可能である。
【０１０２】
ブロック８３０において、検査生成装置は、ＣＢＲＴについて関連するタイムステップ−シーケンス・オブジェクト（ＡＴＳＯ）を作成し、ＡＴＳＯをシーケンス・リスト上に配することができる。タイムステップ−シーケンス・オブジェクトは、１つ以上の後続イベントの結果を表す（例えば、結果は、特定の遷移をファイアーした場合、又はいずれの遷移もファイアーしない場合を表すことができる）。タイムステップ−シーケンス・オブジェクトは、「完全−制約式」(complete-constraint expression)を備えることができる。完全制約式は、タイムステップ−シーケンス・オブジェクトが表す結果が実行されることを確保するために満たすことが必要となる、組み合わせ条件を含む、１つ以上の条件についての情報を備えることができる。
【０１０３】
タイムステップ−シーケンス・オブジェクトは、後続のタイムステップ−シーケンス・ポインタを含むことができる。後続のタイムステップ−シーケンス・ポインタは、１つ以上の後続のイベントの結果を表すことができる。タイムステップ−シーケンス・オブジェクトは、別のタイムステップ−シーケンス・オブジェクトを参照する後続タイムステップ−シーケンス・ポインタを有することができ、更にその別のタイムステップ−シーケンス・オブジェクトが有する後続タイムステップ−シーケンス・ポインタは別のタイムステップ−シーケンス・オブジェクトを参照する等となる。次いで、タイムステップ−シーケンス・オブジェクトの完全−制約式は、タイムステップ−シーケンス・オブジェクトの組み合わせ制約と、タイムステップ−シーケンス・オブジェクトの後続タイムステップ−シーケンス・ポインタを通じて参照したタイムステップ−シーケンス・オブジェクトからの未解決の制約式との連結(conjunction)で構成することができる。
【０１０４】
最初に、後続タイムステップ−シーケンス・ポインタは、後続のイベントがない（即ち、後続タイムステップ−シーケンス・ポインタがヌルである）ことを示し、完全−制約式は、ＣＢＲＴの組み合わせ制約のみを含むことができる。
タイムステップ−シーケンス・オブジェクトの深さは、（ａ）後続−タイムステップ・シーケンス・ポインタが後続のイベントがないことを示す場合には、１、又は（ｂ）後続タイムステップ−シーケンス・ポインタによって指し示されるタイムステップ−シーケンス・オブジェクトの深さに１を加算した値として定義する。例えば、タイムステップ−シーケンス・オブジェクトの後続タイムステップ−シーケンス・ポインタによって指し示されるタイムステップ−シーケンス・オブジェクトの深さが２である場合、タイムステップ−シーケンス・オブジェクトの深さは、２＋１＝３となる。
【０１０５】
ブロック８４０において、検査生成装置は、シーケンス・リストからＡＴＳＯを読み出すことができる。一旦読み出したならば、読み出されたＡＴＳＯをシーケンス・リストから除去してもよい。
ブロック８５０において、検査生成装置は、読み出したＡＴＳＯの完全−制約式を満たすことができるか否か判断する。検査生成装置は、完全−制約式を満たすことができると判断することによって、ＣＢＲＴが「逆方向到達」遷移であると判断する（即ち、逆方向伝搬パスを通じて到達することができる遷移）。検査生成装置は、環境リスト上にあるあらゆる環境における値を検査して、環境内にある値が完全−制約式を満たすことができるか否か確認しようとすることによって、完全−制約式を満たすことができると判断する。環境リストの環境において値を検査するだけでなく、検査生成装置は、更に１つ以上のステートチャート入力変数を、完全−制約式を満たす値に抑制しようとすることもできる。検査生成装置が、読み出したＡＴＳＯの完全制約式を満たすことができると判断した場合、検査生成装置はブロック８６０に移る。検査生成装置が、読み出したＡＴＳＯの完全制約式を満たすことができないと判断した場合、検査生成装置は、解明することができない完全−制約式の部分を格納し、ブロック８７０に移る。
【０１０６】
ブロック８６０において、検査生成装置はＣＢＲＴ環境を生成する。検査生成装置は、完全−制約式を満たすために用いられた環境のコピーを、環境リストから作る。更に、検査生成装置は、必要に応じて、完全−制約式を満たすように、ＣＢＲＴ環境のステートチャート入力変数の値を抑制する。検査生成装置は、ＣＢＲＴ環境のマルチステップ・ベクトルにおける１組の既定値を、完全−制約式を満たすために用いた環境からの値を用いて更新することができる。ＣＢＲＴ環境のマルチステップ・ベクトルの過去状態リストは、完全−制約式を満たすために到達した状態を追加するように更新することができる。ＣＢＲＴ環境のマルチステップ・ベクトルの過去遷移リストは、完全−制約式を満たすために横断したいずれの遷移をも追加するように更新することができる。
【０１０７】
ブロック８６２において、検査生成装置は、ＣＢＲＴ環境を環境リストに追加する。次いで、追加したＣＢＲＴ環境を用いて、未達遷移リストに他の未達遷移が未だあるならば、それを満たすか否か(satisfiability)を判定する。
ブロック８６４において、検査生成装置は、未達遷移リストからＣＢＲＴを以前に除去していなかったのであれば、除去することができる。ブロック８６４のアクションを実行した後、検査生成装置はブロック８１０に移る。
【０１０８】
ブロック８７０において、検査生成装置は、１つ以上の新−タイムステップ−シーケンス・オブジェクト（ＮＴＳＯ）を生成することができる。検査生成装置は、最初に既定−実現可能−タイムステップ−シーケンス・オブジェクト(previous-feasible-timestep sequence object)を生成することによって、各ＮＴＳＯを生成することができる。既定−実現可能−タイムステップ−シーケンス・オブジェクトは、現在のステップ以前に少なくとも１つのタイムステップが受け継がれた少なくとも１つのアクションを表すタイムステップ−シーケンス・オブジェクトである。現在のステップ以前に少なくとも１つのタイムステップが引き継がれたアクションの例には、（ａ）遷移の横断、又はある状態の中で実行されるアクション（例えば、「最中」アクション）がある。
【０１０９】
ＡＴＳＯの未解決制約を判定することができる。ＡＴＳＯの未解決制約を判定するには、ＡＴＳＯが表すアクションの効果をシミュレーションし（例えば、イベントに応答して特定の遷移をファイアーする効果、又はイベントに応答していずれの遷移もファイアーしない効果）、シミュレーションした効果をＡＴＳＯの完全−制約式に適用すればよい。
例えば、ＡＴＳＯの完全−制約式が（（ａ＝＝１）ＡＮＤ（ｂ＝＝２）ＡＮＤ（ｃ＞７））とする。更に、関連するアクションをシミュレーションした効果が、変数ａを１の値に設定する遷移アクションを実行することであると仮定する。すると、完全−制約式における変数ａを１の値で置換し、次いでその式を簡略化することによって、未解決制約を計算する。例えば、（１＝＝１）ＡＮＤ（ｂ＝＝２）ＡＮＤ（ｃ＞７）であれば、（ｂ＝＝２）ＡＮＤ（ｃ＞７）に簡略化する。したがって、未解決制約は（ｂ＝＝２）ＡＮＤ（ｃ＞７）となる。下位条件ａ＝＝１はもはや「未解決」ではない。何故なら、制約のその部分は満たされているからである。ＡＴＳＯと関連のある未解決制約を、各既定−実現可能−タイムステップ−シーケンス・オブジェクトに追加する。
【０１１０】
一旦既定−実現可能−タイムステップ・シーケンスを生成したならば、その後続のシーケンス・ポインタをＡＴＳＯのコピーを参照するように設定する。
ブロック８８０において、検査生成装置は、ＮＴＳＯの深さが最大深さ未満であるならば、１つ以上のＮＴＳＯをシーケンス・リストに追加することができる。検査生成装置は、各ＮＴＳＯをしらべて、ＮＴＳＯの深さを判定することができる。
【０１１１】
ＮＴＳＯの深さが最大深さの値を超過する場合、ＮＴＳＯを破棄し、したがってシーケンス・リストには追加しなければよく、これによってＣＢＲＴの検索を、タイムステップの最大深さのみを用いるように抑制することができる。しかしながら、ＮＴＳＯの深さが最大深さの値を超過しない場合、新−タイムステップ−シーケンス・オブジェクトをシーケンス・リストに追加する。
【０１１２】
ブロック８９０において、検査生成装置は、シーケンス・リストが空であるか否か判断することができる。シーケンス・リストが空である場合、検査生成装置はブロック８９２に移る。シーケンス・リストが空でない場合、検査生成装置はブロック８４０に移る。
【０１１３】
ブロック８９２において、検査生成装置は、ＣＢＲＴを未達遷移として扱うことができる。即ち、ＣＢＲＴは、逆方向伝搬パスを用いた逆方向到達遷移ではない。検査生成装置は、（１）他の遷移に到達した後、再度未達遷移を検査するまで待ち、（２）未達遷移を示す、仕様誤りに対するエラー・メッセージを生成し、（３）仕様誤りを示さないエラー・メッセージを生成し、（４）ＣＢＲＴが未達遷移であることを示す出力を検査生成装置のユーザに供給し、あるいは（５）これらの手順のあらゆる組み合わせによって、到達不可能な遷移を扱うことができる。到達不可能な遷移を扱う他の手順も可能である。ブロック８９２を完了した後、検査生成装置はブロック８１０に移る。
【０１１４】
あるいは、検査生成装置は、遷移が到達不可能であると判断した場合、ブロック８９２において方法８００を中止してもよい。検査生成装置は、入力ステートチャートの遷移の条件として表現した全ての要件を検査することができず、したがって完全なカバレッジを保証することができないために、方法８００を中止することができる。この代替案では、方法８００は、ブロック８９２の手順を実行した後に終了することができる。また、この代替案では、方法６００も、ブロック８９２の手順を実行した後に終了することができる。
【０１１５】
図２のステートチャート２００を用いた逆方向伝搬の一例として、ステートチャート２００を通過する順方向伝搬パスの後、遷移２５２（条件２５４が付随する）に、未達遷移の印を付けることができる。したがって、ブロック８１０において、検査生成装置は、未達遷移があると判断する。遷移２５２が遷移２６２及び２７２よりも高い優先順位を有し、したがって検査生成装置はブロック８２０において遷移２５２をＣＢＲＴとして選択したと仮定すると、検査生成装置は、ブロック８３０においてＡＴＳＯをＣＢＲＴに生成し、生成したＡＴＳＯをシーケンス・リストに入れる。ＡＴＳＯの完全−制約式は、条件２５４を含む。これは、ＣＢＲＴ（遷移２５２）の条件であり、変数「count」が１よりも大きいことを示す。
【０１１６】
ブロック８４０において、検査生成装置は、生成したＡＴＳＯをシーケンス・リストから読み出すことができる。ブロック８５０において、検査生成装置は、生成したＡＴＳＯの完全−制約式を、環境リストにおけるいずれの環境によっても満たすことができないと判断することができる。何故なら、１よりも大きいcountの値を有するものがないからである。次いで、検査生成装置はブロック８７０に移ることができる。ブロック８７０において、検査生成装置は、SecondState状態２２０からのChildState状態２４０への入力を表す、既定−実現可能−タイムステップ−シーケンス・オブジェクトを、完全−制約式in1!＝０ＡＮＤin2!=0を用いて生成することができる。この完全−制約式は、遷移２２２及び２３２に対する条件２２４及び２３４の論理的連結である。ＡＴＳＯの未解決制約を、count>1となるように計算する。既定−実現可能−タイムステップ−シーケンス・オブジェクトの後続シーケンス・ポインタは、ＡＴＳＯのコピーを参照するように設定する。
【０１１７】
ブロック８８０において、最大深さを超過していなかったと仮定すると、検査生成装置はＮＴＳＯをシーケンス・リストに追加することができる。ブロック８９０において、検査生成装置は、シーケンス・リストが空でないと判断し、ブロック８４０に移ることができる。ブロック８４０〜８９０の手順は、満たすことができるＡＴＳＯを発見するまで又はシーケンス・リストが空になるまで継続する。
【０１１８】
図６に戻って、ブロック６７０において、検査生成装置は、未達の遷移があるか否か判断する。検査生成装置は、未達遷移リストが空でないと判断することにより、未達の遷移があると判断する。未達の遷移がない場合（即ち、未達遷移リストが空である場合）、検査生成装置はブロック６９０に移る。未達の遷移がある場合、検査生成装置はブロック６８０に移る。
【０１１９】
ブロック６８０において、検査生成装置は、順方向伝搬パス及び／又は逆方向伝搬パスによって十分な数の遷移に到達の印が付けられているか否か判断する。十分な数の遷移とは、０よりも大きいいずれの整数でもよい（例えば、１）。十分な数の遷移に到達の印が付けられている場合、検査生成装置はブロック６４０に移ることができる。
【０１２０】
順方向伝搬パス及び／又は逆方向伝搬パスによって十分な数の遷移に到達の印が付けられていない場合、検査生成装置はブロック６９０に移る。あるいは、順方向伝搬パス及び／又は逆方向伝搬パスによって十分な数の遷移に到達の印が付けられていない場合、検査生成装置は、入力ステートチャートに仕様誤りがあると判断すること、及び／又はプロセス６００を終了する。
ブロック６９０において、検査生成装置は、ベクトル出力生成を実行することができる。ベクトル出力生成は、本明細書において記載する方法９００の手順の一部又は全部を含むことができる。
【０１２１】
図９は、本発明の実施形態による方法９００の一例のフローチャートである。方法９００は、ブロック９１０において開始する。
ブロック９１０において、遷移に対して生成された環境のマルチステップ・ベクトル５３０を用いて、複数の出力検査ベクトルを生成する。遷移に対して生成される環境は、順方向伝搬パスの間に生成した到達遷移リスト、及び／又は逆方向伝搬パスの間に判断された逆方向到達遷移における環境を含むことができる。各出力検査ベクトルは、システム実行デバイスの実行可能検査に対応することができる。
【０１２２】
複数の出力検査ベクトルの生成は、過去状態リスト５３２、過去遷移リスト５３４、及び／又は遷移に対して生成された各環境５００における各マルチステップ・ベクトル５３０の１組の既定値５３６の使用を含むことができる。出力検査ベクトルの生成は、マルチステップ・ベクトル５３０を出力検査ベクトルにコピーすることを含むことができる。入力ステートチャートの遷移全てに対する複数の出力検査ベクトルの生成は、入力ステートチャートにおける条件として表現したシステム−設計モデルの全ての要件が検査可能であることを示すことができる。
【０１２３】
また、複数の出力検査ベクトルを生成するには、複数の出力検査ベクトルにおける各出力検査ベクトルから、ステートチャート定義変数に対するいずれの参照をも除去することができる。各出力検査ベクトルからステートチャート定義変数を除去することにより、複数の出力検査ベクトルに、ステートチャート入力変数及び／又はステートチャート出力変数のみを供給する。複数の出力検査ベクトルをステートチャート入力変数及び／又はステートチャート出力変数のみと共に用いることによって、システム−設計モデル及び／又はシステム実行デバイスのブラック・ボックス検査を可能とすることができる。
【０１２４】
ブロック９２０において、複数の出力検査ベクトルの人間読み取り可能形態を生成することを決定する。複数の出力検査ベクトルを人間読み取り可能形態で生成する場合、検査生成装置はブロック９３０に移る。複数の出力検査ベクトルを人間読み取り可能形態で生成しない場合、検査生成装置はブロック９４０に移る。
【０１２５】
ブロック９３０において、検査生成装置は出力検査ベクトルの人間読み取り可能形態１０００を生成する。図１０は、本発明の実施形態による、図３に示したステートチャート３００の複数の出力検査ベクトルに対する人間読み取り可能形態１０００の一例である。人間読み取り可能形態１０００は、検査生成装置がステートチャート３００を入力ステートチャートとして用いて生成した複数の出力検査ベクトルの一部を示す。
【０１２６】
出力検査ベクトルの人間読み取り可能形態は、出力検査ベクトルの到達状態及び／又は遷移、ステートチャート入力変数及び／又はステートチャート出力変数の値、及び／又は到達状態の情報に関する内容を提供することができる。図１０に示す人間読み取り可能形態１０００は、列の内容１０２０、イベント情報１０３０、in1の値１０３２、out1の値１０３４、State1の情報１０４０、State1_1の情報１０４２、State1_1_1の情報１０４４、State4の情報１０４６、及びState2の情報１０４８を示す。一例として、人間読み取り可能形態１０００の行１０６０は、１のイベント情報１０３０に対して、in1の値１０３２に示すように、in1ステートチャート入力変数の値が「１」であること、そしてout1ステートチャート入力変数の値が、out1の値１０３４に示すように、「９」であることを示す。また、人間読み取り可能形態１０００の行１０６２は、列の内容１０２０の「REACH State State1」（状態State1到達）で示すように、ステートチャート３００の状態State1３３０に到達することができるという情報を提供する。
【０１２７】
入力ステートチャート、時間及び日付情報、検査生成装置のソフトウェア情報というような、その他の情報も人間読み取り可能形態１０００において提供することができる。図１０は、入力ステートチャート情報１０５２の情報行１０５０を示し、入力ステートチャートの名称である「Chart」、出力検査ベクトルを「２月２日」の日付に生成したことを示す日付情報１０５４、及び検査生成装置が、ＮＪ、MorristownのHoneywell International, Incが供給するＨｉＬｉＴＥコンピュータ・ソフトウェア・パッケージであること、及びこの検査生成装置のソフトウェア・バージョンが「６．２．４．８７４２」であることを示す検査生成装置ソフトウェア情報１０５６を示す。
【０１２８】
検査者が、システム実行デバイスの複数の検査を実行することができる。検査者が実行する複数の検査における各検査は、人間読み取り可能形態１０００に基づくことができる。検査を実行するには、検査について人間読み取り可能形態１０００において示されているステートチャート入力変数に対する出力検査ベクトルにおいて指定されている抑制値に等しい値、又は抑制値の範囲内に収まる値にして、入力をシステム実行デバイスに設定すればよい。システム実行デバイスに入力を設定した後、検査者は、システム実行デバイスを作動させることができる。システム実行デバイスの作動完了時に、検査者はシステム実行デバイスの出力を調べて、これらが、検査について人間読み取り可能形態１０００において示されたステートチャート出力変数の値を満足するか否か判断することができる。システム実行デバイスの出力が、人間読み取り可能形態１０００において示されたステートチャート出力変数の値を満足する場合、検査者は、検査が成功であったと判断することができる。それ以外の場合、検査者は検査が不成功であったと判断することができる。
【０１２９】
図９に戻って、ブロック９４０において、複数の出力検査ベクトルを出力すると決定する。複数の出力検査ベクトルを出力する場合、検査生成装置はブロック９５０に移る。複数の検査ベクトルを出力しない場合、検査生成装置はブロック９６０に移る。
【０１３０】
ブロック９５０において、検査生成装置は複数の出力検査ベクトルを出力する。複数の出力検査ベクトルを検査ドライバに出力することもできる。複数の出力検査ベクトルは、二進フォーマット及び／又は英数字フォーマットで出力することができる。複数の出力検査ベクトルは、データ・ストレージにおけるデータ構造として格納することもできる。検査ドライバは、複数の出力検査ベクトルを受信すること、及び／又は受信した複数の出力検査ベクトルを格納することもできる。
【０１３１】
検査生成装置は、通信インターフェース３４０のような、通信インターフェースを通じて、複数の出力検査ベクトルを出力することができる。同様に、検査ドライバ又はその他の計算機も、通信インターフェース３４０のような通信インターフェースを通じて、複数の出力検査ベクトルを受信することができる。検査生成装置は、恐らくはユーザ・インターフェース３３０の出力ユニット３３４を用いて、ユーザ・インターフェースを通じて複数の出力検査ベクトルを出力することができる。
【０１３２】
ブロック９６０において、検査ドライバは、システム実行デバイスを検査すべきか否か判断する。システム実行デバイスを検査するには、検査生成装置から受信した出力検査ベクトルを用いるとよい。あるいは、検査生成装置及び検査ドライバがコンピュータ・ハードウェア及び／又はソフトウェア資源を共有することもでき、したがって、検査ドライバが出力検査ベクトルを直接用いることもできる（即ち、検査生成装置が出力検査ベクトルを出力することなく、検査生成装置が生成した出力検査ベクトルを用いる）。システム実行デバイスを検査する場合、検査ドライバはブロック９６０に移る。システム実行デバイスを検査しない場合、方法９００は終了し、方法６００も終了することができる。
【０１３３】
ブロック９７０において、検査ドライバは、出力検査ベクトルに基づいて、システム実行デバイスを検査する。ユーザ入力を供給して、種々の検査係数を選択することができる。検査素因には、システム実行デバイス上で実施する検査は何か、出力検査ベクトルの生成源の場所、検査結果及び検査出力を格納する１つ以上のファイル又はその他の構造の場所及び／又は名称、検査しようとする特定のシステム実行デバイスの場所及び／又は名称、システム実行デバイスを検査するために必要な追加の各検査デバイス（が１つでも用いられる場合）の場所等が含まれるが、これらに限定されるのではない。
【０１３４】
検査ドライバは、システム実行デバイスの複数の検査を実行することができる。検査ドライバが実行する複数の検査における各検査は、複数の出力検査ベクトルにおける所与の出力検査ベクトルに基づくことができる。検査を実行するには、ステートチャート入力変数に対して出力検査ベクトルにおいて指定されている抑制値に等しい値、又は抑制値の範囲内に収まる値の入力を、システム実行デバイスに設定すればよい。システム実行デバイスへの入力を設定した後、検査ドライバは、システム実行デバイスを作動させることができる。システム実行デバイスの作動完了時に、検査ドライバは、システム実行デバイスの出力を調べて、所与の出力検査ベクトルにおいて示されているように、ステートチャート出力変数の所与の値を出力が満たすか否か判断することができる。出力がステートチャート出力変数の所与の値を満たす場合、検査ドライバは、検査が成功であったと判断することができる。それ以外の場合、検査ドライバは検査が不成功であったと判断することができる。
ブロック８７０を実行した後、方法９００は終了し、方法６００も終了することができる。
【０１３５】
結論
以上、本発明の実施形態例について説明した。しかしながら、特許請求の範囲によって規定する、本発明の真の範囲及び主旨から逸脱することなく、記載した実施形態には変更や修正が可能であることは、当業者であれば理解できよう。しかしながら、本明細書において詳細に説明した本構成及びその他の構成は、例示の目的のためにのみ提案したのであって、本発明は以下の特許請求の範囲の範囲及び主旨の中に全ての修正や改良を包含することは言うまでもない。したがって、他の構成及びその他の要素（例えば、機械、インターフェース、機能、順序、機能の集合体等）も代わりに用いることができ、いくつかの要素は纏めて省略してもよいことは、当業者には認められるであろう。
【０１３６】
更に、本明細書において記載した要素の多くは、機能的実体であり、離散コンポーネント又は分散構成要素として、あるいは他の構成要素と一緒に、適した組み合わせ及び場所であればいずれでも、そしてハードウェア、ファームウェア、及び／又はソフトウェアの適した組み合わせであれば如何様にも実現することができる。
【図１】
0005495615.tif 000003
【図２】
0005495615.tif 000004
【図３】
0005495615.tif 000005
【図４】
0005495615.tif 000006
【図５】
0005495615.tif 000007
【図６】
0005495615.tif 000008
【図７】
0005495615.tif 000009
【図８】
0005495615.tif 000010
【図９】
0005495615.tif 000011
【図１０】
0005495615.tif 000012