 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | ||||||||||||||||||||||||||||||||||||||||||||||
| Wissensbrowser starten | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||
|  | |  | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Verfahren |
|
B als formale Spezifikationssprache |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung | |||||||||
| |||||||||
| B wurde von J.R. Abrial Mitte der 80er Jahre im Oxford University Computing Laboratory mit Finanzierung der BP (British Petrol) entwickelt. Die Spezifikationssprache Z wurde als Ausgangspunkt verwendet.
Die B-Methode verwendet mathematische Mittel zur Beschreibung von Spezifikationen. Prädikatenlogik, Mengen, Listen und Funktionen werden benutzt. Notationsanleihen wurden bei Z gemacht. (J.R. Abrial hat bei Z mitgearbeitet). Systeme werden als Menge von abstrakten Maschinen modelliert, die zueinander in Beziehung stehen bzw. voneinander abhängen. Die abstrakten Maschinen sind die „Module“ von B, vergleichbar mit Klassen in objektorientierten Sprachen ohne Vererbung. Zur Beschreibung der abstrakten Maschinen wird die Abstract Machine Notation (AMN) verwendet. Eine abstrakte Maschine hält sowohl Zustand wie auch Operationen auf diesem Zustand, sie wird mit der AMN beschrieben. Abstrakte Maschinen können die Verfeinerung einer anderen abstrakten Maschine sein. Eine Spezifikation kann damit über eine Folge abstrakter Maschinen bis hin zum Code konkretisiert werden. Werkzeuge können die Korrektheit der Daten- und algorithmischen Verfeinerung prüfen. Eines der bekanntesten Beispiele für die erfolgreiche Verwendung formaler Methoden wurde mit B erstellt. Die Firma Mantra Transport International (jetzt Siemens) hat die Software für eine unbemannte Linie der Pariser Metro im Meteor Projekt entwickelt. Werkzeugunterstützung ist von zwei Herstellern vorhanden. Werkzeugkästen sind Atilier-B von Digilog oder B-Tool und B-Toolkit von B-Core . | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
 | Übergeordnet | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| ||||
| B als formale Spezifikationssprache | ||||
| ||||
| ||||
| ||||
| ||||
| Erfahrungen | | ||
| ||||
|
| | ||
| ||||
| Literaturhinweise | | ||
| ||||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
