最速

Fastest は、 Z 表記で記述された仕様を扱うモデルベースのテストツールです。このツールは、Phil Stocks と David Carrington によって提案された Test Template Framework (TTF) [ 1 ^{]を実装しています。 [ 2 ]}

Fastest はコマンドラインのユーザーインターフェイスを提供します。ユーザーはまず、ISO標準に準拠したLaTeX形式で記述された Z 仕様を読み込む必要があります。^{[ 3 ]}次に、テストする操作のリストと、それぞれの操作に適用するテスト戦術を入力する必要があります。3 番目のステップで、Fastest は各操作のテスト ツリーを生成します。テスト ツリーが生成されると、ユーザーはそれらとテスト クラスを参照でき、さらに重要なことに、任意のテスト クラスを自動または手動で剪定できます。テスト ツリーが剪定されたら、ユーザーは Fastest に各テスト ツリーの各リーフに対して 1 つの抽象テスト ケースを見つけるように指示できます。^{[ 4 ]}

現在、Fastestは以下のテスト手法をサポートしています。

• 選言標準形（DNF）。これは、デフォルトで適用される唯一のテスト手法であり（ユーザーが他のテスト手法を追加したかどうかに関わらず）、最初に適用される手法です。
• 標準パーティション（SP）。ユーザーは、テキストファイルを編集するだけで、定義済みの任意の Z 数学演算子の標準パーティションを追加、変更、削除できます。^{[ 5 ]}
• フリータイプ（FT）
• セット拡張（ISE）において
• 集合拡張の真部分集合（PSSE）
• 集合拡張の部分集合（SSE）

Fastest はテストツリーを剪定する 2 つの方法を提供します: ^{[ 6 ]}

• 自動剪定。

テストツリーを剪定するために、Fastest は各リーフの述語を分析し、その述語が矛盾であるかどうかを判断します。この問題は決定不能であるため、このツールはユーザーが改善できるベストエフォートアルゴリズムを実装しています。このアルゴリズムの最も重要な側面は、それぞれが矛盾のファミリーを表す、いわゆる消去定理のライブラリです。このライブラリは、テキストファイルを編集するだけでユーザーが拡張できます。消去定理は、パラメトリック Z 原子述語の論理積です。

• 手作業による剪定。

高速なユーザーは、2つのコマンドを実行することで、テストツリーのサブツリーまたは個々のリーフを剪定できます。これらのコマンドは、サブツリー内のすべてのテストクラスを、空であるかどうかにかかわらず剪定します。これらのコマンドの主な目的は、エンジニアがテストケースの数を減らしたり、重要でないテストケースを削除したりできるようにすることです。

このツールは、テストツリーの各リーフに対して有限モデルを計算することで、抽象的なテストケースを見つけます。 ^{[ 7 ]}有限モデルは、各VIS変数の型を有限セットに制限し、これらのセット間のデカルト積を計算することによって計算されます。各リーフ述語は、述語を満たすもの（つまり、抽象的なテストケースが見つかったもの）が見つかるか、またはすべてが尽きるまで（つまり、テストクラスが充足不可能であるか、有限モデルが不適切であるかのいずれかであるまで）、このデカルト積の各要素に対して評価されます。後者の場合、ユーザーはツールが適切な有限モデルを見つけるのを支援したり、充足不可能なテストクラスを剪定したりすることができます。

Fastest はCommunity Z Tools (CZT)プロジェクトに基づいたJavaアプリケーションです。このツールは、次の 2 つのモードのいずれかで使用できます。^{[ 8 ]}

• 分散モードでは、 Fastestはクライアント/サーバーアプリケーションとして動作します。アプリケーションは、クライアント、サーバー、またはその両方として機能する複数のコンピューターにインストールできます。ユーザーはクライアントを介してアプリケーションにアクセスし、クライアントはテストクラスをサーバー（テストサーバーと呼ばれる）に送信します。テストサーバーは、テストクラスから抽象テストケースを見つけ出そうとします。このようにして、最も負荷の高いタスクが可能な限り多くのコンピューターに分散されます。テストクラスから抽象テストケースを計算する処理は完全に独立しているため、このアーキテクチャはテストサーバーの数に比例して処理全体の速度を向上させます。
• アプリケーションモードでは、Fastestの各インスタンスは完全に独立しています。すべてのタスクはローカルコンピュータで処理されます。

パッケージclient.blogic.testing.ttree.tactics ;import java.util.* ; import net.sourceforge.czt.z.ast.Spec ; import common.z.TClass ; import common.z.OpScheme ;/** * テストツリーを生成するために必要なテスト戦術を抽象化し、* テストクラスに適用して新しいテストクラスを生成できるようにするインターフェース。*/ public interface Tactic { /** * 指定されたテストクラスにこの戦術を適用し、 生成されたテストクラス のリストを返します。  * @param tClass  * @return  */ public List < TClass > applyTactic ( TClass tClass ); /**  * テスト対象システムの仕様を設定します。 * @param opScheme  */ public void setSpec ( Spec spec ); /**  * テスト対象の操作の Z スキーマ ボックスを取得します。 * @return  */ public Spec getSpec (); /**  * テスト対象の操作の Z スキーマ ボックスを設定します。 * @param opScheme  */ public void setOriginalOp ( OpScheme opScheme ); /**  * テスト対象の操作の Z スキーマ ボックスを取得します。 * @return  */ public OpScheme getOriginalOp (); /**  * この戦術のパラメータを解析します。 * @param str  * @return  */ public boolean parseArgs ( String str ); /**  * このオブジェクトに関連付けられた TacticInfo のインスタンスを設定します。 * @param tacticInfo  */ public void setTacticInfo ( TacticInfo tacticInfo ); /**  * このオブジェクトに関連付けられた TacticInfo のインスタンスを取得します。 * @return  */ public TacticInfo getTacticInfo (); /**  * この戦術の説明を取得します。 * @return この戦術の説明を含む文字列。 */ public String getDescription (); /**  * この戦術の説明を設定します。 * @param description  */ public void setDescription ( String description ); }

• テストテンプレートフレームワーク
• モデルベーステスト

• Cristiá, Maximiliano; Rodríguez Monetti, Pablo (2009). "モデルベーステストのためのStocks-Carringtonフレームワークの実装と適用". Formal Methods and Software Engineering、第11回形式工学手法に関する国際会議、ICFEM 2009。リオデジャネイロ、ブラジル：Springer-Verlag。
• Stocks, Phil; Carrington, David (1996)、「仕様に基づくテストのためのフレームワーク」、IEEE Transactions on Software Engineering、22 (11): 777–793、doi : 10.1109/32.553698。
• 情報技術 — Z形式仕様表記法 — 構文、型システム、意味論（1 MB PDF）、2002年、 196ページISO /IEC 13568:2002
• Cristiá, Maximiliano; Albertengo, Pablo; Rodríguez Monetti, Pablo (2010). "数学的矛盾の検出によるテストテンプレートフレームワークにおけるテストツリーの剪定".第 8 回 IEEE 国際ソフトウェアエンジニアリングおよび形式手法会議 (SEFM)、2010 年。イタリア、ピサ: IEEE。