Uni-Logo
English      
Rechnerarchitektur - Arbeitsgruppe Bernd Becker
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

AVACS: Automatic Verification and Analysis of Complex Systems

| Beteiligte Mitarbeiter | Kooperationspartner | Projektbeschreibung | Zielsetzung des Projekts | Struktur des Projekts | Vorträge |


Beteiligte Mitarbeiter

ehemalige Mitarbeiter Lehrstuhl für Rechnerarchitektur
Marc Herbstritt, Dr. wissenschaftlicher Mitarbeiter
Natalia Kalinnik, Dipl.-Inf. (Mitarbeit in H1/2) wissenschaftlicher Mitarbeiter
Ilia Polian, Dr. (Mitarbeit in R2 und H2) wissenschaftlicher Mitarbeiter
Erika Ábrahám, Dr. (Mitarbeit in H2) wissenschaftlicher Mitarbeiter
Frank Schmiedle, Dr.-Ing. (Mitarbeit in S3) wissenschaftlicher Mitarbeiter
Jochen Eisinger, Dr. (Mitarbeit in R2 und H1) wissenschaftlicher Mitarbeiter
Lehrstuhl für Rechnerarchitektur
Angelika Fabry-Flashar (Verwaltung) Verwaltung
Bernd Becker, Prof. Dr. (Stellvertr. Sprecher, Site-Koordinator für Freiburg. Mitarbeit in H1/2, S1 und S3) Kontakt
Tobias Schubert, Dr. (Mitarbeit in H1/2) wissenschaftlicher Mitarbeiter
Matthew Lewis, M.Sc.(Eng) (Mitarbeit in S1) wissenschaftlicher Mitarbeiter
Ralf Wimmer, Dipl.-Inf. (Mitarbeit in S3) wissenschaftlicher Mitarbeiter
Stefan Kupferschmid, Dipl.-Inf. (Mitarbeit in H1/2) wissenschaftlicher Mitarbeiter
Bettina Braitling, Dipl.-Inf. (Mitarbeit in S3) wissenschaftlicher Mitarbeiter
Karsten Scheibler, Dipl.-Inf. (Mitarbeit in H1/2) wissenschaftlicher Mitarbeiter
Christian Miller, Dipl.-Inf. (Mitarbeit in S1) wissenschaftlicher Mitarbeiter
Peter Winterer, Dipl.-Ing. (FH) (Technische Verwaltung) Technische Verwaltung
Kooperationspartner

Universität Freiburg
Dagmar Sonntag (SFB-Verwaltung) Verwaltung


Projektbeschreibung

Am "SFB" sind neben IRA die Freiburger Lehrstühle für Künstliche Intelligenz, Softwaretechnik und Betriebssysteme sowie Forschergruppen der Universitäten Oldenburg, Saarbrücken, der Tschechischen Akademie der Wissenschaften in Prag und des Max-Planck-Instituts Saarbrücken beteiligt. Der Projektinhalt ist die Analyse und formale Verifikation komplexer Systeme. Das neue European Train Control Standard wird als Fallstudie zur Erprobung der entwickelten Methoden dienen. Die Wissenschaftler unseres Lehrstuhls werden insbesondere ihre Kompetenz im Bereich der Basistechnologien in den SFB einbringen. Die Genehmigung des SFB für zunächst acht Jahre (mit einer Verlängerungsmöglichkeit für bis zu weiteren vier Jahren) bietet vor allem jungen Forschern eine ausgezeichnete Möglichkeit, strategische Kompetenz in Verifikation von hybriden und Echtzeitsystemen aufzubauen. Wir sehen diesen Vertrauensbeweis seitens der DFG auch als eine Bestätigung unserer bisherigen Forschungsarbeit.

Weitere Informationen finden sich auf der [AVACS Homepage]



Zielsetzung des Projekts

Wie kaum ein anderes Gebiet muss sich die Informationstechnik der Herausforderung stellen, dass ihre Artefakte flexibel und mit vergleichsweise geringem Aufwand technisch machbar sind, bei gleichzeitiger Verdoppelung der technischen Leistungsfähigkeit ihrer Basiskomponenten alle 2 Jahre. Dies hat dazu geführt, dass komplexe Computer-basierte Systeme gebaut und flächendeckend eingesetzt werden, von deren korrektem Verhalten man sich zwar durch Testen zu überzeugen versucht, deren Funktionsweise man in ihrer Gesamtheit aber nicht überschaut. Was technisch gemacht wird übersteigt bei weitem das, was man analytisch versteht. Dieses ist nicht nur vom wissenschaftlichen Standpunkt unbefriedigend, es birgt auch ein hohes Risiko für Leib und Leben der Menschen, die diesen Systemen etwa in Haushalt, Auto, Bahn, Flugzeug, Kraftwerken, Industrieanlagen ausgesetzt sind, ganz abgesehen von den hohen ökonomischen Schäden, wenn es durch Fehler zur Zerstörung teurer Anlagen (Ariane V) kommt oder wenn Schadensersatzleistungen anderer Art notwendig werden.

