SACRES ist ein durch die Europäische Union gefördertes Projekt, das von einem Konsortium bestehend aus den Firmen SIEMENS, British Aerospace (Großbritannien), i-Logix (Großbritannien), SNECMA (Frankreich), SNI, TNI (Frankreich) und den Forschungsinstituten OFFIS, INRIA (Frankreich) und dem Weizmann Institut (Israel) durchgeführt wird.

Der Einsatz formaler Methoden in der Systementwicklung gewinnt zunehmend an industrieller Relevanz. Die bereits in anderen Forschungsprojekten, insbesondere dem FORMAT Projekt, entwickelten leistungsfähigen Kerntechnologien zur Spezifikation und Verifikation sollen in diesem Projekt in den Entwurfsprozeß für sicherheitskritische Systeme aus den Bereichen Avioniks und Fertigungstechnik integriert und erweitert werden. Außerdem werden in SACRES die Kerntechnologien um Methoden zur Behandlung von Realzeiteigenschaften erweitert. Ein wesentlicher Aspekt liegt hierbei in der Integration der Verifikationstechniken in industriell eingesetzte Entwicklungswerkzeuge.

 

Einstieg und Zielsetzung

SACRES bringt konkrete Werkzeuge sowohl für die Verifikationals auch für die Codegenerierung von Embedded Systems hervor, die in die Entwicklungsverfahren der industriellen Partnern integriert sind. Gleichzeitig wird die Anwendbarkeit und Akzeptanz der SACRES Werkzeuge sichergestellt, durch deren Einsatz für industrielle Beispiele und Evaluierung bei industriellen Partnern.

Über diese Integration hinaus erfolgt eine Anpassung an die Anwendungsdomäne durch gezielte Optimierung der eingesetzten Verifikationstechniken sowie der Bereitstellung von anwendungsspezifischen Spezifikationswerkzeugen.

 

SACRES basiert auf den Sprachen StateCharts und Signal sowie deren werkzeugmäßige Ausprägung in STATEMATE und Sildex/Grafcet. Eine besondere Herausforderung im SACRES Projekt liegt in der, aus Anwendersicht geforderten, Mischung von Spezifikationsstilen. Während STATEMATE besonders für kontrolldominierte Applikationen geeignet ist, lassen sich Datenflußgraphen prägnant in SIGNAL beschreiben. Typische Embedded Control Applikationen beinhalten beide Elemente. Ziel des SACRES-Projektes ist es, sowohl automatische Codegenerierung wie auch Verifikation solcher gemischter Entwürfe zu ermöglichen.

 

Anforderungen an das spezifizierte Embedded System können mit Hilfe von, schon im FORMAT Projekt durch OFFIS entwickelten, Symbolischen Zeitdiagrammen formuliert werden. Durch die Semantik der Zeitdiagramme in Temporaler Logik erfolgte eine Kopplung dieser, auf die Bedürfnisse des Anwenders zugeschnittenen, Sprache für Anforderungsdefinitionen und verschiedenen Werkzeugen zur formalen Verifikation eines Systems. Diese Vorgehensweise entbindet den Benutzer von der Verwendung der (schwer verständlichen) Temporalen Logik als Anforderungssprache und erhöht dadurch die Akzeptanz für die Verwendung formaler Verifikation.

 

Durch den Einsatz einer System Specification Language, kurz SSL, können in SACRES gemischte StateCharts/Signal Spezifikationen behandelt werden. SSL wurde durch OFFIS für das SACRES Projekt entwickelt. Es erlaubt insbesondere eine Strukturbeschreibung auf der Basis von Komponenten die lediglich durch ihr Interface festgelegt sind und deren Verhalten, zu einem späteren Zeitpunkt, durch die Bindung an eine Verhaltensbeschreibung in StateCharts oder Signal festgelegt werden kann.

 

OFFIS ist in SACRES maßgeblich an der semantischen Fundierung der zum Einsatz kommenden Sprachen beteiligt. Weiterhin besteht eine Beteiligung an der Bereitstellung der folgenden Werkzeuge für die Sprachen StateCharts und Signal. Ein Model Checker, der in der Lage ist, Realzeitanforderungen an das Eingabe/Ausgabe Verhalten eines Systems zu überprüfen, die als Temporal Logische Formeln formuliert sind. Dies geschieht gegenüber einer Realisierung des Systems durch eine Beschreibung in StateCharts oder Signal.

 

Ein Tautologie Checker, der die Allgemeingültigkeit eines Zeitdiagramms oder einer Temporal Logischen Formel überprüfen kann. Dieser kann insbes. dazu verwendet werden die Gültigkeit einer globalen Anforderung eines zusammengesetzten Systems aus der Gültigkeit von Anforderungen der Teilkomponenten herzuleiten.

 

