Phần mềm-Ứng dụng

            Các phương thức là tương đương nếu người dùng có thể chọn một trong những phương thức đó để đạt được trạng thái mong muốn từ trạng thái hiện hành. Gọi M1, M2 là hai phương thức. E_M1, E_M2 là hai sự kiện của M1, M2 tương ứng. Hai phương thức M1, M2 là tương đương đối với tập nhiệm vụ T, nếu mỗi nhiệm vụ tÎT có thể được kích hoạt bởi E_M1 hoặc E_M2. Tính tương đương thừa nhận một sự kiện đầu vào duy nhất là có thể sinh kết quả đầu ra. Tác giả đã bổ sung phép toán TestEquivalence vào ngôn ngữ TTT để kiểm tra thuộc tính tương đương giữa hai sự kiện E_M1, E_M2.

Cú pháp: TestEquivalence(E_M1, E_M2, T, tw)

Trong đó, iÎ[1, n], E_Mi là các sự kiện, T là nhiệm vụ, tw là cửa sổ thời gian.