形式手法の事例
採用例
クラウド
DeNA
組み込み
BPS1000紙幣検査機
航空系、航空管制
Airbus（フランス）
金融
証券バックオフィスパッケージ
仕様記述言語
VDM++
CSK
VISA
ブロックチェーン
ConsenSys社、Ethereumエコシステム
形式検証（Isabelle/HOLによる定理証明）
イーサリアム2.0の預入契約（Depositコントラクト）
電子商取引(金融？)
言語処理
セキュリティ
米国国家安全保障庁(NSA)の生体認証システム
使用記述言語
マスターカード認証サーバ
仕様記述言語
UML
自然言語
Data61/CSIRO（オーストラリア）
Isabelle/HOLを用い、組込みOSカーネル「seL4」の完全な形式検証を世界で初めて達成 Common Criteria EAL6+相当
鉄道関係
クルーズコントロール
エネルギー
MTUフリードリヒスハーフェン社（独）
アレバ社（現Orano、仏）
ゲーム
FINAL FANTASY XV
確認用
Q. 形式手法の事例
参考
2012/11/15
関連