In Fortführung vielfältiger Aktivitäten der letzten Jahre hat das Projekt KORSYS die Weiterentwicklung und Anwendung von Verifikationstechniken zum Ziel. Kooperiert wird auf der Seite der Technologie- und Werkzeugentwicklung mit der Technischen Universität München sowie der Zentralabteilung Forschung und Entwicklung der Siemens AG.

 

Auf der Anwenderseite finden sich die Bayerischen Motorenwerke AG (Automobilbau), dieElektroniksystem- und Logistik-GmbH (Avionik) sowie der Bereich Automatisierungstechnik der Siemens AG.

 

Anliegen und Struktur

Softwaresystemefinden bei den Anwendern für unterschiedlichste Aufgaben Verwendung. Häufig spielen dann die Programme eine sicherheitskritische Rolle, ihr korrektes Funktionieren muß unter allen Umständen gewährleistet sein. Hieraus ergibt sich die Notwendigkeit, mit Methoden zu arbeiten, die über die gewöhnlich bei der Erstellung von Software eingesetzten hinausgehen, eben formale Verifikation zu betreiben. Nun ist mit allen bekannten derartigen Techniken ein hoher Aufwand verbunden. Erst in den letzten Jahren hatten Bemühungen, die Arbeit in einem hohen Grade zu automatisieren, nennenswerte Erfolge zu verzeichnen. Es ist insbesondere das sogenannte Modelchecken, das sich in vielen Fällen bewährt hat. Es wird in verschiedenen Varianten auch bei OFFIS eingesetzt.

Um eine geforderte Eigenschaft (Spezifikation)eines Systems nachzuweisen, wird beim Modelchecken nicht versucht, einen Beweis zu erstellen. Statt dessen erstellt man einen Automaten, dessen Abläufe denen des Systems entsprechen. Die Eigenschaft muß in eine Formeldarstellung gebracht werden. Dann berechnet man nach einem speziellen Algorithmus, ob es einen Ablauf gibt, der die Formel verletzt. In der Sprache der Logik ausgedrückt, überprüft man also, ob das System Modell der Formel ist. Daher kommt der Name Modelchecken. Wichtig ist, daß es sich um ein automatisches Verfahren handelt, liegen erst einmal der Automat und die Formel vor.

 

Hier liegen nun in der Praxis dieProbleme. Man muß eine Übersetzung von der Systembeschreibungssprache (Programmiersprache) in die Automatenrepräsentation vornehmen können, die resultierenden Automaten müssen eine handhabbare Größe behalten, und die Spezifikationen müssen formalisiert werden. Die Erfahrung hat gelehrt, daß diese Anforderungen bei verschiedenen Anwendungsgebieten in unterschiedlichem Maße zu Schwierigkeiten führen. In der Regel sind zur Überwindung der Schwierigkeiten zum Modelchecken komplementäre Techniken nötig.

 

Der Ansatzpunkt von KORSYS ist es, die Problematik nun in den Ausprägungen zu studieren, wie sie sich bei den Anwendern im Projekt ergibt. Jeder der Anwender präsentiert ein typisches Problem aus seinem Gebiet. Bei BMW ist es die Steuerung der Karosserieelektronik (z.B. Zentralverriegelung), von der ESG ist es die Überwachung des Flugzeugzustandes, die Siemens Automatisierungstechnik betrachtet die Kontrolle von Fertigungszellen. Diese Fallstudien werden zur Grundlage für die Entwicklung und Gestaltung adäquater, ergänzender Techniken.

 

Technische ArbeitszieleWichtiger Punkt im Ansatz von OFFIS ist es, dem Systementwickler zu ermöglichen,vorwiegend graphische Beschreibungsmittel sowohl für die Systeme als auch für Spezifikationen zu verwenden. Graphikorientierte Verfahren sind dem Systementwickler leichter zugänglich. Indem man so die Akzeptanz der Verfahren erhöht, vereinfacht man die Einführung formaler Methoden in den industriellen Entwicklungsprozeß.

 

Systembeschreibungen können mit Hilfe von Statemate erstellt werden.Bei Statemate handelt es sich um ein kommerzielles Werkzeug, das durch ein ausgefeiltes Hierarchiekonzept die übersichtliche graphische Definition selbst komplexer Systeme erlaubt. Zur Codeerzeugung existieren Übersetzer in Standardsprachen.

 

