数理論理学・集合論等に基づく厳密な数学的言語を使って仕様・設計を厳密に記述する

主が計算であるソフトウェア向けの手法

Z, OBJ, VDM, Bメソッド

リアクティブシステム向けの手法

CSP, π計算、LOTOS

事例

フェリカ

VDMを利用

ライフロボティクス

自社開発の仕様記述言語