AP 4: Analyse der Beschreibungstechniken auf den verschiedenen Schichten

Problembeschreibung

In jeder der zu untersuchenden Schichten werden mithilfe einer formalen Sprache Modellbildungen und Anforderungen an diese Modelle beschrieben. Grundsätzlich sollen — je nach Abstraktionsgrad der zu beschreibenden Schicht — die sicherheitsrelevanten Eigenschaften schon während des Entwicklungsprozesses identifiziert, formal repräsentiert und mit entsprechenden Werkzeugen analysiert werden.

Für die Zwischenschichten spielen mehr und mehr vernetzte Mehrprozessor-Architekturen sowie Betriebssysteme und Busprotokolle eine Rolle, sodaß Beschreibungstechniken zu entwickeln sind, die das Zeitverhalten und seine Robustheit (von sequentiellen Programmen) als Folge der Systemintegration behandeln.

Letztlich sind die prozessornahen Schichten zu beschreiben, auf denen das Zeitverhalten über eine Worst-Case-Execution-Time-Analyse bestimmt wird.

Zielsetzung/Leistungsumfang

Schnittstellen zwischen diesen Sprachen und Tools werden definiert, damit Ergebnisse auf der einen Schicht von der nächsten Schicht übernommen werden können. Für diese Schnittstellen ist zu berücksichtigen, daß sich verschiedene Beschreibungssprachen nicht nur syntaktisch und semantisch, sondern eventuell auch pragmatisch unterscheiden. So kann es vorkommen, daß innerhalb einer Schicht — je nach gewünschter, erwarteter oder befürchteter Eigenschaft — verschiedene Beschreibungstechniken und Werkzeuge zur Anwendung kommen.

In abstrakteren Schichten bieten sich mit Hinblick auf Realzeiteigenschaften Temporallogiken wie LTL, CTL und ICTL an, sowie Werkzeuge, die mit diesen Eigenschaftssprachen umzugehen wissen. Dazu zählen beispielsweise das Verification Support Environment (VSE), HyTech, Uppaal und Kronos, sowie ein Symbolic-Model-Checker, der gegenwärtig am DFKI entwickelt und implementiert wird und der es erlaubt, mit abstrakten Datentypen zu arbeiten.

Als integratives Werkzeug für alle diese Techniken wird das Verification Support Environment (VSE) des DFKI Verwendung finden, welches temporallogische Spezifikationen, abstrakte Datentypen und dynamische Logik in sich vereinigt. Die Erfahrungen des DFKI im Bereich der Observer-Modellierung (in VSE) führen zu einer Vereinheitlichung der diversen Beschreibungstechniken und ihrer Ergebnisse. Dazu wird für jede dieser Techniken untersucht, welche Ausdrucksstärke die darunter liegende formale Sprache hat und wie die verschiedenen formalen Sprachen in Beziehung gesetzt werden können. Somit wird gewährleistet, daß Ergebnisse möglichst vieler Tools von anderen Tools, insbesondere VSE, importiert werden können.

AP 4.1: Identifikation der Beschreibungstechniken

Abstrakte Schichten werden im wesentlichen mithilfe von Logikformalismen beschrieben werden. Je näher die zu beschreibende Schicht der Programmebene liegt, desto mehr werden Automaten, UML, abstrakte Datentypen und dynamische Logik und auch Programmiersprachen-Analysewerkzeuge wie beispielsweise Java-Annotationen zur Datenflußanalyse zur Anwendung kommen. Die notwendigen und hilfreichen Beschreibungstechniken werden in diesem Unterarbeitspaket identifiziert und anwendungsspezifisch ausgerichtet.

AP 4.2: Definition der Schnittstellen

In diesem Unterarbeitspaket werden die Schnittstellen zwischen den in AP 4.1 identifizierten Beschreibungstechniken definiert. Dies beinhaltet eine Analyse der Werkzeuge und der Beschreibungssprachen.

AP 4.3: Beschreibung der Sichten über Beobachtermodelle

Beobachtermodelle dienen einer einheitlichen und konsistenten Sicht auf spezifizierte Anforderungen. Ihre Definition liefert eine horizontale Strukturierung der diversen Schichten. In diesem Arbeitspaket werden Beobachtermodelle beschrieben, mit deren Hilfe die für die aktuelle Problemstellung notwendigen Aspekte für die verschiedenen Komponenten isoliert betrachtet werden können.

AP 4.4: Interoperabilität der verschiedenen Beschreibungstechniken

Alle in SuReal zur Verwendung kommenden Beschreibungstechniken sind gewissen Abstraktionsschichten zugeordnet. Sie agieren untereinander entweder vertikal, d.h. über einen Verfeinerungsbegriff (s. AP 5) oder horizontal, d.h. in der gleichen Schicht. In diesem Unterarbeitspaket wird mithilfe der Beobachtermodelle aus AP 4.3 die Austauschbarkeit der Ergebnisse verschiedener Werkzeuge möglich gemacht.

Abhängigkeiten von anderen Arbeitspaketen

Import: in AP 1 werden die beteiligten Artefakte identifiziert, die innerhalb des Projektes entstehen bzw. anfallen. Diese schränken die zu untersuchenden Beschreibungstechniken ein. In AP 2 werden geeignete Spezifikationsmechanismen entwickelt, die in formaler Sprache bzw. Werkzeugen unmittelbar Gegenstand der Analyse von Techniken in den verschiedenen Abstraktionsschichten sind. Der Schwerpunkt von AP 3 liegt im Vergleich von Systemmodellen mit Analysewerkzeugen, ohne allerdings die verschiedenen Abstraktionsschichten zu berücksichtigen. Dieser Vergleich ist auf die diversen Schichten zu projizieren.

Export: die in AP 4 analysierten Beschreibungstechniken dienen zur Modellierung der verschiedenen Abstraktionsschichten. Diese wiederum werden in AP 5 in Beziehung gesetzt (Verfeinerungsbegriff). Das in AP 6 untersuchte Zeitverhalten des Gesamtsystems orientiert sich an der Systemintegration und den in AP 4 analysierten Techniken. Letztlich werden in AP 9 anhand von geeigneten Beispielen alle analysierten und verwendeten Techniken und Werkzeuge evaluiert.

Beteiligte Projektpartner

• DFKI (verantwortlich)
• aicas
• ScopeSET