Problembeschreibung
Auch wenn die verschiedenen Schichten im wesentlichen
Abstraktionsebenen entsprechen, handelt es sich bei den jeweiligen
Beschreibungen immer um dasselbe zu untersuchende System. Dabei ist
die Beschreibung der genaueren Schichten um Details angereichert,
die zwar näher an die Implementierung führen, allerdings über Artefakte
oder Eigenschaften reden, die in den abstrakteren Schichten (noch) keine
Rolle spielen.
Dennoch müssen Eigenschaften, die für die abstrakten
Schichten nachgewiesen wurden, auch auf den konkreteren Schichten gelten.
Um einen solchen Nachweis zu führen, bedient man sich häufig eines
geeigneten Verfeinerungsbegriffs. Im Allgemeinen spricht man von einer
Verfeinerung, wenn alle Modelle der abstrakten Schicht auch Modelle der
konkreten Schicht sind. Sollten allerdings die unterliegenden Sprachen
nicht gleichartig sein, so ist diese Modellinklusion nicht ausreichend.
In diesem Fall ist zusätzlich eine Abbildung zu formulieren, die Modelle
der einen Sprache in Modelle der anderen Sprache überführt.
Zielsetzung/Leistungsumfang
Ausgehend von den in AP 4 analysierten
Beschreibungstechniken und deren Übertragung nach VSE wird ein Verfeinerungsbegriff
definiert. Dies schließt klassische Modelldefinitionen aber auch auf die
Bedürfnisse des SuReal-Projektes spezialisierte Modelldefinitionen ein,
die sich aus der Beobachtermodellierung ergeben.
Anhand von geeigneten Beispielen werden Verfeinerungsbeweise
durchgeführt, was wiederum in einem iterativen Prozess zu Varianten der
Beobachtermodellierung führen kann. Die spätestens für AP 6
und AP 9 notwendigen Zusammenhänge zwischen den einzelnen
Beschreibungstechniken verlangen einen Korrespondenzbegriff zwischen den
dort verwendeten verschiedenen formalen Sprachen. Auf diese Weise können
nicht nur zwischen verschiedenen Abstraktionsschichten, sondern auch
innerhalb einer Abstraktionsschicht verschiedene Beschreibungstechniken
zur Anwendung kommen, deren Zusammenhänge über die in diesem Arbeitspaket
definierten Korrespondenzen und Verfeinerungen gegeben sind und mithilfe
von VSE formal beschrieben werden.
Zwischen der Programmiersprachenebene und der Prozessorschicht
sind analoge Verfeinerungen zu betrachten. So wird in diesem Zusammenhang an
der Korrektheit von Verfeinerungen der Byte-Code-Übersetzer gearbeitet.
AP 5.1: Definitionen geeigneter Verfeinerungsbegriffe
In diesem Unterarbeitspaket werden die für die
SuReal-Methodologie geeigneten und notwendigen Verfeinerungsbegriffe definiert.
Dies beinhaltet logische Verfeinerungen, Verfeinerungen auf abstrakten Automaten,
auf Programmiersprachenebene und auf Compilerebene.
AP 5.2: Nachweise der Adäquatheit für die Verfeinerungsbegriffe
Im wesentlichen dienen Verfeinerungsbeweise dazu, zu garantieren,
dass Eigenschaften, die für eine abstrakte Ebene nachgewiesen wurden, auf den
konkreteren Ebenen erhalten bleiben. In diesem Unterarbeitspaket wird nachgewiesen,
daß die in AP 5.1 definierten Verfeinerungsbegriffe diesem Anspruch genügen.
AP 5.3: Verfeinerungen auf Byte-Code-Ebene
Auf Byte-Code-Ebene werden Verfeinerungen betrachtet, durch
die Binär-Code-Fragmente um Informationen wie Code-Zeilen und Methodennamen
angereichert werden. In diesem Arbeitspaket werden die diesbezüglichen
Korrektheitsnachweise geführt und eine Werkzeugintegration vorgenommen.
AP 5.4: Adaption auf das Verification Support Environment (VSE)
Über AP 4 wird VSE als integratives
Spezifikations- und Verifikationssystem verwendet. Über die Beobachtermodellierung
bietet VSE eine einheitliche Sicht auf die verwendeten Tools, bzw. deren Ergebnisse.
In diesem Unterarbeitspaket werden die Verfeinerungsbegriffe aus AP 5.1 und AP 5.2
auf die VSE-Spezifikationssprache übertragen, um Verfeinerungsbeweise mithilfe
von VSE durchführen zu können.
AP 5.5: Anwendung auf das Gesamtsystem
Letztlich ist anhand von Beispielanwendungen zu zeigen, daß
die in einem gegebenen beispielhaften Gesamtsystem vorgenommenen Verfeinerungen
geeignet sind, Korrektheitsaussagen für die abstrakten Ebenen auf die konkreteren
Ebenen zu übertragen. In diesem Unterarbeitspaket wird die Adaption aus AP 5.4
auf ein solches System angewendet, also ein durchgängiger VSE-Verfeinerungsbeweis
durchgeführt.
Abhängigkeiten von anderen Arbeitspaketen
Import: die zu verfeinernden Spezifikationen werden
anhand des in AP 1 entwickelten Entwurfsprozesses bestimmt.
Die in AP 2 entwickelten Spezifikationsmechanismen, die
sich in den Verifikationsproblemen des AP 3 wiederfinden,
sowie die im AP 4 analysierten Beschreibungstechniken und
Werkzeuge liefern unmittelbar Eingaben für einen zugehörigen Korrespondenznachweis,
bzw. für den Beweis, daß eine logische Verfeinerung vorliegt.
Export: über die Aussagen, die sich innerhalb einer
Schicht über Teile des zu untersuchenden Systems machen lassen, sowie über
die zugehörigen Verfeinerungsbeweise, läßt sich eine Aussage über das
Zeitverhalten des Gesamtsystems oberhalb der Prozessorebene machen
(AP 6). Letztlich wird in AP 9
anhand geeigneter Beispiele die Gesamtmethodik — und somit auch
der Teil, der von AP 5 abgedeckt wird — evaluiert.
Beteiligte Projektpartner
· DFKI (verantwortlich)
· aicas
|