Campus Event Calendar
Event Entry
What and Who
Automatische Verifikationsunterstützung für Operationsverfeinerung
Dr. Bettina Buth
Universität Bremen
DFKI-Kolloquium
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, RG1, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Monday, 23 October 95
16:00
60 Minutes
43.1 - DFKI
0.25
Saarbrücken
Abstract
Spezifikation der Datenbereiche und Operationen wird durch schrittweise
Verfeinerung (data reification, operation refinement) eine konkrete
Spezifikation entwickelt. Datenverfeinerung fuer VDM-Spezifikation wurde in
den letzten Jahren ausfuehrlich untersucht; hingegen gibt es kaum Ansaetze
fur Operationsverfeinerung.
Ein spezieller Aspekt der Operationsverfeinerung fur VDM-artige
Spezifikationen ist die Verfeinerung von impliziten Spezifikationen zu
expliziten. In diesem Rahmen sind implizite Spezifikationen Paare von
Praedikaten, die Vor- und Nachbedingungen von Operationen beschreiben, also
moegliche Ergebnisse und den Effekt auf den globalen Zustand. Explizite
Spezifikationen sind Operationsdeklarationen, die herkoemmliche imperative
Sprachkonstrukte verwenden. Fur realistische Anwendungen sind haeufig
Systeme wechselseitig rekursiver Operations- und Funktionsdefinitionen zu
betrachten.
Im Vortrag wird ein werkzeuggestutzter Ansatz fur den Nachweis der
partiellen Korrektheit von Mengen von Operationsspezifikationen bzgl. der
zugehoerigen impliziten Spezifikationen vorgestellt. Der Ansatz ist modular
und erlaubt es, die einzelnen Spezifikationen unabhaengig voneinander zu
beweisen, wobei nur die impliziten Spezifikationen als Zusatzinformation
zur Verfuegung stehen. Das Beweisunterstuetzungssystem PAMELA ist speziell
fuer die im Rahmen der Operationsverfeinerung anfallende Verifikation
entwickelt worden. Die Herleitung der Beweisverpflichtungen, die die
Korrektheit des Gesamtsystems gewaehrleisten, basiert auf der symbolischen
Auswertung der expliziten Spezifikationen.
Das System berechnet die notwendigen Beweisverpflichtungen fur eine
gegebene Spezifikation durch Verwendung des sogenannten Splittens. Dabei
werden fur jeden Pfad durch den Rumpf einer expliziten Spezifikation die
staerkste Nachbedingung und das symbolische Resultat berechnet, die zur
Bestimmung von Voraussetzung und Behauptung des Teilbeweises verwendet
werden. Darueberhinaus werden - basierend auf Termersetzungtechniken - die
einzelnen Teilbeweise vom System automatisch durchgefuehrt. Die Grundlage
hierfur sind Regeln, die vom Benutzer in Form von bedingten oder
unbedingten Ersetzungsregeln oder als Deduktionsregeln angegeben werden.
Die Regelanwendung wird von einer ebenfalls benutzerdefinierten Strategie
gesteuert.
Verfeinerung (data reification, operation refinement) eine konkrete
Spezifikation entwickelt. Datenverfeinerung fuer VDM-Spezifikation wurde in
den letzten Jahren ausfuehrlich untersucht; hingegen gibt es kaum Ansaetze
fur Operationsverfeinerung.
Ein spezieller Aspekt der Operationsverfeinerung fur VDM-artige
Spezifikationen ist die Verfeinerung von impliziten Spezifikationen zu
expliziten. In diesem Rahmen sind implizite Spezifikationen Paare von
Praedikaten, die Vor- und Nachbedingungen von Operationen beschreiben, also
moegliche Ergebnisse und den Effekt auf den globalen Zustand. Explizite
Spezifikationen sind Operationsdeklarationen, die herkoemmliche imperative
Sprachkonstrukte verwenden. Fur realistische Anwendungen sind haeufig
Systeme wechselseitig rekursiver Operations- und Funktionsdefinitionen zu
betrachten.
Im Vortrag wird ein werkzeuggestutzter Ansatz fur den Nachweis der
partiellen Korrektheit von Mengen von Operationsspezifikationen bzgl. der
zugehoerigen impliziten Spezifikationen vorgestellt. Der Ansatz ist modular
und erlaubt es, die einzelnen Spezifikationen unabhaengig voneinander zu
beweisen, wobei nur die impliziten Spezifikationen als Zusatzinformation
zur Verfuegung stehen. Das Beweisunterstuetzungssystem PAMELA ist speziell
fuer die im Rahmen der Operationsverfeinerung anfallende Verifikation
entwickelt worden. Die Herleitung der Beweisverpflichtungen, die die
Korrektheit des Gesamtsystems gewaehrleisten, basiert auf der symbolischen
Auswertung der expliziten Spezifikationen.
Das System berechnet die notwendigen Beweisverpflichtungen fur eine
gegebene Spezifikation durch Verwendung des sogenannten Splittens. Dabei
werden fur jeden Pfad durch den Rumpf einer expliziten Spezifikation die
staerkste Nachbedingung und das symbolische Resultat berechnet, die zur
Bestimmung von Voraussetzung und Behauptung des Teilbeweises verwendet
werden. Darueberhinaus werden - basierend auf Termersetzungtechniken - die
einzelnen Teilbeweise vom System automatisch durchgefuehrt. Die Grundlage
hierfur sind Regeln, die vom Benutzer in Form von bedingten oder
unbedingten Ersetzungsregeln oder als Deduktionsregeln angegeben werden.
Die Regelanwendung wird von einer ebenfalls benutzerdefinierten Strategie
gesteuert.
Contact
Dr. Werner Stephan
--email hidden
passcode not visible
logged in users only
Tags, Category, Keywords and additional notes
verification