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

Một TESTCTT có nhiều đầu vào và nhiều đầu ra. Các đầu vào của TESTCTT tương ứng với các đầu ra của ứng dụng tương tác và các đầu vào của TESTCTT tương ứng với các đầu ra của ứng dụng tương tác. Mệnh đề sets định nghĩa các kiểu dữ liệu được sử dụng trong TESTCTT. Trong ngôn ngữ TTT có các kiểu dữ liệu boolean, integer hoặc kiểu liệt kê. Mệnh đề var trình bày các biến trạng thái của mô hình kiểm thử. Các biến trạng thái cung cấp một khung nhìn trừu tượng về trạng thái hiện hành của ứng dụng tương tác. Bước chính trong việc thiết kế mô hình là lựa chọn các biến trạng thái và các kiểu dữ liệu của chúng. Sự lựa chọn của các biến trạng thái phụ thuộc vào những thuộc tính cần thiết để kiểm soát và quan sát các hành vi của các ứng dụng tương tác.