B-Methode - B-Method

Die B-Methode ist eine Methode der Softwareentwicklung basierend auf B , einer werkzeuggestützten formalen Methode basierend auf einer abstrakten Maschinennotation , die bei der Entwicklung von Computersoftware verwendet wird . Es wurde ursprünglich in den 1980er Jahren von Jean-Raymond Abrial in Frankreich und Großbritannien entwickelt . B ist mit der Z-Notation (ebenfalls von Abrial) verwandt und unterstützt die Entwicklung von Programmiersprachencode aus Spezifikationen. B wurde in wichtigen sicherheitskritischen Systemanwendungen in Europa verwendet (wie die automatischen Pariser Métro-Linien 14 und 1 und die Ariane 5- Rakete). Es verfügt über eine robuste, kommerziell erhältliche Werkzeugunterstützung für Spezifikation , Design , Proof und Codegenerierung .

Im Vergleich zu Z ist B etwas niedriger und konzentrierter auf die Verfeinerung des Codes und nicht nur auf die formale Spezifikation – daher ist es einfacher, eine in B geschriebene Spezifikation korrekt zu implementieren als eine in Z. Insbesondere gibt es eine gute Werkzeugunterstützung für diese. In Spezifikation, Design und Programmierung wird dieselbe Sprache verwendet. Zu den Mechanismen gehören Kapselung und Datenlokalität.

Anschließend wurde eine weitere formale Methode namens Event-B entwickelt. Ereignis-B gilt als eine Weiterentwicklung von B (auch bekannt als klassisches B). Es ist eine einfachere Notation, die einfacher zu erlernen und zu verwenden ist. Es wird mit Werkzeugunterstützung in Form des Rodin-Werkzeugs geliefert .

Die Hauptkomponenten

Die B-Notation hängt von der Mengenlehre und der Logik erster Ordnung ab, um verschiedene Softwareversionen zu spezifizieren, die den gesamten Zyklus der Projektentwicklung abdecken.

Abstrakte Maschine

In der ersten und abstraktesten Version, die sich Abstract Machine nennt , sollte der Designer das Ziel des Designs spezifizieren.

Raffinesse

  • Dann kann er in einem Verfeinerungsschritt die Spezifikation ergänzen, um das Ziel zu verdeutlichen oder die abstrakte Maschine konkreter zu machen, indem er Details zu Datenstrukturen und Algorithmen hinzufügt, die definieren, wie das Ziel erreicht wird.
  • Die neue Version mit dem Namen Refinement soll sich als kohärent erweisen und alle Eigenschaften der abstrakten Maschine beinhalten.
  • Der Designer kann B-Bibliotheken verwenden, um Datenstrukturen zu modellieren oder vorhandene Komponenten einzubinden oder zu importieren.

Implementierung

  • Die Verfeinerung wird fortgesetzt, bis eine deterministische Version erreicht ist: die Implementierung .
  • Bei allen Entwicklungsschritten wird dieselbe Notation verwendet und die letzte Version kann zur Kompilierung in eine Programmiersprache übersetzt werden .

Software

B-Toolkit

Das B-Toolkit , entwickelt von Ib Holm Sørensen et al. , ist eine Sammlung von Programmierwerkzeugen, die entwickelt wurden, um die Verwendung des B-Tools, eines mengentheoretischen mathematischen Interpreters, für die Zwecke einer formalen Softwareentwicklungsmethodik, die als B-Methode bekannt ist, zu unterstützen.

Das Toolkit verwendet eine benutzerdefinierte X Window Motif- Schnittstelle für die GUI-Verwaltung und läuft hauptsächlich auf den Betriebssystemen Linux , Mac OS X und Solaris . Es wurde von der britischen Firma B-Core (UK) Limited entwickelt.

Der B-Toolkit-Quellcode ist jetzt verfügbar.

Atelier B

Atelier B wurde von ClearSy entwickelt und ist ein industrielles Werkzeug, das den operativen Einsatz der B-Methode zur Entwicklung fehlerfreier, bewährter Software (formale Software) ermöglicht. Es stehen zwei Versionen zur Verfügung: Community Edition für jedermann ohne Einschränkung verfügbar, Maintenance Edition nur für Wartungsvertragsinhaber.

Es dient der Entwicklung von Sicherheitsautomatismen für die verschiedenen weltweit installierten U-Bahnen von Alstom und Siemens sowie für die Common Criteria-Zertifizierung und die Entwicklung von Systemmodellen von ATMEL und STMicroelectronics .

Bücher

  • Das B-Book: Programme Bedeutungen zuordnen , Jean-Raymond Abrial , Cambridge University Press , 1996. ISBN  0-521-49619-5 .
  • The B-Method: An Introduction , Steve Schneider, Palgrave Macmillan , Cornerstones of Computing series, 2001. ISBN  0-333-79284-X .
  • Software Engineering mit B , John Wordsworth, Addison Wesley Longman , 1996. ISBN  0-201-40356-0 .
  • The B Language and Method: A Guide to Practical Formal Development , Kevin Lano , Springer-Verlag , FACIT-Reihe, 1996. ISBN  3-540-76033-4 .
  • Spezifikation in B: An Introduction using the B Toolkit , Kevin Lano , World Scientific Publishing Company , Imperial College Press , 1996. ISBN  1-86094-008-0 .
  • Modeling in Event-B: System and Software Engineering , Jean-Raymond Abrial , Cambridge University Press , 2010. ISBN  978-0-521-89556-9 .

Konferenzen

  • Konferenz Z2B, Nantes, Frankreich, Okt. 10-12 1995
  • Erste B-Konferenz, Nantes, Frankreich, nov. 25-27 1996
  • Zweite B-Konferenz, Montpellier, Frankreich, ap. 22-24 1998,
  • ZB'2000, York, Großbritannien, 28. August, 2. September 2000,
  • ZB'2002, Grenoble, Frankreich, 23.-25. Januar 2002,
  • ZB'2003, Turku, Finnland, 4.-6. Juni 2003
  • ZB'05, Guildford, Großbritannien, 2005
  • B'2007, Besançon, Frankreich, 2007
  • B, von der Forschung zur Lehre, Nantes, Frankreich, 16. Juni 2008
  • B, von der Forschung zur Lehre, Nantes, Frankreich, 8. Juni 2009
  • B, von der Forschung zur Lehre, Nantes, Frankreich, 7. Juni 2010
  • ABZ-Konferenz: ABZ 2008, British Computer Society, London, UK, 16.–18. September 2008
  • ABZ-Konferenz: ABZ 2010, Oxford, Québec, Kanada, 23.–25. Februar 2010
  • ABZ-Konferenz: ABZ 2012, Pisa, Italien, 18.–22. Juni 2012
  • ABZ-Konferenz: ABZ 2014, Toulouse, Frankreich, 2.–6. Juni 2014
  • ABZ-Konferenz: ABZ 2016, Linz, Österreich, 23.–27. Mai 2016

Siehe auch

  • APCB (Association de Pilotage des Conférences B)
  • BHDL

Verweise

Externe Links

  • B Method.com : Diese Seite soll verschiedene Arbeiten und Themen rund um die B-Methode präsentieren, eine formale Methode mit Beweis with
  • Atelier B.eu : Atelier B ist eine Werkstatt für Systemtechnik, die es ermöglicht, Software zu entwickeln, die garantiert fehlerfrei ist
  • Standort B Grenoble

Dieser Artikel basiert auf Material, das vor dem 1. November 2008 aus dem Free Online Dictionary of Computing entnommen wurde und unter die "Relicensing"-Bedingungen der GFDL , Version 1.3 oder höher, aufgenommen wurde.