Sprungmarken

Servicenavigation

Hauptnavigation

Sie sind hier:

Hauptinhalt

PG 507: LiVe - Lernen impliziter Verhaltensmodelle

 

Thema

Entwicklung eines Frameworks zur Generierung von globalen Zustands- Modellen aus ECA-Regelsystemen.

 

Motivation

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].

 

Ziele

Abbildung 1: Beispiel eines ECA Regelsystems
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 regel­basierten 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
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 wer­den. 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:

  1. Festlegung einer geeigneten Sprache zu Spezifikation von regelbasierten Systemen: Die Projektgruppe wählt eine bestehende Sprache zu Spezifikation von regelbasierten Systemen aus und implementiert die zugehörigen Compiler-Komponenten (Scanner, Parser, Semantische Analyse, ...)
  2. Ausführungsumgebung für regelbasierte Systeme: Es wird ein Laufzeitsystem entwickelt, mit dem sich regelbasierte Systeme direkt ausführen lassen. Außerdem muss entschieden werden können, ob ein regelbasiertes System eine Anweisungsfolge zulässt oder nicht. Dabei ist zu beachten, dass die gewählten Anwendungs-Szenarien auch zu integrieren sind.
  3. Automaten-Lern-Schnittstelle: Die vom Lehrstuhl entwickelte Bibliothek zur Analyse von Automaten-Lern-Algorithmen (LearnLib) [3] wird an die entwickelte Ausführungsumgebung angepasst und gegebenenfalls erweitert.
  4. Modell-Checking: Der vom Lehrstuhl entwickelte Modell-Checker wird integriert. Hierdurch ermöglicht es die Projektgruppe globale Eigenschaften von regelbasierten Systemen zu verifizieren. Die Ergebnisse des Modell-Checkings werden mit den bestehenden graphischen Visualisierungs-Tools dargestellt.
  5. Evaluation: Hier sollen die ausgewählten Anwendungsszenarien mit Hilfe der entwickelten Technologie untersucht werden.

 

Teilnahmevoraussetzungen

Erforderlich

  • Fundierte Kenntnisse mindestens einer objektorientierten Programmiersprache wie beispielsweise Java, C++, o.ä.
  • Kenntnisse in mindestens einem der Gebiete Übersetzerbau, Testorganisation komplexer Systeme, Formale Methoden des Systementwurfs, Grundlagen des Modell-Checking oder Softwarekonstruktion durch Teilnahme an einer entsprechenden Vorlesung.

Wünschenswert

  • Kenntnisse im Design graphischer Benutzeroberflächen
  • Expertensysteme, insbesondere ECA-Regelsysteme
  • Objektorientierte Modellierung (UML) [11]

 

Zeitraum

Wintersemester 2006/2007 und Sommersemester 2007

 

Umfang

Jeweils 8 Semesterwochenstunden

 

Veranstalter

  • Prof. Dr. Bernhard Steffen
  • Dipl.-Inform. Harald Raffelt
  • Dipl.-Inform. Christian Kubczak

 

Literatur zur Projektgruppe

  1. S. Gilmore and M. Ryan editors. Language Constructs for describing Features, Springer-Verlag, 2000
  2. C. Higuera. A Bibliographical Study of Grammatical Inference. In Pattern Recognition 38, pp 1332-1348, Elsevier, 2005
  3. H. Raffelt, B. Steffen, and T .Berg. Learnlib: A library for automata learning and experimentation. In Proc. of the 10th Int. Workshop on Formal Methods for Industrial Critical Systems FMICS'05, vol.3440 of LNCS, pp. 557-562, Spinger-Verlag
  4. M. Broy, B. Jonsson, J. Katoen, M. Leucker, and A. Pretschner. Model-Based Testing of Reactive Systems:, vol. 3472 of LNCS. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2005.
  5. D. Angluin, Learning Regular Sets from Queries and Counterexamples, Information and Computation, vol 2 no. 75,pp. 87-106, 1987
  6. J. E. Cook, Z. Du, C. Liu, A. L. Wolf. Discovering Models of Behavior for Concurrent Systems Tech. rep. New Mexico State University, Dept. of Computer Science, Aug. 2002
  7. J. E. Cook, A. L. Wolf Discovering Models of Software Processes from Event-Based Data ACM Trans. on Software Engineering and Methodology (TOSEM) pp. 215-249, 1998
  8. L. Mariani, M. Pezzè. A technique for verifying component-based software Proc. of the Int. Workshop on Test and Analysis of Component Based Systems, TACOS 2004, Barcelona, March 2004
  9. D. Peled, M. Y. Vardi, M. Yannakakis. Black Box Checking Formal Methods for Protocol Engineering and Distributed Systems, (FORTE/PSTV), pp. 225-240, 1999, Kluwer.
  10. B. Steffen and H. Hungar, Behavior-based model construction. In S. Mukhopadhyay and L. Zuck, editors, Proc. 4th Int. Conf. on Verification, Model Checking and Abstract Interpretation, LNCS 2575, Springer 2003.
  11. G. Booch, J. Rumbaugh, and I. Jacobson. The Unified Modelling Language User Guide. Addison Wesley, 1999.
  12. G. Joeris and O. Herzog. Towards Flexible and High-Level Modeling and Enacting of Processes. In Jarke, M.; Oberweis, A. (eds.): Advanced Information Systems Engineering, Proc. of the 11th Int. Conference, CAiSE’99, LNCS 1626, Springer Verlag, pp. 88-102
  13. G. Kappel, P. Lang, S. Rausch-Schott, and W. Retschitzegger. Work ow management based on objects, rules, and roles. IEEE Data Engineering Bulletin, 18(1):11-18, March 1995.
  14. A. Hagerer, H. Hungar, O. Niese, and B. Steffen. Model generation by moderated regular extrapolation. In Proc. of the 5th International Conference on Fundamental Approaches to Software Engineering, vol. 2306 of LNCS, pages 80-95, Springer-Verlag, 2002.


Nebeninhalt

 

Kontakt

Tel. (0231) 755-5801
Fax (0231) 755-5802