Bメソッドは 、コンピュータソフトウェア の開発で使用される、抽象機械記法に基づくツールサポート型形式手法である B に基づくソフトウェア開発 手法です。[ 1 ] [ 2 ]
Z記法 と比較すると、B記法はやや低レベルであり、形式的な仕様記述 よりもコードへの洗練 に重点を置いています。そのため、Z記法で書かれた仕様よりもB記法で書かれた仕様の方が正しく実装しやすいと言えます。特に、この点に関して優れたツールサポートが提供されています。仕様記述、設計、プログラミングにおいて同じ言語が使用されます。カプセル化 やデータ局所性といったメカニズムも備えています。
イベントB その後、Rodin Platform [ 17 ] [ 18 ] Event-B [ 14 ] [ 15 ] [ 16 ]
主な構成要素 B表記法は、集合論 と一階述語論理 に基づいて、プロジェクト開発の全サイクルを網羅するさまざまなレベルのソフトウェア記述を指定する。
抽象機械 最初の、そして最も抽象的なバージョンである「抽象機械」 では、設計者は設計の目的を明確に定める必要がある。
洗練 そして、改良段階において、目標を明確にするため、あるいは目標達成の方法を定義するデータ構造やアルゴリズムに関する詳細を追加することで、抽象的な機械をより具体的にするために、仕様を補足することがある。 「Refinement」 と呼ばれるこの新バージョンは、一貫性があり、抽象機械のすべての特性を含んでいることが証明されるべきである。設計者は、データ構造をモデル化したり、既存のコンポーネントを含めたりインポートしたりするために、Bライブラリを利用する場合があります。
実装 決定論的なバージョンが実現するまで改良が続けられます。これが実装です 。 開発の全段階において同じ表記法が使用され、最終バージョンはコンパイルのためにプログラミング言語 に変換される場合がある。
ソフトウェア BメソッドとイベントBをサポートするソフトウェアは数多く存在する。
Click'n'Prove ツールは、証明義務の生成と解除、一貫性チェックと洗練チェックのための環境を提供する。[ 26 ]
会議 以下の会議では、Bメソッドおよび/またはイベントBが明示的に含まれています。[ 32 ]
Z2Bカンファレンス、フランス 、ナント 、1995年10月10日～12日 第1回Bカンファレンス、フランス・ナント、1996年11月25日～27日 第2回B会議、フランス、モンペリエ 、1998年4月22日～24日 ZB 2000、ヨーク 、イギリス 、2000年8月28日～9月2日 ZB 2002、グルノーブル 、フランス、2002 年 1 月 23 ～ 25 日 ZB 2003、トゥルク 、フィンランド 、2003 年 6 月 4 ～ 6 日 ZB 2005、ギルフォード 、イギリス、2005年 B 2007、ブザンソン 、フランス、2007 B、研究から教育へ、フランス、ナント、2008年6月16日 B、研究から教育へ、フランス、ナント、2009年6月8日 B、研究から教育へ、フランス、ナント、2010年6月7日 ABZ 2008、BCS 、ロンドン 、イギリス、2008年9月16日～18日 ABZ 2010、カナダ 、ケベック州 オーフォード 、2010 年 2 月 23 ～ 25 日 ABZ 2012、イタリア 、ピサ 、2012 年 6 月 18 ～ 22 日 ABZ 2014、トゥールーズ 、フランス、2014 年 6 月 2 ～ 6 日 ABZ 2016、オーストリア 、リンツ 、2016 年 5 月 23 ～ 27 日 ABZ 2018、英国サウサンプトン、2018年6月5日～8日 ABZ 2020、ドイツ ・ウルム 、 2020年6月9日～13日（新型コロナウイルス感染症（COVID-19 ）のパンデミックのため延期） ABZ 2021、ドイツ・ウルム、2021年6月9日～13日 ABZ 2023、フランス、ナンシー 、2023年5月30日～6月2日 ABZ 2024、ベルガモ 、イタリア 、2024 年 25 ～ 28 日 ABZ 2025、デュッセルドルフ 、ドイツ、2025 年 6 月 10 ～ 13 日 ABZ 2026、東京 、日本、2026 年 5 月 18 ～ 20 日
参考文献 ↑ Cansell, Dominique、および Dominique Méry。「B メソッドの基礎」。Computing and informatics 22、no. 3-4 (2003): 221-256。 ↑ Butler, Michael、Philipp Körner、Sebastian Krings、Thierry Lecomte、Michael Leuschel、Luis-Fernando Mejia、Laurent Voisin 。「Bメソッドの産業利用の最初の25年間」。『産業クリティカルシステムのための形式手法に関する国際会議』、pp. 189-209。Springer、Cham、2020年。 ↑ Jean-Raymond Abrial (1988). "The B Tool (Abstract)" (PDF) . Robin E. Bloomfield、Lynn S. Marshall、Roger B. Jones (編)『 VDM – The Way Ahead、第2回VDM-Europeシンポジウム議事録 』 Lecture Notes in Computer Science 、第328巻 、 Springer 、 pp. 86–87。doi : 10.1007/ 3-540-50214-9_8。ISBN 978-3-540-50214-2 。↑ Abrial, JR.、Matthew KO Lee、DS Neilson、PN Scharbach、および Ib Holm Sørensen。「Bメソッド」。International Symposium of VDM Europe、pp. 398-405。Springer、ベルリン、ハイデルベルク、1991年。 ↑ Bowen, Jonathan P. ; Habrias, Henri (2025 年 4 月～6 月). "Jean-Raymond Abrial: A Scientific Biography of a Formal Methods Pioneer". IEEE Annals of the History of Computing . 48 (2). IEEE Computer Society : 71– 80. arXiv : 2604.07353 . doi : 10.1109/MAHC.2026.3685515 . ↑ Gerhart, Susan、D. Craigen、および Ted Ralston。「ケーススタディ：パリ地下鉄信号システム」 IEEE Software 11、no. 1 (1994): 32-28。 ↑ Behm, Patrick、Paul Benoit、Alain Faivre、Jean-Marc Meynadier。「METEOR：大規模プロジェクトにおけるBの成功事例」。『形式手法に関する国際シンポジウム』、pp. 369-387。Springer、ベルリン、ハイデルベルク、1999年。 ↑ ルコント、ティエリー。「産業界における形式手法の適用：15年の軌跡」。『産業クリティカルシステムのための形式手法に関する国際ワークショップ』、pp. 26-34。シュプリンガー、ベルリン、ハイデルベルク、2009年。 ↑ Bhattacharya, Sourav; Winter, Victor L. 編 (2012). "8. B の歴史". High Integrity Software. Springer . p. 40. ISBN 978-1461513919 。 1 2 Bowen, Jonathan (2022年7月)。 「Ib Holm Sørensen: 10年後」 (PDF) 。FACS FACTS ( 2022–2 )。BCS -FACS : 41–49 。 2022年 8月3日 取得 。 ↑ クリクトン、エドワード (2022年3月29日)。「 BToolkit」。GitHub。 ↑ ロスコー、ビル （2012年2月8日）。「イブ・ソーレンセン追悼」。オックスフォード大学コンピュータサイエンス学部 、英国。↑ Wordsworth, JB (1996). Software Engineering With B. Addison-Wesley. ISBN 978-0201403565 1 2 3 「Event-Bとロダン・プラットフォーム」 . Event-B.org . ↑ バトラー、マイケル。「イベントBの分解構造」。国際統合形式手法会議、pp. 20-38。シュプリンガー、ベルリン、ハイデルベルク、2009年。 ↑ アブリアル、ジャン＝レイモンド。『Event-Bにおけるモデリング：システムとソフトウェアエンジニアリング』ケンブリッジ大学出版局 、2010年。 1 2 Abrial, Jean-Raymond、Michael Butler、Stefan Hallerstede、Thai Son Hoang、Farhad Mehta、Laurent Voisin。「Rodin: Event-B でのモデリングと推論のためのオープンなツールセット」International Journal on Software Tools for Technology Transfer 12、no. 6 (2010): 447–466。 ↑ Hoang, Thai Son、Andreas Fürst、Jean-Raymond Abrial。「Event-Bパターンとそのツールサポート」。Software & Systems Modeling 12、no. 2 (2013): 229–244。 ↑ "AtelierB.eu" . ↑ Mentré, David、Claude Marché、Jean-Christophe Filliâtre、Masashi Asuka。「複数の自動証明器を使用したAtelier Bからの証明義務の解除」。International Conference on Abstract State Machines、Alloy、B、VDM、Z、pp. 238-251。Springer、ベルリン、ハイデルベルク、2012年。 ↑ 「B-Toolkit」 。 [B-Core (UK) Limited] 。2004年。 2004年10月12日の オリジナル からアーカイブ。 2012年 2月22日 取得 。 ↑ ハワード・ホートン、ケビン・ラノ。『B言語による仕様記述：Bツールキットを用いた入門』ワールド・サイエンティフィック、1996年。 ↑ アブリアル、ジャン＝レイモンド。「Bツール」。VDMヨーロッパ国際シンポジウム、pp. 86-87。シュプリンガー、ベルリン、ハイデルベルク、1988年。 ↑ B-Toolkitの要件は、 2004年10月12日にWayback Machine に アーカイブされました。 ↑ クリクトン、エドワード。 「B-Toolkit ソースコード 」 。GitHub 。 ↑ Abrial, J.-R.; Cansell, D. (2003). "Click'n Prove: 集合論における対話型証明". Basin, D.; Wolff, B. (編). 高階論理における定理証明 (TPHOLs) . Lecture Notes in Computer Science . Vol. 2758. Berlin, Heidelberg: Springer. doi : 10.1007/10930755_1 . ↑ 「ProBとは何か？」 。ドイツ： ハインリッヒ・ハイネ大学デュッセルドルフ。 2026年 3月28日 取得 。 ↑ 「ProB?」 。 railML.org 。 2026年 3月28日 取得 。 ↑ Abrial, JR.「Event-BとRodinプラットフォームを用いたシステム開発プロセス」『形式工学手法に関する国際会議』pp. 1–3. Springer、ベルリン、ハイデルベルク、2007年。 ↑ Aljer, Ammar、Philippe Devienne、 Sophie Tison 、JL. Boulanger、および Georges Mariano。「BHDL: B による回路設計」。第 3 回システム設計への並行性適用に関する国際会議議事録、pp. 241–242。IEEE、2003 年。 ↑ 「水先案内協会 B」 . librairiecosmopolite.com 。 2022 年 7 月 27 日 に取得 。 ↑ 「会議」 . ABZ . 2026年 1月16日 取得 。 
