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

Kỹ thuật đặc tả ứng dụng dựa trên hành vi cho phép áp dụng kỹ thuật kiểm tra mô hình để xác minh tính chất của ứng dụng tương tác một cách tự động. Loại đặc tả này cũng phù hợp với mô hình hệ thống đồng thời. Chúng xác định hệ thống phần mềm như chuỗi các trạng thái. Ví dụ, các ký hiệu dựa trên hành vi gồm mạng Petri, quá trình đại số, và logic thời gian. Một mạng Petri bao gồm các điểm, các chuyển tiếp, và các cung có hướng. Tại mỗi thời điểm trong quá trình thực hiện của nó, điểm có thể chứa không hoặc nhiều thẻ. Một chuyển tiếp dùng các thẻ từ các điểm đầu vào và các thẻ đầu ra đến những điểm đầu ra. Một chuyển tiếp xảy ra khi những điểm vào của nó chứa đủ số lượng thẻ yêu cầu. Keh và Lewis, trong [39], sử dụng mạng Petri gắn chú thích để mô hình hóa giao diện thao tác trực tiếp. Các chú thích cho phép đặc tả các điều kiện và thực hiện của các đối tượng được kích hoạt đồng thời. Palanque, trong [40], trình bày một mô hình hướng đối tượng được thiết kế đặc biệt cho các giao diện hướng sự kiện. Hình thức này, được gọi là đối tượng hợp tác tương tác (Interactive Cooperative Objects-ICO), dựa trên mạng Petri. Mỗi đối tượng bao gồm bốn thành phần: cấu trúc dữ liệu, hoạt động, biểu diễn, và hành vi. ICO được sử dụng để mô tả các khía cạnh cấu trúc tĩnh của hệ thống trong khi khía cạnh động hoặc hành vi của hệ thống được mô phỏng theo một mạng Petri cấp độ cao với các đối tượng được gọi là cấu trúc điều khiển đối tượng (Object Control Structure-ObCS).Có nhiều phương pháp phát sinh ca kiểm thử  từ đặc tả dựa trên hành vi. Logic thời gian là một trong những ví dụ và có thể được sử dụng bởi kỹ thuật kiểm chứng mô hình (model checking) để sinh các ca kiểm thử. Ngoài ra còn có phương pháp phân tích các dấu vết hoạt động [41] (Communicating Sequential Processes - CPS) để tạo ra các ca kiểm thử.