形式手法が適しているもの
抽象的なライブラリのコードの検証
仕様バグの検出
デッドロックやデータレース、レースコンディション等、確率的に発生する不具合の防止
分散処理、分散アルゴリズム、スマートコントラクト
モジュールを結合した時の不整合の検出
ドメインごとにどんなものが適しているか
飛行制御システム
姿勢制御アルゴリズムの論理検証（NASAがよく使うTLA+やPVS）
フェイルセーフ条件の証明（ドローン、自律飛行体）
衛星通信・地上局
通信プロトコルのモデル検証（TLA+、SPIN）
電波干渉やプロトコル不整合の形式モデル（Alloy）
鉄道 (Railway Systems)
信号・ポイント制御システム
誤った進路設定の回避（Bメソッド、Event-B）
自動列車運転(ATO)システムの安全性証明（VDM、SPARK/Ada）
運行スケジュール最適化
スケジュール生成ロジックの正当性証明（Z記法、Alloy）
スケジュール不整合検出・解決モデル（Alloy, SMT）
参考
ChatGPT.iconhttps://chatgpt.com/share/6825a290-dc38-800d-9a49-2104d25455e1