Kombinierte formale Methoden -- Spezifikation und Verifikation

zur Spezifikation von Software- und Hardwaresystemen. Formale
Spezifikationssprachen sind meist spezifisch auf die
Modellierung von bestimmten Aspekten eines Systems zugeschnitten
(z.B. Modellierung der Use Cases des Systems oder der Daten). Im
Gegensatz
dazu zeichnen sich komplexe Softwaresysteme dadurch aus, dass sie ganz
unterschiedlichen Arten von Anforderungen (wie etwa bzgl. Daten,
dynamischem
Verhalten, Zeit oder Verteiltheit) genügen müssen. Die Notwendigkeit
zur
Beschreibung unterschiedlichster Sichten auf ein System führte zur
Entwicklung
von sogenannten kombinierten formalen Methoden. Diese verbinden eine
Reihe
wohl untersuchter Einzelformalismen zu einer neuen Sprache, mit der
unterschiedliche Aspekte in der Systembeschreibung abgedeckt werden
können.
Durch die Einführung von kombinierten Methoden ergeben sich allerdings
auch
eine Reihe von neuen Herausforderungen. Der wesentliche Vorteil bei der
Benutzung von formalen Methoden im Systementwurf liegt in der präzisen
Festlegung der Funktionalität: jede Spezifikation besitzt eine formale
Semantik. Die Semantik ermöglicht den Nachweis der Korrektheit von
Spezifikationen gegenüber Anforderungen. Diese Möglichkeit zur
automatischen
Verifikation von Systementwürfen ist ausschlaggebend für das Interesse
der
Industrie an formalen Methoden. Die gleichen Vorteile muss auch eine
Kombination existierender Sprachen bieten.

In dem Vortrag werden verschiedene Problemstellungen bei der
Kombination formaler Methoden diskutiert, und an Hand einer ausgewählten
Kombination Lösungen vorgestellt. Ein Schwerpunkt wird auf der
Verifikation
von Spezifikationen objekt-orientierter Kombinationen liegen, bei der
durch
Vererbung entstandene Beziehungen zwischen Klassen in der Verifikation
ausgenutzt werden können.