Techniken zur Modellierung und Verifikation von Echtzeitsystemen
Jürgen Ruf
ISBN 978-3-89722-325-7
228 Seiten, Erscheinungsjahr: 1999
Preis: 40.00 Eur
Stichworte/keywords: Formale Methoden , Systementwurf , Verifikartion , Echtzeitsysteme , Temporallogik
Der rasante Fortschritt auf dem Gebiet der elektronischen Systeme hat in den
vergangenen Jahren dazu geführt, daß unser tägliches Leben in immer stärkerem
Maße von elektronischen Geräten beeinflußt wird. Heutzutage befinden sich im
Durchschnitt in jedem Haushalt zehn bis zwanzig Mikrocontroller, in modernen
PKWs kommen sogar bis zu 40 Mikrocontroller zum Einsatz. Auch in Bereichen,
die durch sehr hohe Sicherheitsanforderungen geprägt sind, hat die Mikroelektronik
Einzug gehalten, zum Beispiel in der Medizintechnik, bei Verkehrsleitsystemen,
in Produktionsautomatisierungssystemen oder im Finanzwesen.
Der massive Einsatz elektronischer und insbesondere digitaler Systeme zwingt die
Hersteller dazu, in immer kürzeren Abständen neue Produkte auf den Markt zu bringen.
Eine ausgiebige Fehlersuche durch Simulations- und Testmethoden ist aufgrund der
kurzen Entwicklungszyklen nicht mehr möglich. Zudem wird von solchen Verfahren nur
ein endliches Teilverhalten der Systeme untersucht.
Auf der anderen Seite sind Fehler, die eine Überarbeitung eines Systems notwendig
machen, sehr kostspielig, insbesondere wenn integrierte Schaltkreise bereits gefertigt
wurden und erneut durch den Entwurfs-Produktionszyklus laufen müssen. Außerdem können
fehlerhafte Systeme, wenn sie sich im Einsatz befinden, finanzielle oder materielle
Schäden verursachen oder sogar zu einer Bedrohung von Menschenleben werden.
Um diesen Umständen Rechnung zu tragen, wurden in den letzten Jahren große Anstrengungen
unternommen, die Fehlersuche bereits in frühen Stadien des Entwurfs zu unterstützen.
Dazu wurden Verfahren entwickelt, die mittels mathematischer Methoden die Durchführung
von Korrektheitsbeweisen unterstützen (formale Verifikation). Die ersten ausgereiften
vollautomatischen Verifikationswerkzeuge haben bereits Einzug in die Entwicklungslabors
von Industrieunternehmen gehalten. Diese Techniken eignen sich vorwiegend für die
funktionale Überprüfung von vollsynchronen digitalen Schaltungen.
Durch den Einsatz eingebetteter Systeme, die aus vielen unterschiedlichen Modulen
(analog, digital, mechanisch, ...) zusammengesetzt sind, spielt die Überprüfung von
Zeiteigenschaften eine immer wichtigere Rolle. So muß zum Beispiel die Steuerung
eines ABS-Systems nicht nur funktional korrekt arbeiten und die Bremsbacken beim
Blockieren der Räder wieder öffnen, sondern es muß auch sichergestellt sein, daß
dies innerhalb einer maximalen Zeitschranke geschieht. Oder es muß in einem chemischen
Reaktor garantiert werden, daß die Ventile für die Heiß- und Kaltluft, die 5 Sekunden
zum Öffnen und Schließen benötigen, niemals gleichzeitig offen sind.
In dieser Arbeit wird ein neues Verfahren vorgestellt, das es erlaubt, modular
aufgebaute, zeitbehaftete Systeme zu beschreiben und spezifische Zeiteigenschaften
dieser Systeme automatisch und formal abgesichert nachzuweisen. Dazu werden bekannte
effiziente Algorithmen, die für vollsynchrone Systeme entworfen wurden, als Grundlage
herangezogen und so erweitert, daß der neue Ansatz ihre guten Komplexitätseigenschaften
beibehält. Um dieses Ziel zu erreichen werden erstmals zu diesem Zweck multiterminale
Entscheidungsdiagramme (MTBDD) eingesetzt.
Außerdem werden die formalen Modelle, anhand derer die Verifikation durchgeführt wird,
so um eine quantitative Zeitkomponente erweitert, daß eine einfache Modellierung möglich
ist, und daß sich viele Klassen von Systemen in diesem Formalismus beschreiben lassen.
Zur Spezifikation von Zeiteigenschaften wird eine bekannte temporale Logik eingesetzt,
die im Rahmen dieser Arbeit ebenfalls um einen quantitativen Zeitbegriff erweitert wird.
Zudem dienen neue Operatoren dazu, komplexe Zeiteigenschaften intuitiv mit dieser Logik
beschreiben zu können.
zurück zum Katalog
Startseite
