フォーマルメソッドとは？
アトリエでは「フォーマルメソッド」を「安全の安⼼」のエビデンス作りに活かしています。
フォーマルメソッド（形式手法）は、数学や数理論理学に基づいて正しいソフトウェアを開発するための手法であり、ソフトウェア工学の重要な研究分野として発展してきました。今日では、高信頼システム工学やデータバリデーションへと適用範囲を広げています。フォーマルメソッドの主な用途は、次の3つに分類できます。
１）フォーマル仕様記述
システムの要求仕様を形式的な記述により定義します。これにより、仕様の定義もれを防ぎ、解釈のあいまいさを排除します。
２）フォーマル検証
システムにおいて期待されるプロパティ（安全性など）が成り立つことを、論理的な証明によって立証します。そのために、プロパティを形式的に記述したうえで、ツールを用いて、自動的または対話的に証明を実施します。これにより、網羅的な検証が可能となります。
３）フォーマルプログラム合成
フォーマル仕様記述からプログラムを自動生成します。仕様を満たすプログラムを正しく生成します。
さまざまなフォーマルメソッドとBメソッド
フォーマルメソッドには様々な手法が存在します。下図は、おもな手法を用途ごとに分類したものです。これらのうち、アトリエでは特にBメソッドを活用しています。Bメソッドは色々な用途に活用できる、実践的なフォーマルメソッドです。
フォーマルメソッドの⼿法と対応範囲
フォーマルメソッドの⼿法と使⽤率
出典：IPA/SEC「形式⼿法適⽤調査報告書」（2010年7⽉29⽇公開）
Bメソッド（B-Method）
について
Classical BとEvent-B
Bメソッドは、現在では「Classical B」と「Event-B」という2つの流派が確立しており、目的に応じて使い分けます。
Classical Bは、要求仕様を事前条件・事後条件および不変条件により定義した上で、定理証明で検証しながら詳細化することで、仕様をみたすプログラム実装を導きます。ソフトウェア開発工程の中では、要求仕様の作成、設計、実装に向いています。
これに対して、Event-Bはシステム設計に向いています。Event-Bでは、システムを外部コンポーネントや操作者といった環境要因も含めてモデル化し、相互作用によるシステムの振る舞いを分析・検証します。基本性質を表す仕様を出発点として、段階的詳細化（リファインメント）をほどこすことにより、複雑な制御ロジックまでを論理の飛躍なく導出できます。
Event-B による開発の特徴
Event-Bによる開発の進め方には、次の2つの特徴があります。
１）システムに求める性質を明確にする
システム要求から、システムが満たすべき性質を不変条件としてフォーマル記述します。
２）リファインメントにより段階的に具体化し検証する
下図のように、基本的な初期モデルから出発して徐々に複雑なシステムを構成していきます。リファインメントを経ても不変条件が成立するようにすることで、システムの妥当性が確認しやすくなります。
アトリエでのフォーマルメソッドの活用
アトリエではEvent-Bをはじめとするフォーマルメソッドの適用ノウハウを蓄積しており、安全性検証に活用しています。
- システムの安全要求をフォーマル記述する
- システムの振舞いをフォーマル記述し、検証する
- 安全な振舞いのための前提条件を明確にする