MENÜ MENÜ  

Techniken zur Modellierung und Verifikation von Echtzeitsystemen

Jürgen Ruf

ISBN 978-3-89722-325-7
228 pages, year of publication: 1999
price: 40.00 €
Techniken zur Modellierung und Verifikation von Echtzeitsystemen
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.

Keywords:
  • Formale Methoden
  • Systementwurf
  • Verifikartion
  • Echtzeitsysteme
  • Temporallogik

BUYING OPTIONS

40.00 €
only 1 in stock