Loading article…
B法は、コンピュータソフトウェアの開発に使用される、抽象機械記法に基づくツール支援形式手法であるBに基づくソフトウェア開発手法である。[1] [2]
概要
Bはもともと1980年代にフランスとイギリスのJean-Raymond Abrial [3] [4]によって開発されました。BはZ表記法（これもAbrialが考案）に関連しており、仕様からプログラミング言語コードの開発をサポートしています。Bはヨーロッパの主要なセーフティクリティカルなシステムアプリケーション（パリ地下鉄14号線と1号線、アリアネ5ロケットなど）で使用されています。 [5] [6] [7]仕様、設計、証明、コード生成のための堅牢な市販ツールサポートがあります。
Z と比較すると、B は若干低レベルで、形式的な仕様よりもコードの改良に重点を置いています。そのため、B で記述された仕様は Z で記述された仕様よりも正しく実装しやすいです。特に、これに対するツール サポートは優れています。仕様、設計、プログラミングには同じ言語が使用されます。メカニズムにはカプセル化とデータ ローカリティが含まれます。
イベントB
その後、B法に基づいて、ロダンプラットフォーム[11] [12]のサポートを受けて、 Event-B [8] [9] [10]と呼ばれる別の形式手法が開発されました。Event -Bは、システムレベルのモデリングと分析を目的とした形式手法です。Event-Bの特徴は、モデリングに集合論を使用すること、異なる抽象化レベルでシステムを表現するために洗練を使用すること、そしてこれらの洗練レベル間の一貫性を検証するために数学的証明を使用することです。
主なコンポーネント
B 表記法は、プロジェクト開発の完全なサイクルをカバーするソフトウェアのさまざまなバージョンを指定するために、 集合論と第一階述語論理に依存します。
抽象機械
最初の最も抽象的なバージョンは「抽象マシン」と呼ばれ、設計者は設計の目標を指定する必要があります。
改良
- その後、改良のステップでは、目標を明確にするために仕様を補強したり、目標の達成方法を定義するデータ構造やアルゴリズムの詳細を追加して抽象マシンをより具体的にしたりすることがあります。
- Refinementと呼ばれる新しいバージョンは、一貫性があり、抽象マシンのすべてのプロパティが含まれていることが証明される必要があります。
- 設計者は、データ構造をモデル化したり、既存のコンポーネントを含めたりインポートしたりするために、B ライブラリを利用できます。
実装
- 決定論的なバージョン、つまり実装が達成されるまで、改良は続けられます。
- すべての開発ステップで同じ表記法が使用され、最終バージョンはコンパイルのためにプログラミング言語に翻訳される場合があります。
ソフトウェア
Bツールキット
B -Toolkit [13] [14]は、B-Tool の使用をサポートするために設計されたプログラミングツールのコレクションであり、[15] は、B-Method をサポートするために集合論に基づく数学的インタープリタです。開発は、当初はBP Research のIb Holm Sørensenらによって行われ、その後 B-Core (UK) Limited に移りました。[16]
このツールキットはGUI管理にカスタムX Window Motif Interface [17]を使用し、主にLinux、Mac OS X、Solarisオペレーティングシステム上で動作します。
B-Toolkitのソースコードが利用可能になりました。[18]
アトリエB
ClearSy社が開発したAtelier B [19] [20]は、Bメソッドを運用に利用して欠陥のない実証済みソフトウェア（フォーマルソフトウェア）を開発できる産業用ツールです。1) 誰でも制限なく使用できるコミュニティエディション、2) 保守契約者のみが使用できるメンテナンスエディションの2つのバージョンがあります。Atelier Bは、アルストムやシーメンスが世界各地に設置したさまざまな地下鉄の安全自動化システムの開発や、 ATMELやSTマイクロエレクトロニクスによるコモンクライテリア認証やシステムモデルの開発に使用されています。
ロダン
RodinプラットフォームはEvent-Bをサポートするツールです。[8] [21] [11] RodinはEclipseソフトウェアIDE（統合開発環境）に基づいており、改良と数学的証明のサポートを提供します。このプラットフォームはオープンソースであり、Eclipseフレームワークの一部を形成しています。ソフトウェアコンポーネントプラグインを使用して拡張可能です。Rodinの開発は、欧州連合プロジェクトDEPLOY（2008〜2012年）、RODIN（2004〜2007年）、およびADVANCE（2011〜2014年）によってサポートされています。 [8]
BHDL
BHDLは、ハードウェア記述言語VHDLの利点とBの形式性を組み合わせた、デジタル回路の正しい設計方法を提供します。 [22]
インド
APCB（フランス語：Association de Pilotage des Conférences B、国際B会議運営委員会）は、Bメソッドに関連する会議を開催してきました。[23] ZユーザーグループとのZB会議や、抽象ステートマシン（ASM）やZ表記法を含むABZ会議を開催してきました。
書籍
- 『B-Book: プログラムに意味を割り当てる』、Jean-Raymond Abrial、ケンブリッジ大学出版局、1996年。ISBN 0-521-49619-5 。
- B メソッド: 入門、Steve Schneider、Palgrave Macmillan、Cornerstones of Computing シリーズ、2001 年。ISBN 0-333-79284-X。
- Software Engineering with B、John Wordsworth、Addison Wesley Longman、1996年。ISBN 0-201-40356-0。
- B言語とメソッド：実践的な形式開発ガイド、Kevin Lano、Springer-Verlag 、 FACITシリーズ、1996年。ISBN 3-540-76033-4。
- 『Specification in B: An Introduction using the B Toolkit』、 Kevin Lano 著、World Scientific Publishing Company、Imperial College Press、1996 年。ISBN 1-86094-008-0。
- Event-B におけるモデリング: システムおよびソフトウェア エンジニアリング、Jean-Raymond Abrial、Cambridge University Press、2010 年。ISBN 978-0-521-89556-9。
会議
以下の会議では、B メソッドおよび/またはイベント B が明示的に組み込まれています。
- 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、英国コンピュータ協会、ロンドン、イギリス、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年
- ABZ 2020、ウルム、ドイツ、2021年（ COVID-19パンデミックのため延期）
- ABZ 2021、ウルム、ドイツ、2021年
参照
参考文献
- ^ Cansell, Dominique、および Dominique Méry。「B メソッドの基礎」。コンピューティングとインフォマティクス 22、第 3-4 号 (2003): 221-256。
- ^ バトラー、マイケル、フィリップ・ケルナー、セバスチャン・クリングス、ティエリー・ルコント、マイケル・ロイシェル、ルイス・フェルナンド・メヒア、ローラン・ヴォワザン。「Bメソッドの産業利用の最初の25年間」。産業クリティカルシステムのための形式手法に関する国際会議、pp. 189-209。シュプリンガー、チャム、2020年。
- ^ Jean-Raymond Abrial (1988)。「B ツール (概要)」(PDF)。Bloomfield, Robin E.、Marshall, Lynn S.、Jones, Roger B. (編)。VDM – The Way Ahead、 Proc . 2nd VDM-Europe Symposium。Lecture Notes in Computer Science。Vol . 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 年。
- ^ Gerhart, Susan, D. Craigen、および Ted Ralston。「ケーススタディ: パリの地下鉄信号システム」IEEE ソフトウェア11、第 1 号 (1994): 32-28。
- ^ Behm, Patrick、Paul Benoit、Alain Faivre、Jean-Marc Meynadier。「METEOR: 大規模プロジェクトにおける B の成功したアプリケーション」International Symposium on Formal Methods、pp. 369-387。Springer、ベルリン、ハイデルベルク、1999 年。
- ^ Lecomte, Thierry. 「業界における形式手法の適用: 15 年間の軌跡」。産業クリティカル システムのための形式手法に関する国際ワークショップ、pp. 26-34。Springer、ベルリン、ハイデルベルク、2009 年。
- ^ abc 「Event-Bとロダンプラットフォーム」。Event -B.org。
- ^ バトラー、マイケル。「イベント B の分解構造」。国際統合形式手法会議、pp. 20-38。シュプリンガー、ベルリン、ハイデルベルク、2009 年。
- ^ Abrial, Jean-Raymond. Event-B におけるモデリング: システムおよびソフトウェア エンジニアリング。ケンブリッジ大学出版局、2010 年。
- ^ ab Abrial、Jean-Raymond、Michael Butler、Stefan Hallerstede、Thai Son Hoang、Farhad Mehta、Laurent Voisin。「Rodin: Event-B のモデリングと推論のためのオープン ツールセット」技術移転のためのソフトウェア ツールに関する国際ジャーナル 12、第 6 号 (2010): 447-466。
- ^ Hoang、Thai Son、Andreas Fürst、Jean-Raymond Abrial。「イベント B パターンとそのツール サポート」ソフトウェア & システム モデリング 12、第 2 号 (2013): 229-244。
- ^ 「The B-Toolkit」[B-Core (UK) Limited] 2004年。2004年10月12日時点のオリジナルよりアーカイブ。2012年2月22日閲覧。
- ^ Haughton、Howard、Kevin Lano。B での仕様: B ツールキットを使用した入門。World Scientific、1996 年。
- ^ Abrial, Jean-Raymond. 「B ツール」。VDM ヨーロッパ国際シンポジウム、pp. 86-87。Springer、ベルリン、ハイデルベルク、1988 年。
- ^ ボウエン、ジョナサン（2022年7月）。「イブ・ホルム・ソーレンセン：10年後」（PDF）。FACS FACTS。第 2022-2号。BCS-FACS。pp.41-49。 2022年8月3日閲覧。
- ^ B-Toolkit 要件 2004-10-12 にWayback Machineにアーカイブ
- ^ Crichton, Edward. 「B-Toolkit ソースコード」。GitHub。
- ^ 「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 年。
- ^ Abrial, JR. 「Event-B と Rodin プラットフォームを使用したシステム開発プロセス」。International Conference on formal engineering methods、pp. 1-3。Springer、ベルリン、ハイデルベルク、2007 年。
- ^ Aljer、Ammar、Philippe Devienne、Sophie Tison、JL. Boulanger、Georges Mariano。「BHDL: B での回路設計」。2003 年の第 3 回システム設計への並行処理の適用に関する国際会議。議事録、pp. 241-242。IEEE、2003 年。
- ^ “水先案内協会 B”. librairiecosmopolite.com 。2022 年7 月 27 日に取得。
外部リンク
- B Method.com – 証明を伴う形式手法であるB法に関する作業と主題
- Atelier B.eu 2008-02-21にWayback Machineでアーカイブされました: Atelier Bは、欠陥のないことが保証されたソフトウェアを開発できるシステムエンジニアリングワークショップです。
- サイトB グルノーブル