Ein Theorembeweiser, in dem Temporale Logik und SSL Datentypen eingebettet wurden, um insbesondere Eigenschaften zusammengesetzter Systeme aus den Eigenschaften der Teilsysteme formal herzuleiten.

 

Transformatoren, die für Anforderungsspezifikationen in Zeitdiagrammen und Beschreibungen in StateCharts oder Signal interne Repräsentationen für die Weiterverarbeitung durch die Verifikationswerkzeuge bereitstellen. Dabei wird einem Zeitdiagramm eine Temporal Logische Formel zugeordnet. Sowohl StateCharts als auch Signal Beschreibungen werden in Modelle als zustandsendliche Graphen (symbolische Transitionssysteme) überführt. Die gewählte Darstellung dieser Graphen als Binary Decision Diagram ist besonders kompakt und erlaubt insbesondere ein effizientes Real-Time Model Checking.

 

Methodologie von SACRES

Die Methodologie von SACRES kann in dem folgenden, starkvereinfachten, Entwicklungsszenario zusammengefaßt werden:

Die informelle Anforderungsspezifikation des zu entwickelnden Embedded System wird durch die Formulierung in Zeitdiagrammen in eine formale Anforderungsspezifikation überführt. Eine abstrakte Implementierung des Systems wird als Strukturbeschreibung in SSL gegeben, deren Teilkomponenten wiederum an Strukturkomponenten oder an Verhaltensbeschreibungen in StateCharts oder Signal gebunden sind. Für die Teilkomponenten werden Anforderungsspezifikationen mit Zeitdiagrammen erstellt, die genügend Aspekte der Teilsysteme darstellen, um mit dem Theorembeweiser oder dem Tautologie Checker daraus die Anforderungsspezifikation des globalen Systems abzuleiten. Die Konsistenz der an Verhaltensbeschreibungen gebundenen Komponenten kann durch Model Checking verifiziert werden. Dabei stellt eine Partitionierung des Systems in genügend kleine Teilkomponenten sicher, daß dieses, im allgemeinen sehr aufwendige Verfahren, auch durchführbar ist. Für strukturelle Teilkomponenten kann das Verfahren analog zum globalen System angewendet werden.

 

Projektstatus

Projektstart war der 15. November 1995. In der ersten Phase des Projektes bis Mitte Mai 1996 wurden Untersuchungen durchgeführt, welche Art von Anforderungen an das zu entwickelnde System in SACRES behandelt werden können. Außerdem wurde in dieser Phase die Softwarearchitektur von SACRES definiert. Die Ergebnisse der ersten Phase wurden vom 9. bis 11. Juni durch den Projekt Officer und Gutachter der Europäische Union begutachtet. Hierbei kam es zu einer sehr positiven Einschätzung der erreichten Ergebnisse und weitergehenden Ziele des Projektes. Die anschließende und über das Jahr 1996 hinausgehende zweite Phase hat zum Ziel, Prototypen der Verifikationswerkzeuge bereitzustellen und an Fallstudien der SACRES Partner zu erproben. Diese Prototypen beinhalten noch nicht die Behandlung von Realzeiteigenschaften, sie behandeln qualitative Eigenschaften wie sie auch im FORMAT Kontext auftreten. Der Schwerpunkt von OFFIS lag hierbei in der Bereitstellung der Semantiken für StateCharts und SSL, sowie der Implementierung von Transformatoren von StateChart Spezifikationen in Modelle.

Am 5. und 6. Dezember 1996 fand eine weitere Begutachtung statt auf der insbesondere Fragen zur semantischen Integration der in SACRES verwendeten Sprachen diskutiert wurden. Auch hier kamen die Gutachter zu einer sehr positiven Einschätzung des Projekts. Die Bewilligung für die zweite Förderungsphase des Projekts wurde schon Ende Dezember vorab erteilt, obwohl diese Entscheidung erst Mitte März 1997 nach Ablauf und Begutachtung der zweiten Projektphase von der Europäischen Union zu treffen war.

 

Zusammenfassung

Dieses Projekt ergänzt auf einer technischen Ebene die in OFFIS durchgeführten Arbeiten im KORSYS-Projekt. Während in KORSYS die Schwerpunkte der Arbeiten auf Abstraktionstechniken zur Reduzierung der Modelle liegen, sollen innerhalb von SACRES die Erweiterung der Verifikationstechniken zur Behandlung von Realzeiteigenschaften im Vordergrund stehen. Insgesamt stellt das SACRES Projekt eine Reihe von Werkzeugen zur Verfügung die, zusammen mit der Methodologie, zur Unterstützung des Entwicklungsprozesses von Safety Critical Embedded Systems beitragen. Besonders hervorzuheben ist dabei die Abstützung auf den im industriellen Kontext verwendeten Sprachen StateCharts und Signal und die Verwendung von symbolischen Zeitdiagrammen zur graphischen Eingabe von Anforderungsdefinitionen.