形式手法(Bメソッド)

形式手法とは

形式手法は、数学を基盤としたソフトウエアやシステムの仕様記述、検証、開発手法の総称で、数多くの手法が考案されています。 形式仕様記述を用いて厳密に仕様を定義することによる仕様の曖昧性の排除・仕様の前提条件の明確化や、形式検証での数学的解析による開発ソフトウェアの信頼性・頑健性の向上が可能となります。

形式手法の分類

・形式仕様記述
– モデル規範…集合論・述語論理を用いて仕様を表現
– 性質規範…代数仕様を用いて仕様を表現
・形式検証
– 定理証明…要求・仕様と設計や実装との間の論理的整合性や一貫性処理の正しさを数学的に証明する
– モデル検査…振る舞いについて全状態空間を時相論理式などを用いて自動検査
・形式プログラム合成

形式手法の分類

機能安全規格IEC 61508や情報セキュリティ評価の為のコモンクライテリアISO/IEC15408といった安全性やセキュリティを保証する為の国際規格では、特に高信頼性が求められる高い水準の保証の為に形式手法を適用することを求めています。

ISO/IEC15408 情報技術セキュリティ評価の為の共通基準の形式手法の適用要求

保証コンポーネント 内容 評価保証レベル
ADV_SPM.1 形式的なTOE セキュリティ方針モデル EAL5~7
ADV_FSP.6 追加の形式的仕様を伴う完全な準形式的機能仕様 EAL7
ADV_TDS.6 形式的な上位レベルの設計提示を伴う完全な準形式的モジュール設計 EAL7

IEC 61508 ソフトウェア安全要求への形式手法適用の推奨

要求項目 推奨 強い推奨
システム安全検証のソフトウェア観点をカバーする形式モデリング SIL2~3 SIL4
ソフトウェア安全要求の仕様記述への形式手法の使用 SIL2~3 SIL4
ソフトウェアアーキテクチャ設計とソフトウェア詳細設計への形式設計と詳細化手法の使用 SIL2~3 SIL4
ソフトウェア検証への形式証明の使用 SIL2~3 SIL4
ソフトウェアモジュールテストと結合への形式検証の使用 SIL3~4

Bメソッドとは

[Bファミリー]
Bメソッドのファミリーには、システムモデリングの為のEvent-Bとソフトウェア開発の為のBメソッド(Event-Bに対して、Classical Bと呼ばれることもあります)があります。

[Bメソッド]
Bメソッドは形式仕様記述言語であるZ記法を元にVDMのアイデアを取り入れてソフトウェアを構造化し、モジュールの要件・仕様と実装の整合性・一貫性を全て論理的な証明により保証しながら実行コードを導出する一連のソフトウェア開発手法です。

Bメソッドでは、モジュールの仕様を一階述語論理を用いて仕様を高い抽象度でかつ厳密に定義した上で、論理の飛躍を抑えながら徐々に詳細化して実装表現を導きます。

Bメソッドによる仕様記述と実装

ソフトウェア全体の構造は、最上位のモジュールI/Fを決め、サブモジュールにブレークダウンするといったスタイルでソフトウェア全体構造を定義していきます。処理の正しさを保証する為に、あるモジュールの状態値を更新するアクセスは1つのモジュールに限定するといった制約を設けている為、ソフトウェア全体構造がツリー状のシンプルな呼出し関係で表現できるという特徴があり、Bメソッドのソフトウェア構造を表現するこのツリーのダイアグラムをインポートツリーと呼んでいます。

Bメソッドによるソフトウェアの構造化

ソフトウェア全体の構造は、最上位のモジュールI/Fを決め、サブモジュールにブレークダウンするといったスタイルでソフトウェア全体構造を定義していきます。処理の正しさを保証する為に、あるモジュールの状態値を更新するアクセスは1つのモジュールに限定するといった制約を設けている為、ソフトウェア全体構造がツリー状のシンプルな呼出し関係で表現できるという特徴があり、Bメソッドのソフトウェア構造を表現するこのツリーのダイアグラムをインポートツリーと呼んでいます。

Bメソッドによるソフトウェア開発のメリット

・形式仕様は自然言語の仕様に非常に近い形で表現できる(何をすべきなのかを表す)
・要求が仕様としてモジュール毎に明記でき、その仕様と実装との一貫性が証明により保・証できる
・検証しやすい健全なプログラム構造が強制される
・昔ながらのプログラムエラーは排除される(オーバーフロー、配列の範囲超えアクセス、0割、無限ループなど)
許容する全ての条件組合せで、実装表現の処理結果が望んだ仕様どおりになることが保証される(条件網羅の為の単体テストが軽減できる)
・証明により設計・実装の誤りを早期に検出でき、修正の為の手戻りがなくなる
・ソフトウェアの修正・改訂時に、影響範囲がツールにより自動検出できる

Event-B

Bメソッドにアクションシステム(並行分散処理)の概念を取り入れ、システム仕様検討をできるようにしたのがEvent-Bです。 単純化した要件から徐々に肉付けをしながらシステムをモデル化し、要件とモデルの整合性検証をすることができます。

Bメソッドは一般にシングルタスクのソフトウェア動作を表現しますが、Event-Bはマルチタスク間の協調動作のモデリング・検証も可能です。 さらに開発対象のソフトウェア動作のみでなく、通信であれば通信相手、ハードウェアや操作者などの環境要因をモデルに含めて、それらとの関わりによる振る舞いをモデリング・検証することもできます。

Event-Bでの段階的詳細化を用いたシステムモデリング

Bメソッドにアクションシステム(並行分散処理)の概念を取り入れ、システム仕様検討をできるようにしたのがEvent-Bです。 単純化した要件から徐々に肉付けをしながらシステムをモデル化し、要件とモデルの整合性検証をすることができます。

Bメソッドは一般にシングルタスクのソフトウェア動作を表現しますが、Event-Bはマルチタスク間の協調動作のモデリング・検証も可能です。 さらに開発対象のソフトウェア動作のみでなく、通信であれば通信相手、ハードウェアや操作者などの環境要因をモデルに含めて、それらとの関わりによる振る舞いをモデリング・検証することもできます。

Event-Bによるシステムモデリングのメリット

Bモデル構築により、不明点が確認され、システムを深く理解できる。
システム設計レベルのエラーを早期に検出でき、ソフトウェア仕様を改善できる。

ヴィッツのBメソッドへの取り組み

弊社は機能安全や組込みセキュリティといった基盤技術開発の為の研究事業で自動車部品の制御ソフトウェアや組込み用通信ミドルウェアをBメソッドを用いて開発するなど、Bメソッドの組込みソフトウェア開発への実践適用に取り組んできました。

また2012年にはBメソッドによるソフトウェア開発ツールの開発元であるフランスのClearSy社と日本におけるBメソッドの普及に向けて提携するなど積極的な取り組みを行っています。

Bメソッド開発ツール ATELIER B(関連情報リンク)

ATELIER Bの開発元CLEARSY社

CQ出版 Interface誌に連載したBメソッド紹介記事 (弊社と共同研究企業で執筆したものです)

第9回クリティカルソフトウェアワークショップ(WOCS2)発表資料
「Bメソッドを用いた組込みソフトウェア自動コード生成の実用性評価」 (弊社と共同研究企業によるレポートです)

お問い合わせはコチラ

ご相談・ご質問等ございましたら、
お気軽にお問い合わせください。

株式会社ヴィッツ
〒460-0008 
名古屋市中区栄2-13-1名古屋パークプレイス 1F
TEL (052)220-1218 / FAX (052)218-5855