IPAが形式手法調査結果を公開していたので読みました

プレス発表 形式手法適用調査報告書の公開：IPA 独立行政法人 情報処理推進機構

IPAが形式手法に関する言語（仕様？）、ツール、事例の調査結果を公開していたので読みました。

以下、メモ。

• VDM以外にもBとか色々仕様があるらしい。
• 事例は主に組み込み系（列車制御とか航空制御とか）。やっぱり業務システムには向かないのか事例はまだないみたい。
• 形式手法はISO化されている
• 形式手法はレベルがいくつかある
• RFP？などに形式手法の使用が推奨されていることがある
• 開発工程の全般に使うものとは限らない。設計-検証や安全性確認（セーフティケース？）で使うことが多い。

具体的にどういうコードを書くのかまでは書いてないのですが、その辺も知りたい。将来的には組み込み開発をする人材は形式手法で仕様を書けることが要件になるかもしれないですね。

最近のIPAは調査公開が多くてウォッチする価値あります。