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.