Spezifikationen werden in Form von sogenannten symbolischen Zeitdiagrammengeschrieben. Die Zeitdiagramme sind in Oldenburg entwickelt worden und spielten bereits im Projekt FORMAT eine wichtige Rolle. Sie ermöglichen eine anschauliche Darstellung von Verhaltensbeschreibungen. Ihre Bedeutung ist durch eine Übersetzung in eine Temporallogik, die sich mit Modelcheckern behandeln läßt, gegeben. Jedoch sind die Zeitdiagramme oft wesentlich kompakter als entsprechende Formeln.

 

Innerhalb von KORSYS wird zunächst eine Übersetzung von StateMatein Automaten realisiert. Mit einer Anpassung der die Zeitdiagramme betreffenden Werkzeuge macht dies die Basistechnologie des Modelcheckens in der graphischen Entwicklungsschiene anwendbar, und es können in den Fallstudien erste praktische Ergebnisse gewonnen werden. Für die Beispiele der Anwender reicht diese Basistechnologie jedoch nicht immer aus, die Automatenrepräsentationen kompletter Systeme sind häufig zu groß. Weitergehende Arbeiten werden dieses Problem der Skalierbarkeit der Verifikationsmethoden angehen.

 

Dabei werden zweierlei ergänzende Techniken zu realisieren sein.Es handelt sich dabei um Abstraktion und Dekomposition.

 

Abstraktion nutzt aus, daß häufig von vielen Aspekten einesSystems abgesehen werden kann, wenn es um die Erfüllung eines Teils der Spezifikation geht. So kann man Systembeschreibungen - und damit ihre Automatenrepräsentationen - in ihrer Größe stark reduzieren, wenn es um die Überprüfung nur jeweils einer Eigenschaft geht. Beispielsweise ist es nicht notwendig, Datenwerte konkret zu betrachten, wenn es darum geht, Fehler bei der Einhaltung eines vorgeschriebenen Protokolls auszuschließen. Eine systematische Transformation der Systembeschreibung führt dann auf ein stark vereinfachtes Verifikationsproblem. Andere Abstraktionen vereinfachen etwa die interne Kommunikationsstruktur zwischen Systemkomponenten, mit ebenfalls drastischen Reduktionen der Problemkomplexität. Implementiert man Abstraktionen, benötigt man in der Regel Hilfsprogramme, die Transformationen durchführen oder Nebenbedingungen prüfen.

 

Unter Dekomposition versteht man das Aufteilen einer Anforderung aufdie einzelnen Komponenten eines Systems, die in unterschiedlichem Maße an der Erfüllung der Anforderung beteiligt sind. Das heißt, man muß Spezifikationen der Komponenten eines Systems finden, so daß sie zusammengefaßt die globale Spezifikation ergeben. Anders als bei Abstraktionen orientiert man sich hier also an der algebraischen Struktur eines Systems, wie sie vom Entwickler vorgegeben ist. Ðbrig bleiben dann die - kleineren - Verifikationsprobleme der Komponenten sowie die Ðberprüfung der Frage, ob die Dekomposition selber korrekt ist. In dem bei OFFIS verfolgten Ansatz sind die Komponentenspezifikationen natürlich wiederum Zeitdiagramme. Festzustellen, ob die Dekomposition korrekt ist, läßt sich mitunter - ähnlich wie das Modelchecken - automatisch erledigen. Für den Fall jedoch, daß der Schritt aus Komplexitätsgründen scheitert, wird ein graphischer Beweiskalkül auf der Ebene der Zeitdiagramme entwickelt.

 

Für alle diese Schritte wird eine Werkzeugunterstützung benötigt. Teils lassen sich die bereits im FORMAT-Projekt entwickelten Programme modifizieren oder weiterbenutzen, teils sind es Neuentwicklungen. Angestrebt wird die Erstellung eines integrierten Werkzeugsystems, das zum Projektende als Prototyp vorliegt und an Fallstudien, die auf den von den Anwendern im Projekt bereitgestellten Beispielproblemen beruhen, getestet ist.

 

Einordnung des Beitrags von OFFIS

Insgesamt gesehen ist das Ziel der Aktivitäten von OFFIS im Rahmenvon KORSYS, bekannte, zum Teil bei OFFIS entwickelte Verifikationstechniken den Bedürfnissen der Praxis anzupassen. Die Probleme, die in früherer Zeit den Einsatz formaler Methoden erschwert haben, werden konsequent angegangen:

 

Ein hoher Automatisierungsgrad entlastet den Entwickler von Detailarbeit. Die Verwendung graphischer Formalismen zur System- und Anforderungsbeschreibung verbessern Handhabbarkeit und Akzeptanz. Und ein Instrumentarium verschiedener Techniken zielt auf Skalierbarkeit, die Beherrschbarkeit auch größerer Aufgaben, ab.