X-Machine_Testing
（ストリーム）X-マシンテスト方法である完全 機能テストするアプローチソフトウェア-ハードウェアの試験のスケーラビリティ利用ストリームX-マシン計算モデルを。この方法論を使用すると、テストされたシステムの実装がその仕様と一致するかどうかを徹底的に決定する有限のテストセットを特定する可能性がこの目標は、分割統治アプローチによって達成されます。このアプローチでは、設計が改良によってStreamX -Machinesのコレクションに分解されます。、個別のモジュールとして実装され、ボトムアップでテストされます。各統合段階で、テスト方法により、テストされたコンポーネントが正しく統合されていることが保証されます。
この方法論は、仕様および実装中にテスト原則の特定の設計に従うことを要求することにより、正式な決定不能性の制限を克服します。結果として得られるスケーラビリティは、数十万の状態と数百万の遷移で構成される実用的なソフトウェアおよびハードウェアシステムが正常にテストされたことを意味します。
コンテンツ
1 動機
1.1 スケーラブルで抽象的な仕様 1.2 増分的にテスト可能な仕様
2 仕様方法
2.1 高レベルの仕様 2.2 低レベルの仕様 2.3 テスト用の設計条件
3 試験方法
3.1 すべての州をテストする 3.2 すべての遷移をテストする
4 アプリケーション
5 参考文献
動機
多くのソフトウェアテストは単に希望に満ちたものであり、さまざまな方法でソフトウェアシステムを実行して、障害を検出できるかどうかを確認しようとしています。テストによって実際にいくつかの障害が明らかになる場合がありますが、テストが終了すると、システムが正しいことを保証することはできません。機能テスト方法は、システムの意図された動作を説明する正式な仕様を開発することにより、この状況を改善しようとします。これに対して、実装は後でテストされます（一種の適合性テスト）。仕様は、ユーザーの要件に照らして検証でき、後で数学的推論によって一貫性があり完全であることが証明されます（論理的な設計上の欠陥を排除します）。完全な機能テスト方法は、仕様を体系的に活用し、実装されたソフトウェアシステムを徹底的に実行するテストセットを生成して、仕様に準拠しているかどうかを判断します。特に：
完全陽性テスト：必要なすべての動作がシステムに存在することを確認します。
完全なネガティブテスト：システムに意図しない動作がないことを確認します。
ソフトウェアシステムは非常に複雑で、数十万の状態と数百万の遷移があるため、このレベルのテストを達成するのは難しい場合が必要なのは、仕様とテストの問題を個別に対処できる部分に分解する方法です。
スケーラブルで抽象的な仕様
Mike Holcombeは、1980年代後半に、ソフトウェア仕様の基礎としてSamuelEilenbergの理論上のXマシンモデルを使用することを最初に提案しました。これは、モデルがシステムの制御フローをシステムによって実行される処理から明確に分離しているためです。与えられた抽象化レベルでは、システムは、いくつかの状態と遷移で構成される単純な有限状態マシンと見なすことができます。より複雑な処理は、遷移の処理関数に委任されます。これにより、基になる基本データ型Xが変更されます。後で、各処理機能が個別に公開され、別のXマシンによって特徴付けられ、そのシステム操作の動作がモデル化される場合が
これは、分割統治アプローチをサポートします。このアプローチでは、システムアーキテクチャ全体が最初に指定され、次に各主要なシステム操作が指定され、次にサブルーチンが指定されます。各レイヤーが独立しているため、各ステップで複雑さのレベルを管理できます。特に、ソフトウェアエンジニアは、ユーザーの要件に照らして単純な有限状態マシンを検証するのが簡単です。
増分的にテスト可能な仕様
Gilbert Laycockは、テスト方法の基礎として、特定の種類のXマシンであるStreamX-Machineを最初に提案しました。このバリアントの利点は、テストを制御できる方法でした。ストリームX-マシン、基本データ型は、特定の形態を有する：X =アウト*× Memの×で*、で*は、入力ストリームが、あるアウトが*出力ストリームであり、MEMは、内部メモリです。Stream X-Machineの遷移は、φ：Mem × In Out × Memの形式の処理関数でラベル付けされます。つまり、入力ストリームから1つの入力を消費し、メモリを変更し、出力ストリームに1つの出力を生成します。 （詳細については、関連する記事を参照してください）。
テストの利点は、このように設計されたソフトウェアシステムが各ステップで観察できることです。入力ごとに、マシンは1つのステップを実行し、入力と出力のペアが正確に一致するように出力を生成します。これは、観察が行われる前にシステムが完了するまで実行される（複数のステップを実行する）他のアプローチとは対照的です。さらに、階層化されたStream X-Machinesは、便利な抽象化を提供します。各レベルで、テスターは処理機能の詳細を忘れて、（サブ）システムを単純な有限状態マシンと見なす場合がChowのW法など、有限状態仕様に準拠するシステムをテストするための強力な方法が存在します。
仕様方法（ストリーム）X-Machine方法論に従う場合、最初の段階は、処理されるさまざまなタイプのデータを識別することです。たとえば、ワードプロセッサは、基本タイプの文字（キーボード入力）、位置（マウスカーソル位置）、およびコマンド（マウスまたはメニューコマンド）を使用します。以下のような他の構築のタイプが存在し得るテキスト :: =文字*（文字のシーケンス）、セレクション :: =ポジション×ポジション（選択範囲の開始と終了）とドキュメント :: =テキスト×セレクション×ブール（テキスト、可能な選択、およびドキュメントが変更されたかどうかを通知するフラグ）。
高レベルの仕様
最上位の仕様は、システムとの主なユーザーインタラクションを説明するStreamX-Machineです。たとえば、ワードプロセッサはさまざまな状態で存在し、キーストロークとコマンドの効果は異なります。このワードプロセッサが{書き込み、選択、ファイリング、編集}の状態で存在するとします。ワードプロセッサは最初の書き込み状態で起動しますが、マウスをドラッグするか、Shiftキーを押したままにすると、選択状態に移行します。選択が確立されると、書き込み状態に戻るはずです。同様に、メニューオプションを選択すると、編集状態またはファイリング状態になります。これらの状態では、特定のキーストロークの意味が異なる場合がメニューコマンドが終了すると、ワードプロセッサは最終的に書き込み状態に戻ります。このステートマシンは、状態を変化させるさまざまなアクションで非公式に設計およびラベル付けされています。
トップレベルマシンの入力、メモリ、および出力タイプが形式化されました。単純なワードプロセッサのメモリタイプが上記で定義されたタイプDocumentであると仮定します。これは、ドキュメントをテキスト文字列として扱い、2つの位置が選択の可能性を示し、フラグが最後のsaveコマンド以降の変更を示します。より複雑なワードプロセッサは、ドキュメントの状態のシーケンスを使用して、元に戻すことができる編集をサポートする場合がドキュメント :: =（テキスト×選択）*。これは、saveコマンドが実行されるたびに1つのドキュメントに折りたたまれます。
：マシンの入力タイプがあるとして :: =コマンド×文字×ポジション。これは、すべての対話が単純な文字の挿入、メニューコマンド、またはカーソルの配置である可能性があることを認識しています。特定のインタラクションは3タプルですが、一部の場所は空である可能性がたとえば、（Insert、 ‘a’、ε）は文字 ‘a’の入力を表します。while（Position、ε、32）は、文字32と33の間にカーソルを置くことを意味します。および（Select、ε、32）は、現在のカーソル位置と文字32と33の間の場所の間のテキストを選択することを意味します。
機械の出力タイプは、与えられた入力に応じて、どの処理機能が実行されたかを出力から判別できるように設計されています。これは、以下で説明する出力の識別可能性の特性に関連しています。
低レベルの仕様
システムが複雑な場合、システムは複数のStreamX-Machineに分解される可能性が最も一般的な種類の改良は、主要な処理機能（高レベルのマシンのラベルでした）のそれぞれを取得し、これらを個別のStreamX-Machinesとして扱うことです。この場合、低レベルのマシンの入力、メモリ、および出力のタイプは、高レベルのマシンに定義されているものとは異なります。これは、高レベルで使用されるデータセットの拡張として扱われるか、高レベルのより抽象的なデータセットから低レベルのより詳細なデータセットへの変換がたとえば、高レベルのコマンドSelectは、低レベルのMouseDown、MouseMove、MouseUpの3つのイベントに分解できます。
Ipateとホルコムには改良のいくつかの種類、言及機能リファイン処理機能の挙動を詳細に詳述されている、および状態の改良、簡単な状態空間をより複雑な状態空間に仕切られているが、。 Ipateは、これら2種類の改良が最終的に同等であることを証明しています
それ以外の場合、システムは、設計者が実装環境でサポートされている基本的な操作を信頼する準備ができているレベルまで指定されます。他の試験方法で小型ユニットを徹底的に試験することも可能です。
テスト用の設計条件（ストリーム）X-Machine方法論では、設計者はテスト条件について特定の設計を観察する必要がこれらは通常、満たすのはそれほど難しくありません。仕様のStreamX-Machineごとに、以下を取得する必要が
最小仕様：仕様は最小 有限状態マシンである必要がこれは、ステートマシンに冗長な状態、つまり、観察可能な遷移動作が他の状態と同じである状態を含めるべきではないことを意味します。
決定論的仕様：マシンの状態ごとに、現在のメモリと次の入力値に対して、最大で1つの処理関数φを有効にする必要がこれにより、テストする必要のある動作が予測可能になります。
テストの完全性：各処理関数φは、すべてのメモリ状態に関して、少なくとも1つの入力に対して実行可能である必要がこれにより、現在のメモリ状態によってマシンがブロックされるデッドロックが発生しなくなります。テストの完全性を確保するために、関数φの定義域は、テスト中にのみ使用される特別なテスト入力で拡張できます。
出力の識別可能性：すべてのメモリと入力のペアについて、呼び出された処理関数をその出力値のみから区別できる必要がこれにより、ステートマシンを処理機能から切り離すことができます。出力の識別可能性を確保するために、関数φの終域は、テスト中にのみ関連する特別なテスト出力で拡張される場合が
最小限のマシンとは、特定の動作に対して状態と遷移が最も少ないマシンです。仕様を最小限に抑えることで、テストセットを可能な限り小さくすることができます。予測可能なシステムには、決定論的なマシンが必要です。そうしないと、実装はどの遷移が行われたかに関して任意の選択を行う可能性が最近のいくつかの作業により、この仮定が緩和され、非決定性マシンのテストが可能になりました。
実装が扱いやすい時間内にテスト可能であることを確認するには、テストの完全性が必要です。たとえば、システムに遠い状態、またはメモリが特定の制限値に達した後にのみ入力される到達困難な状態がある場合、メモリをバイパスできるように特別なテスト入力を追加して、ステートマシンを遠方に強制する必要が州。これにより、テスト中にすべての（抽象的な）状態をすばやくカバーできます。出力の識別可能性は、スケーラブルなテスト方法をサポートする重要なプロパティです。これにより、テスターは処理関数φを単純なラベルとして扱うことができ、次の統合レイヤーのステートマシンをテストする際に、その詳細な動作は無視しても問題ありません。一意の出力は監視値であり、特定の関数が呼び出されたことを保証します。
試験方法（ストリーム）Xマシンのテスト方法では、設計と実装の両方をストリームXマシン（のコレクション）と見なすことができると想定しています。対応するマシンの各ペア（Spec、Imp）について、テストの目的は、実装のマシンであるImpの動作が、仕様のマシンであるSpecの動作と正確に一致するかどうかを判断することです。注ことインプは最小限のマシンである必要はない-それは、より多くの状態と遷移を有することができる仕様とやはり同じように動作します。
すべての動作をテストするには、マシンをすべての状態に駆動してから、すべての可能な遷移（成功する必要があるものとブロックする必要があるもの）を試行して、完全なポジティブテストとネガティブテストを実行できる必要があります（上記を参照）。成功する遷移の場合、宛先の状態も確認する必要がSpecとImpの状態数が同じである場合、上記は目的を達成する最小のテストセットを説明していることに注意して場合インプがより多くの状態と遷移を持っている仕様、長いテストシーケンスをすることを保証するために必要な冗長内の状態インプが期待通りにも振る舞います。
すべての州をテストする
テスト生成戦略の基礎は、有限状態オートマトンをテストするためのTsun S. ChowのWメソッドであり、冗長な実装のテストをサポートするために選択されました。Chowの方法は、観測可能な入力と出力を備えた単純な有限状態マシンを想定していますが、直接観測可能な状態は想定しチョウの形式主義にマッピングする、関数をφのIの遷移にストリームX-マシンは単にラベル（チョウの用語で入力）と区別出力として扱われ、直接使用されます。（後で、実際の入力とメモリ（mem、in）からのマッピングが選択され、そのドメインに応じて各関数φがトリガーされます）。
Impの特定の状態を識別するために、Chowは特性化セットWを選択します。これは、Specの各状態を一意に特性化するテストシーケンスの最小セットです。つまり、特定の状態で開始する場合、Wでシーケンスを実行すると、他の状態で開始する場合と比較して、少なくとも1つの観察可能な違いが生じるはずです。
仕様で期待される各状態に到達するために、テスターは状態カバーCを作成します。これは、すべての状態に到達するテストシーケンスの最小セットです。これは、Specの自動幅優先探索によって構築できます。最小Impのすべての状態を検証するテストセットは次のとおりです。 ⊗ W {C otimes W}
、 どこ ⊗ { otimes}
2つのセットの連結された積を示します。例えば、C = {⟨ ⟩、⟨ B ⟩}およびW = {⟨ C ⟩、⟨ D ⟩}、次いで ⊗W = {{ ⟨ ⟩ ⟨ ⟩ ⟨ ⟩ ⟨ ⟩ } {C otimes W = { langle ac rangle、 langle ad rangle、 langle bc rangle、 langle bd rangle }}
。
すべての遷移をテストする
上記のテストセットは、最小のImpがSpecと同じ状態であるかどうかを判別します。最小のImpもSpecと同じ遷移動作を持つかどうかを判断するために、テスターは遷移カバーKを作成します。これは、すべての状態に到達し、その状態から可能なすべての遷移を1回試行するテストシーケンスの最小セットです。ここで、入力アルファベットはΦのすべての関数φ（のラベル）で構成されます。私たちはΦから選ばれた単一の機能からなる、長さ-1試験シーケンスのセットを構築し、このΦ呼びましょう1。トランジションカバーは次のように定義されます。 K ：= ∪ ⊗Φ 1
{K：= C cup C otimes Phi _ {1}}
。
これにより、すべての状態から可能なすべての遷移が試行されます。成功した場合は、宛先の状態を検証する必要がしたがって、最小のImpの動作を完全に検証する最小のテストセットT 1は、次の式で与えられます。 1
:: = ⊗ W ∪ ⊗
Φ1 W {T_ {1} :: = C otimes W cup C otimes Phi _ {1} otimes W}
。この式は、次のように再配置できます。 1
:: = ⊗（（ Φ0 Φ 1 ）。 ⊗ W {T_ {1} :: = C otimes left（ Phi _ {0} cup Phi _ {1} right） otimes W}
、
ここで、Φ 0は空のシーケンスを{}⟨⟩含むセットです。
ImpにSpecよりも多くの状態がある場合、上記のテストセットは、Impで複製された状態の適合動作を保証するのに十分でない可能性がだから、より長いテストシーケンスのセットは、関数Φのすべてのペアからなる、選択される2、関数Φのすべてのトリプル3いくつかの制限Φの最大kはテスターは、その満たされた場合に、IMPはより長い重複状態の鎖を含むことができませんK -1 。最終的なテスト式は次の式で与えられます。 k
:: = ⊗（（ Φ0
Φ1 ∪ Φ k ）。 ⊗ W {T _ { mathrm {k}} :: = C otimes left（ Phi _ {0} cup Phi _ {1} ldots cup Phi _ { mathrm {k}} right ） otimes W}
。
このテストセットは、重複状態のチェーンがk -1以下であると予想される非最小Impの動作を完全に検証します。ほとんどの実用的な目的では、k = 2またはk = 3までのテストは非常に徹底的であり、非常に貧弱な実装でのすべての状態関連の障害が明らかになります。
アプリケーション
あなたはそれに追加することによって助けることができます
参考文献
^ M. Holcombe and F. Ipate（1998）正しいシステム-ビジネスプロセスソリューションの構築。Springer、AppliedComputingシリーズ。
^ Gilbert Laycock（1993）仕様ベースのソフトウェアテストの理論と実践。シェフィールド大学博士論文。抽象 アーカイブで2007年11月5日、ウェイバックマシン
^ F. Ipate and M. Holcombe（1998）「一般化された機械仕様を改良およびテストする方法」。Int。J.Comp。算数。 68、pp。197–219。
^ F. Ipate and M. Holcombe（1997）「すべての障害を見つけることが証明されている統合テスト方法」、 International Journal of Computer Mathematics 63、pp。159–178。
^ K.BogdanovおよびM.Holcombe（1998）「ステートチャートの自動テストセット生成」、D。Hutter、W Stephan、P。Traverso、およびM.Ullmann編。Applied Formal Methods：FM-Trends 98、Boppard、Germany、 Lecture Notes in Computer Science 1641、pp.107–121。
^ Salim Vanak（2001）、ハードウェア設計の完全な機能テスト、博士論文、シェフィールド大学。
^ M. Holcombe（1988）「動的システム仕様の基礎としてのXマシン」、 Software Engineering Journal 3（2）、69〜76ページ。
^ T. S. Chow（1978）「有限状態マシンによってモデル化されたソフトウェア設計のテスト」、ソフトウェアエンジニアリングに関するIEEEトランザクション、4 （3）、178〜187ページ。
^ Florentin Ipate（1995）仕様とテストに応用できるXマシンの理論、博士論文、シェフィールド大学コンピュータサイエンス学部。
^ F. Ipate and M. Holcombe（2000）「非決定論的Xマシンのテスト」。In： Words、Sequences、Grammars、Languages：Where Biology、Computer Science、Linguistics and Mathematics Meet、Vol II、eds。CMartin-VideおよびV.Mitrana、Kluwer。”