fOOSE- Eine integrierte formale Softwareentwicklungsmethode

Abstract

Die Methode "fOOSE" (formal Object-Oriented Software Engineering) exemplifiziert eine auf der "Unified Modeling Language" (UML) basierende, integrierte formale Softwareentwicklungsmethode: Jacobsons "Object-Oriented Software Engineering"-Methode (OOSE) wird um diagrammgestützte, formale Spezifikationen, Beweisverpflichtungen und Verfeinerungen erweitert. Die diagrammatischen UML- Modelle werden um Anmerkungen, etwa Invarianten, in einer formalen, algebraischen Sprache optional ergänzt. Aus der Semantik der Diagramme und der Anmerkungen kann halbautomatisch eine ablauffähige Spezifikation in der objektorientierten, algebraischen Spezifikationssprache Maude abgeleitet werden: Ein automatisch erstelltes Spezifikationsgerüst muß vom Benutzer unter Ausnutzung der formalen Annotationen vervollständigt werden. Diese Spezifikationen erlauben insbesondere die Verifikation von Verfeinerungsbeziehungen zwischen Modellen. Schließlich bildet die semi-automatisch erstellte Spezifikation aus einem gegebenen, annotierten Softwaremodell auch die Grundlage für eine korrekte Implementierung dieses Modells in der objektorientierten, nebenläufigen Programmiersprache Java.