B-Method
B法は方法であるソフトウェアの開発に基づいてB、工具支持形式手法に基づく抽象機械表記コンピュータの開発に使用される、ソフトウェア。もともとは1980年代にフランスとイギリスのジャンレイモンドアブリアルによって開発されました。BはZ表記（これもAbrialによって作成されたもの）に関連しており、仕様からプログラミング言語コードの開発をサポートします。Bは、ヨーロッパの主要なセーフティクリティカルシステムアプリケーションで使用されています。（自動パリメトロ14号線と1号線、アリアン5ロケットなど）。仕様、設計、証明、およびコード生成のための堅牢な市販のツールサポートが
Zと比較して、Bはわずかに低レベルであり、正式な仕様ではなくコードの改良に重点を置いています。したがって、Zで記述された仕様よりもBで記述された仕様を正しく実装する方が簡単です。これ。同じ言語が仕様、設計、プログラミングで使用されています。メカニズムには、カプセル化とデータの局所性が含まれます。
その後、Event-B と呼ばれる別の形式手法が開発されました。イベントBは、Bの進化と見なされます（クラシックBとも呼ばれます）。これはより単純な表記法であり、習得と使用が容易です。Rodinツールの形でツールサポートが付属しています。
コンテンツ
1 主なコンポーネント
1.1 抽象機械 1.2 洗練 1.3 実装
2 ソフトウェア
2.1 B-ツールキット 2.2 アトリエB 3 本 4 会議
5 も参照してください
6 参考文献
7 外部リンク
主なコンポーネント
B表記は、プロジェクト開発の完全なサイクルをカバーするソフトウェアのさまざまなバージョンを指定するために、集合論と一階述語論理に依存します。
抽象機械
抽象マシンと呼ばれる最初の最も抽象的なバージョンでは、設計者は設計の目標を指定する必要が
洗練
次に、改良ステップ中に、目標を明確にするため、または目標の達成方法を定義するデータ構造とアルゴリズムに関する詳細を追加することにより、抽象マシンをより具体的にするために、仕様を埋めることができます。
Refinementと呼ばれる新しいバージョンは、一貫性があり、抽象マシンのすべてのプロパティを含むことが証明されている必要が
設計者は、データ構造をモデル化するため、または既存のコンポーネントを含めたりインポートしたりするために、Bライブラリを利用できます。
実装
改良は、決定論的なバージョンが達成されるまで続きます：実装。
すべての開発ステップで同じ表記が使用され、最後のバージョンがコンパイル用のプログラミング言語に翻訳される場合が
ソフトウェア
B-ツールキット
B-ツールキット、によって開発されたIbのホルムセーレンセン ら。は、Bメソッドとして知られる正式なソフトウェアエンジニアリング方法論の目的で、集合論ベースの数学的インタープリターであるBツールの使用をサポートするように設計されたプログラミングツールのコレクションです。
このツールキットは、GUI管理にカスタムX Window Motifインターフェイスを使用し、主にLinux、Mac OS X、およびSolarisオペレーティングシステムで実行されます。これは、英国を拠点とする会社B-Core（UK）Limitedによって開発されました。
B-Toolkitのソースコードが利用可能になりました。
アトリエB
ClearSyによって開発されたAtelierB は、Bメソッドを運用上使用して、欠陥のない実証済みのソフトウェア（正式なソフトウェア）を開発できるようにする産業用ツールです。コミュニティエディションは誰でも無制限に利用でき、メンテナンスエディションはメンテナンス契約者のみが利用できます。
これは、AlstomとSiemensによって世界中に設置されたさまざまな地下鉄の安全自動化を開発するために使用されます。また、CommonCriteria認証とATMELおよびSTMicroelectronicsによるシステムモデルの開発にも使用されます。
本
B-帳：意味に割り当てプログラム、ジーン・レイモンド・アブリアル、ケンブリッジ大学出版、1996年ISBN 0-521-49619-5。
B-方法：入門、スティーブ・シュナイダー、Palgrave Macmillan社、コンピューティングシリーズの基礎、2001年
ISBN 0-333-79284-X 。
Bとソフトウェア工学、ジョン・ワーズワース、アディソンウェスリー・ロングマン、1996年
ISBN 0-201-40356-0。
B言語と方法：Aガイド実践形式的開発に、ケビン・ラノ、シュプリンガー・フェアラーク、FACITシリーズ、1996年
ISBN 3-540-76033-4。
Bでの仕様：B Toolkitを使用して入門、ケビン・ラノ、世界の科学出版社、インペリアル・カレッジ・プレス、1996年
ISBN 1-86094-008-0。
イベント-Bにモデル化：システムとソフトウェア工学、ジーン・レイモンド・アブリアル、ケンブリッジ大学出版、2010年
ISBN 978-0-521-89556-9。
会議
会議Z2B、ナント、フランス、10月。1995年10月12日
最初のB会議、ナント、フランス、11月。1996年25〜27日
第2回B会議、フランス、モンペリエ、ap。1998年22〜24日、
ZB’2000、英国ヨーク、8月28日、9月2日 2000、
ZB’2002、フランス、グルノーブル、1月23〜25日。2002年、
ZB’2003、フィンランド、トゥルク、6月4〜6日。2003年
ZB’05、英国ギルフォード、2005年
B ‘2007、フランス、ブザンソン、2007年
B、研究から教育まで、フランス、ナント、2008年6月16日
B、研究から教育まで、フランス、ナント、2009年6月8日
B、研究から教育まで、フランス、ナント、2010年6月7日
ABZ会議：ABZ 2008、British Computer Society、ロンドン、英国、2008年9月16〜18日
ABZ会議：ABZ 2010、カナダ、ケベック州オックスフォード、2010年2月23〜25日
ABZ会議：ABZ 2012、イタリア、ピサ、2012年6月18〜22日
ABZ会議：ABZ 2014、フランス、トゥールーズ、2014年6月2〜6日
ABZ会議：ABZ 2016、オーストリア、リンツ、2016年5月23〜27日
も参照してください
APCB（Association dePilotagedesConférencesB）
BHDL
参考文献
^ ジャン・レイモン・アブリアル（1988）。「Bツール（要約）」（PDF）。ロビンE.ブルームフィールドとリンS.マーシャルとロジャーB.ジョーンズ（編）。VDM —先の道、Proc。第2回VDM-ヨーロッパシンポジウム。コンピュータサイエンスの講義ノート。328。スプリンガー。pp。86–87。土井：10.1007 / 3-540-50214-9_8。ISBN
978-3-540-50214-2。
^ Event-B.org —Event-BとRodinプラットフォーム。
^ 「B-Toolkit」。[B-Core（UK）Limited]。2004年。
^ ウェイバックマシンで2004年10月12日にアーカイブされたBツールキットの要件
^ 「B-Core（UK）Limited」。会社データレックス。
^ B-Toolkitソースコード ^ 「AtelierB.eu」。
外部リンク
B Method.com：このサイトは、証明付きの形式手法であるBメソッドに関するさまざまな作業と主題を提示するように設計されています。
Atelier B.eu：Atelier Bは、完璧であることが保証されているソフトウェアの開発を可能にするシステムエンジニアリングワークショップです。
サイトBグルノーブル
は、2008年11月1日より前にFree Online Dictionary of Computingから取得され、GFDLバージョン1.3以降の「再ライセンス」条件に基づいて組み込まれた資料に基づいています。