Der Transregio SFB AVACS widmet sich besonders den Systemen, die in sicherheitskritischen Bereichen eingesetzt werden und dort physikalische und technische Prozesse kontrollieren und steuern, wie etwa im Transportwesen bei Auto, Eisenbahn und Flugzeug. Die Komplexität der in diesen Anwendungen verwendeten Systeme hat mehrere Ursachen. Erstens, wenn physikalische Prozesse beobachtet und gesteuert werden, kommt es zur Interaktion von diskreten und kontinuierlichen Systemen, die mathematisch besonders komplex sind in ihrer Modellierung und Analyse. Steuerungsvorgänge müssen in vorgegebenen Zeitschranken ablaufen und Steuersignale so berechnen, dass der physikalische Prozess innerhalb des sicheren Bereiches bleibt. Eine zweite Ursache von Komplexität liegt in der Architektur dieser Systeme, wo eine große Anzahl von Komponenten miteinander vernetzt sind, miteinander kommunizieren und in kooperierender Weise die Funktion des Gesamtsystems bestimmen. Drittens sind solche Systeme mobil sowohl im physikalischen, wie im informationstechnischen Sinn. Mobile Computerprogamme und -systeme müssen in ständig wechselnden Umgebungen mit oftmals unbekannten Parametern zuverlässig und fehlertolerant funktionieren.

Die für AVACS ins Auge gefassten Forschungsziele beruhen auf der Erkenntnis, dass Systemzuverlässigkeit nur dann flächendeckend entscheidend verbessert werden kann, wenn kritische Eigenschaften sowohl in der Spezifikation wie in der Realisierung mit automatisierten Techniken, also auf Knopfdruck, vom Softwareingenieur analysisert und überprüft werden können. Die kombinatorische Komplexität der Systemzustände ist zu hoch, die mathematischen und logischen Fähigkeiten der Ingenieure oft nicht ausreichend, und der zeitliche Aufwand zu groß, als dass nichtautomatische Methoden in großem Stil einsetzbar wären.

Die Vision von AVACS ist es, dass nach Ablauf des Projektes die Zeitanforderungen auch an hochgradig vernetzte Systeme automatisch überprüft werden können, sowohl auf der Modellebene, wie auch für die auf der realen Hardware ablaufenden Maschinenprogramme. AVACS wird dabei in neue Größenordnungen von Systemkomplexität (Anzahl der Systemzustände, Nutzung moderner Hardwarekomponenten, algorithmisch optimierte Controller mit spezialisierten Datenstrukturen) vorstoßen.

Bei den hybriden Systemen, wo diskrete Controller kontinuierliche wie diskontinuierliche physikalische Prozesse beobachten und steuern, wird AVACS wesentlich realistischere Systemmodelle als bisher betrachtet beherrschen helfen und gleichzeitig die Differenziertheit der an diesen Modellen automatisch überprüfbaren Aussagen über Stabilität und Sicherheit wesentlich verfeinern.

Schließlich wird AVACS Methoden entwickeln, die eine neue Qualität der Analyse des globalen Zusammenspiels von Teilkomponenten komplexer Systeme herstellen. Hierzu zählen Techniken zur Untersuchung der Interaktion von Steuergeräten in Bezug auf die Realisierung einer Gesamtfunktionalität, zur Analyse von Kooperationsmechanismen bei sich dynamisch ändernden Kommunikationstopologien sowie zum formalen Nachweis globaler Verfügbarkeitsanforderungen. Durch die in AVACS geplanten Arbeiten werden Analysen dieser wichtigen Systemeigenschaften zum Teil erstmalig automatisiert und auch für solche Systeme einsetzbar werden, die sich bisher aufgrund ihrer Komplexität entsprechenden Untersuchungen entzogen.

Zur Verwirklichung dieser Vision braucht es die Kombination von Methoden der mathematischen Semantik komplexer Systeme (Fundierung) mit algorithmisch-deduktiver Experise (Automatisierung), wie sie im AVACS-Konsortium gegeben ist.



Struktur des Projekts

Der AVACS SFB ist in drei Bereiche unterteilt:

Projektbereich R: Realzeit-Systeme
Projektbereich H: Hybride System
Projektbereich S: Grobgranulare Systemstrukturen

Die einzelnen Projektbereiche sind jeweils wieder unterteilt in
Teilprojekte:

Projektbereich R:
Teilprojekt R1: Mehr als Timed Automata
Teilprojekt R2: Zeitanalysen, Scheduling und Verteilung von Realzeit-Tasks
Teilprojekt R3: Heuristisches Suchen und Abstraktes Model-Checking für Realzeit-Systeme

Projektbereich H:
Teilprojekt H1/2: Constraint-basierte Verifikation für hybride Systeme
Teilprojekt H3: Automatische Abstraktion für Hybride Controller
Teilprojekt H4: Automatische Verifikation von Stabilitätseigenschaften in Hybriden Systemen

Projektbereich S:
Teilprojekt S1: Kompositionelle Verifikation komplexer Systeme
Teilprojekt S2: Dynamische Kommunikationssysteme
Teilprojekt S3: Formale Verifikation von Verfügbarkeitseigenschaften

Zusätzlich gibt es noch einen Projektbereich Z (Zentrale Dienste).

Genauere Informationen über die Projektstruktur erhalten sie unter [AVACS Homepage].





Vorträge

Hinweise zum Betrachten der Aufzeichnungen finden sie unter
[Hinweise]

Liste der Vortrge