idw – Informationsdienst Wissenschaft
Nachrichten, Termine, Experten
Nachrichten, Termine, Experten
Schon während des Entwurfs sollten potentielle Fehler im Design technischer Systeme - wie z.B. von Kommunikationsprotokollen oder Verkehrssicherungssystemen - nach Möglichkeit erkannt und behoben werden. In diesen Zusammenhang ordnet sich das Projekt "Automatische Verifikation von Qualitätsmerkmalen verteilter Systeme" ein, das an der Universität Erlangen-Nürnberg am Lehrstuhl für Rechnerarchitektur und -Verkehrstheorie von Prof. Dr. Ulrich Herzog durchgeführt wird. Forschungen zur Spezifikation und Verifikation paralleler Prozesse gewinnen auch in der Industrie immer mehr an Bedeutung.
Als formale Spezifikationsmethode werden Prozeßalgebren verwendet, die das funktionale Verhalten von Prozessen, wie z.B. die Reihenfolgebeziehungen zwischen Aktivitäten oder den Kontrollfluß eines parallelen Programms, beschreiben. Da in vielen Fällen nicht nur eine qualitative, sondern auch eine quantitative Systemanalyse von Interesse ist, wurden Prozeßalgebren um stochastische Zeitattribute erweitert. Solche stochastische Prozeßalgebren ermöglichen es, bereits in der Entwurfsphase eines Systems eine Leistungsbewertung durchzuführen, um mögliche Leistungsengpässe frühzeitig zu erkennen.
Für die Formalisierung der relevanten quantitativen Eigenschaften werden temporale Logiken und zugehörige Verifikationsalgorithmen entwickelt. Das Ziel ist die vollautomatische Verifikation (das sog. Model Checking), d.h. der Entwurf von Algorithmen, die als Eingabe einen stochastischen Prozeß und die temporallogische Spezifikation von (zeitlichen) Eigenschaften haben und testen, ob der Prozeß die Eigenschaften erfüllt. Ein Beispiel wäre die Frage: "Ist die Wahrscheinlichkeit, daß nach Auslösen eines Alarms innerhalb von 100 ms eine Reaktion erfolgt, ohne daß zwischenzeitlich eine kritische Situation eintritt, größer als 99,8 Prozent"?
Explosion des Zustandsraums
Bedingt durch die enorme Anzahl von Zuständen (100 Trillionen oder mehr), die ein reales System annehmen kann, sind Verifikationstechniken, die auf einer expliziten Darstellung des Zustandsraums (meist in Form einer Matrix) beruhen, in der Praxis nur bedingt einsetzbar. Um dieser sog. Zustandsraumexplosion entgegenzuwirken, haben sich für die Analyse qualitativer Systemeigenschaften zwei prinzipielle Strategien etabliert: Symbolische Methoden, die mit einer impliziten Darstellung des Zustandsraums arbeiten (binary decision diagrams), und Methoden, die auf der Reduktion des Zustandsraums mittels Halbordnungen beruhen (partial order reduction). Im Rahmen des Projekts wird an einer Erweiterung dieser Methoden für eine quantitative Systemanalyse gearbeitet, einer Fragestellung, die bisher weitgehend unerforscht ist.
An den Forschungen sind die Universität Mannheim, die University of Birmingham und die University of Edinburgh beteiligt. Das Projekt wird vom DAAD und dem British Council seit dem 1. Juli 1998 gefördert und hat zunächst eine Laufzeit von zwei Jahren. Seit April 1999 wird außerdem ein Mitarbeiter des Lehrstuhls mit dem Thema "Automatische Verifikation" von der DFG gefödert.
* Kontakt:
Prof. Dr. Ulrich Herzog, Dr. Markus Siegle
Lehrstuhl für Informatik (Rechnerarchitektur und -Verkehrstheorie)
Martensstraße 3, 91058 Erlangen
Tel.: 09131/85 -27041, -28339, Fax: 09131/85 -27409
E-mail: siegle@informatik.uni-erlangen.de
http://www7informatik.uni-erlangen.de/~siegle
Merkmale dieser Pressemitteilung:
Informationstechnik, Maschinenbau, Mathematik, Physik / Astronomie
überregional
Forschungsprojekte
Deutsch
Sie können Suchbegriffe mit und, oder und / oder nicht verknüpfen, z. B. Philo nicht logie.
Verknüpfungen können Sie mit Klammern voneinander trennen, z. B. (Philo nicht logie) oder (Psycho und logie).
Zusammenhängende Worte werden als Wortgruppe gesucht, wenn Sie sie in Anführungsstriche setzen, z. B. „Bundesrepublik Deutschland“.
Die Erweiterte Suche können Sie auch nutzen, ohne Suchbegriffe einzugeben. Sie orientiert sich dann an den Kriterien, die Sie ausgewählt haben (z. B. nach dem Land oder dem Sachgebiet).
Haben Sie in einer Kategorie kein Kriterium ausgewählt, wird die gesamte Kategorie durchsucht (z.B. alle Sachgebiete oder alle Länder).
