Entwicklung eines Frameworks zur Generierung von globalen Zustands- Modellen aus ECA-Regelsystemen.
ECA (Event/Condition/Action) Regeln [1,12,13] sind das dominantes Format zur Beschreibung von Reaktiven Systemen in der Praxis. Hunderte von Regeln definieren
Telefonsysteme: „B wählt Nummer von A / A auf Blacklist von B / A wird abgewiesen“
Internetdienste: „A klickt Link X / A hat die Berechtigung für X / A erhält Zugang zu X“
Workflowsystem: „A sendet Teilresultat X / B ist Kooperationspartner / Y bekommt X“
Zwar ist die Definition einzelner solcher Regeln einfach und intuitiv, ihr globaler Einfluss auf den durch viele Regeln definierten Gesamtdienst bleibt jedoch im Dunkeln. Tatsächlich ist es oft kaum möglich nachzuvollziehen, was passiert, wenn nur eine weitere Regel hinzugefügt wird. Zuverlässige Dienste können durch kleinste Variantenbildung an thematisch entfernten Teilen lahm gelegt werden. Dieser Effekt, eine Variante der sogenannten Feature Interaction kann gut an einem themenfremden Beispiel illustriert werden:
Eine Autofirma hatte ein neues Sicherheitssystem (also ein komplexes Security-Feature) für ihre Luxusklasse vorgestellt und einen Preis für den geboten, dem es gelingt, den Wagen ohne Schlüssel zu öffnen. Ein `Experte` nahm daraufhin einen Gummihammer und schlug auf die vordere Stoßstange, worauf alle Türen aufsprangen – eine Maßnahme zur Bergung von Verletzten nach einem (hier vermeintlichen) Unfall (ein Personenschutz Feature).
Das wegen der Wichtigkeit des Personenschutzes vorrangige Feature hatte den Security-Mechanismus außer Kraft gesetzt. Es ist wohl offensichtlich, wie derartige Effekte Dienste jeder Art bedrohen können. Aufgedeckt werden können sie nur auf Basis globaler Modelle, die das Gesamtsystem abdecken.
Da einzelne Regeln immer nur sehr lokale Verhaltensweisen und Eigenschaften eines Systems beschreiben, ist es nicht möglich globale Eigenschaften des Gesamtsystems anhand der Regeln abzulesen, geschweige denn formal nachzuweisen. Allerdings lassen sich globale Eigenschaften leicht mit Hilfe temporal-logischer Formeln formal beschreiben. Diese finden eine breite Anwendung bei der Verifikation von Hard- und Softwaresystemen [4]. Tatsächlich ist es möglich, mit Hilfe formaler Verifikationstechniken Feature Interactions, beispielsweise durch Modell-Checking Techniken, unmittelbar zu erkennen. Diese wissenschaftlich fundierten Methoden setzen aber in der Regel Modelle in Form erweiterter (endlicher) Automaten (Transitionssysteme) voraus. Eine direkte Umwandlung von regelbasierten Systemen in Transitionssysteme gemäß einer operationalen Semantik scheitert aber typischerweise daran, dass die entstehenden Transitionssysteme unendlich oder zumindest so groß würden, dass sie nicht mehr beherrscht werden können.
Eine vielversprechende Lösung bieten Lernverfahren für endliche Automaten. Das Lernen von endlichen Automaten wird auch als regular inference bezeichnet, und bildet ein Teilgebiet des maschinellen Lernens. Automaten-Lern-Verfahren sind nicht nur von theoretischem Interesse, sie lassen sich vielfältig im Bereich der Hard- und Softwareentwicklung einsetzen [6–10]. Eine umfassende Übersicht über das Themengebiet gibt C. Higuera [2]
Lernverfahren ermöglichen es abstrakte, sogar Aspekt-spezifische, aber dennoch konsistente, globale Modelle auf Basis von Beobachtung des Ein- und Ausgabeverhaltens eines Systems abzuleiten und ggf. nach Bedarf zu verfeinern. Auf diese Weise lassen sich `spielerisch´ Problem-angemessene Modelle konstruieren. Dies wurde bereits im Rahmen eines industriellen Projektes im Bereich der integrierten Computer/Telefonie Systeme (Computer Telephony Integrated Systems) gezeigt [14].
Abbildung 1: Beispiel eines ECA Regelsystems
Im Rahmen der Projektgruppe soll ein Framework entstehen, das es erlaubt, aus ECA-Regelsystemen globale Modelle zu generieren. Wichtig ist dabei die Möglichkeit, mit dem Abstraktionsniveau der Modellbildung zu „spielen“, da „naive“ Ansätze notwendig an der generierten Modellgröße scheitern (Zustandsexplosion). Um das zu erreichen soll die am Lehrstuhl V entwickelte LearnLib [3] eingesetzt werden, eine Bibliothek für praxisorientiertes Lernen von Verhaltensspezifikationen. Sie basiert auf Angluins Lern-Algorithmis L* [5] und ist direkt für derartige maßgeschneiderte Modellkonstruktionen konzipiert worden.
Zu den Hauptaufgaben der Projektgruppe zählt jedoch die Entwicklung einer Ausführungsumgebung für regelbasierte Systeme. Dieser Simulator soll zusammen mit der LearnLib eingesetzt werden, um beobachtungsbasiert konsistente Automatenmodelle aus regelbasierten Systemen abzuleiten. In einer zweiten Phase soll das entstandene Framework an den vom Lehrstuhl entwickelten Modell-Checkers GEAR zur Verifikation der extrapolierten Modelle angebunden werden. Die grobe Architektur des anvisierten Gesamtsystems ist in der Abbildung 2 dargestellt.
Abbildung 2: Verifikation von ECA-Regelsystemen
Die von der Projektgruppe entwickelte Lösung soll anschließend anhand zweier strukturell möglichst unterschiedlicher praxisrelevanter Beispiele evaluiert werden. Hier bieten sich beispielsweise eine Anwendung aus dem Bereich der `Value-Added´ Telefonieservices (hier könnte z.B. die Voice-over-IP-Testanlage des Lehrstuhls einbezogen werden) und eine aus dem Bereich personalisierter Workflowsysteme (hier gibt es mögliche Anknüpfungspunkte an Office-Automatisierungs- und Supply-Chain-Management-Systeme) an.
Im Einzelnen sind folgende Teilaufgaben vorgesehen:
Erforderlich
Wünschenswert
Wintersemester 2006/2007 und Sommersemester 2007
Jeweils 8 Semesterwochenstunden