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
Criteria of this press release:
Information technology, Mathematics, Mechanical engineering, Physics / astronomy
transregional, national
Research projects
German
You can combine search terms with and, or and/or not, e.g. Philo not logy.
You can use brackets to separate combinations from each other, e.g. (Philo not logy) or (Psycho and logy).
Coherent groups of words will be located as complete phrases if you put them into quotation marks, e.g. “Federal Republic of Germany”.
You can also use the advanced search without entering search terms. It will then follow the criteria you have selected (e.g. country or subject area).
If you have not selected any criteria in a given category, the entire category will be searched (e.g. all subject areas or all countries).
