形式仕様記述言語
Specification language
数理論理学・集合論等に基づく厳密な数学的言語を使って仕様・設計を厳密に記述する
主が計算であるソフトウェア向けの手法
Z
,
OBJ
,
VDM
,
Bメソッド
リアクティブシステム
向けの手法
CSP
,
π計算
、
LOTOS
事例
https://www.ipa.go.jp/files/000044283.pdf
フェリカ
VDM
を利用
http://jasst.jp/symposium/jasst17tokyo/pdf/D3.pdf
ライフロボティクス
自社開発の仕様記述言語
https://www.principia-m.com/slides/formal_methods.pdf