AP 5: Verifikation der Verfeinerungsschritte

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