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

Trong đặc tả dựa trên mô hình, trạng thái của một hệ thống được mô hình hóa một cách rõ ràng bởi các cấu trúc toán học như tập hợp, ánh xạ, hàm, và quan hệ. Các hoạt động của hệ thống được định nghĩa bằng cách xác định ảnh hưởng của chúng đến trạng thái của hệ thống. Lý thuyết tập hợp, phép tính lambda, và logic vị từ làcácký hiệu toán học được sử dụng trong ngôn ngữ đặc tả. Thông thường, ngôn ngữ đặc tả dựa trên mô hình có các trạng thái và các hoạt động thay đổi trạng thái. Các bất biến là các biểu thức Boolean để hạn chế các tập của các trạng thái hợp lệ. Các hoạt động có thể có tiền điều kiện và hậu điều kiện liên quan. Tiền điều kiện xác định tập các trạng thái mà các hoạt động có thể xảy ra và hậu điều kiện xác định trạng thái đạt được sau khi thực hiện các hoạt động và giá trị trả về của hoạt động.