Spesifikasi Formal sebagai Himpunan Perilaku

Program adalah daftar instruksi, sedangkan spesifikasi formal adalah himpunan perilaku.

Program terbagi menjadi transformasional (input-output tunggal) dan reaktif (berjalan lama dengan interaksi kontinu).

Perilaku (behavior) adalah eksekusi yang berisi urutan input dan output, baik yang benar maupun salah.

Spesifikasi formal memeriksa apakah suatu perilaku termasuk dalam himpunan perilaku yang benar.

Spesifikasi mendeskripsikan himpunan perilaku tak hingga dengan mendefinisikan generator Init dan Next.

Nondeterminisme dalam spesifikasi formal berarti terdapat beberapa cara valid untuk memperluas perilaku.

Properti sistem juga merupakan himpunan perilaku, dan verifikasi adalah pengecekan apakah spesifikasi merupakan subset dari properti.