• Computergestützte Verifikation /
  Computer Aided Verification
• Algorithmen für Services /
  Algorithms for Services

Projekt Computergestützte Verifikation / Project Computer Aided Verification

Wir setzen die Entwicklung des Modelchecking-Werkzeugs LoLA fort. LoLA verifiziert Systemeigenschaften durch erschöpfende Durchmusterung des Zustandsraumes. Dabei werden Reduktionstechniken zur Beherrschung des Zustandsraumexplosionsproblems entwickelt und implementiert.

We continue improving the model checking tool LoLA. LoLA verifies system properties through exhaustive state space exploration. In particular, we develop and implement reduction techniques for alleviating state explosion.

Reduktion durch Vertauschbarkeit / Partial Order Reduction

Zu den Reduktionstechniken gehört die Stubborn-Set-Methode, die vor allem auf verteilte Systeme gut anwendbar ist. In ihrer klassischen Variante bewahrt sie Deadlocks, in fortgeschrittenen Varianten beliebige Eigenschaften, die in temporaler Logik (LTL, später auch CTL) beschrieben werden können. Je größer die Zahl der bewahrten Eigenschaften ist, desto schwieriger ist es natürlich, substantielle Reduktion zu erzielen. Wir suchen daher nach Verbesserungen der Technik für sehr kleine, aber wichtige Klassen von Eigenschaften. Dabei nutzen wir die allgemein akzeptierte Erfahrung, dass in der Praxis auftretende Eigenschaften sich meist mit sehr einfachen (kurzen) temporallogischen Formeln beschreiben lassen.

The stubborn set method is a particular reduction technique which is particularly well suited for distributed systems. In its classical version, it preserves deadlocks. Advanced versions preserve arbitrary properties expressible in temporal logic (LTL, CTL). The larger a class of preserved properties is, the more difficult it is to obtain substantial reduction. Consequently, we aim at improved versions of the method for preserving small but frequently used classes of properties. We refer to the commonly accepted fact that most practically relevant properties can be specified with rather simple (short) formulas of temporal logic.

zurück zum Seitenanfang

Sweep-Line-Methode / Sweep-Line-Method

Die Sweep-Line-Methode nutzt Wissen über Progress im System aus, um alte, nicht mehr benötigte Zustände bereits während der Durchmusterung des Zustandsraumes wieder zu löschen. Das Wissen über Progress im System wird in Form einer sog. Progress-Measure vorgegeben. Wir haben eine Technik zur automatischen Berechnung einer Progress Measure vorgeschlagen. Diese Measure wollen wir unter Einsatz verschiedener Heuristiken verbessern. Weiterhin wollen wir die Sweep-Line-Methode insgesamt auf Möglichkeiten der Verbesserung hin untersuchen.

The sweep-line method exploits knowledge about progress in a system for deleting expired, no longer relevant states during a state space exploration. The notion of progress is thereby bound to a so called progress measure. We developed an algorithm for the automated calculation of a progress measure. We want to implement various heuristics for improving the quality of this measure. Furthermore, we want to investigate opportunities for speeding up the method in general.

zurück zum Seitenanfang

Abstraktion und Abstraktionsverfeinerung / Abstraction and Abstraction Refinement

Erfolgreiche Verifikation setzt eine Reduktion des gegebenen Systems auf seine für die untersuchte Eigenschaft wesentlichen Größen (Abstraktion) voraus. Es existieren einige Vorschläge zur Automatisierung des Abstraktionsprozesses. Dabei kann es passieren, dass wegen zu grober Abstraktion die Verifikationsresultate sich nicht auf das Originalsystem übertragen lassen. In einem solchen Fall kann man (ggf. auch automatisch) die ursprüngliche Abstraktion verfeinern und sich so iterativ an einen angemessenen Abstraktionsgrad herantasten. Wir wollen nach geeigneten Abstraktions- und Verfeinerungstechniken für Petrinetze (die Eingabesprache von LoLA) suchen.

For successful verification, it is inevitable to abstract the system to those entities which are relevant for the investigated property. There several approaches for automated abstraction. Using abstraction, it can happen that the verification result on the abstracted system are inconclusive for the original system. In such a case, it is possible to refine (even computer aided) the abstraction. This way, we can step by step approach a suitable abstraction. We look for abstraction and abstraction refinement techniques which are well suited for systems given as Petri nets (which is the input language for LoLA).

zurück zum Seitenanfang

Verteilte Verifikation / Distributed verification

Zur Beschleunigung von Verifikationsläufen sowie zur Nutzbarmachung der Speicherressourcen möglichst vieler Rechner wollen wir Verifikationstechniken auf Cluster oder Netzwerke von Workstations verteilen.

We want to distribute verification algorithms to a cluster or network of workstations. This way, we would like to speed up runtime at, at the same time, be able to employ the memory resources of all involved stations.

zurück zum Seitenanfang

Projekt Algorithmen für Services / Project Algorithms for Services

Ein Service besteht aus einem Interface, einer internen Kontrollstruktur und einer Identifikation. Er stellt einen in sich geschlossenen Dienst bereit, den z.B. andere Services lose anbinden können. Die Interaktion zwischen Services wird in service-orientierten Architekturen geregelt. BPEL ist eine junge Sprache zur Beschreibung von Services. Nichtsdestotrotz scheint sie sich zum Standard für die Beschreibung von Services zu entwicklen. Da BPEL sehr viele Features hat, die sich insbesondere auch im Laufe der Zeit ändern werden, ist es sinnvoll, formale Methoden für Services unabhängig von BPEL, auf der Basis einer einfachen Sprache zu entwickeln. Wir wählen dafür offene Workflownetze (oWFN), eine Klasse von Petrinetzen.

A service consists of an interface an internal control structure, and an identifier. It offers a well encapsulated functionality which can, for instance, be loosely invoked by other services. Interaction between services is organised in service oriented architectures. BPEL is a recently proposed language for specifying services. It is presumably the upcoming standard for describing services. Due to the large number of features of BPEL, which are subject to continues changes, it makes sense to develop formal methods for services independently of BPEL, and based on a simple language instead. We choose open workflow nets (oWFN), a class of Petri nets, for this purpose.

zurück zum Seitenanfang

Flexible Modelle aus BPEL / Flexible models of BPEL processes

Zur Nutzbarmachung der oWFN-Algorithmen für reale Anwendungen ist eine automatische Generierung von oWFN aus BPEL-Prozessen notwendig. Zwar existieren bereits formale Petrinetz-Semantiken für BPEL, diese führen aber zu zu großen oWFN. Daher wollen wir mittels statischer Analyse Informationen aus einem BPEL-Prozess extrahieren, mit deren Hilfe die Generierung einfacherer oWFN möglich wird.

For being able to use our oWFN based algorithms for real applications, it is necessary to generate oWFN out of BPEL specifications. There are already formal Petri net semantics for BPEL, but these semantics lead to prohibitively large oWFN. Thus, we aim at extracting information from the BPEL specification (using static analysis) which helps us to generate condensed oWFN.

zurück zum Seitenanfang

Bedienbarkeit / Controllability

Bedienbarkeit ist eine grundlegende Service-Eigenschaft. Ein Service ist bedienbar, falls es eine Umgebung gibt, in die eingebettet der Service vernünftig arbeitet. Dieses Problem zerfällt in viele Varianten, je nachdem,

• ob die Umgebung aus Teilen besteht, die zur Laufzeit oder zur Konstruktionszeit nicht miteinander kommunizieren (verteilte Umgebung),
• ob Nachrichten synchron oder asynchron fließen, ob sie gepuffert werden, ob kausale Zusammenhänge zwischen ihnen berücksichtigt werden
  (z.B. leeres Formular – ausgefülltes Formular: ein ausgefülltes Formular kann erst gesendet werden, nachdem ein leeres empfangen wurde) ,
• ob „korrekt arbeiten“ nur die Möglichkeit der Terminierung oder die Zusicherung von Terminierung bedeutet, ob Terminierung durch eine der Seiten erzwingbar sein soll,
• ob während der Arbeit bestimmte Aktionen oder Nachrichten ausgeschlossen oder erzwungen werden sollen.

Controllability is a fundamental property of a service. A service is controllable iff there exists an environment in which the service works properly. This problem has a number of instances depending on

• whether or not the environment is assumed to consist of independent parts which do not communicate with each other during run time, or during build time
• whether messages are passed synchronously or asynchronously, whether thea are buffered, whether causal dependencies are considered
  (e.g., empty form – filled form: a filled form can be sent only after having received an empty form),
• whether “working properly” means that it is always possible to terminate, or whether eventual termination is required, or whether termination should be enforceable by one of the parties
• whether or not certain actions or messages should be excluded or enforced.

zurück zum Seitenanfang

Bedienungsanleitungen (gefördert durch die DFG)/ Operating guidelines (funded by DFG)

Web Services spielen im Netz eine ähnliche Rolle wie öffentlich zugängliche Geräte (z.B. Passbildautomaten, Geträkeautomaten, Geldautomaten) in der realen Welt. Die realen Geräte stellen einem Nutzer typischerweise Instruktionen zu ihrer Bedienung bereit. Mit dem Konzept von Bedienungsanleitungen bilden wir diese Idee auf die virtuelle Welt der Web services ab. Insbesondere interessiert uns die automatische Generierung einer Bedienungsanleitung aus einer operationellen Servicebeschreibung sowie die algorithmische Unterstützung verschiedener Anwendungsszenarien im Serviceorientierten Rechnen.

In the virtual world, web services play a similar role as publicly available appliances such as teller machines, vending machines etc. in the real world. The appliances of the real world provide their users with instructions for a correct interaction. With our concept of operating guidelines, we aim at developing a similar concept for the virtual world of web services. We are particularly interested in an automated calculation of an operating guideline ifrom an operational service description and in algorithmic support for various application scenarios in the realm of service oriented computing.

zurück zum Seitenanfang

Adapter (gefördert durch die DFG)/ Adapter (funded by DFG)

Unabhängig entwickelte Services passen nicht notwendigerweise perfekt zusammen, lassen sich aber durch Zwischenschaltung eines Adapters passend machen. Ein Adapter kann z.B. Nachrichten umsortieren, kopieren, einige Arten von Nachrichten selbst generieren oder abfangen, neue Nachrichteninhalte aus vorhandenen Nachrichten rekombinieren usw. Diese Fähigkeiten sind sinnvollerweise eingeschränkt (ein Adapter soll kein Passwort „erraten“, keine materiellen Güter selbst generieren usw.).
Wir suchen ein möglichst einfaches Konzept, um die Möglichkeiten und Einschränkungen für die Fähigkeiten eines Adapters zu spezifizieren. Darauf aufbauend, studieren wir, unter welchen Umständen Services adaptierbar sind und ggf. Adapter automatisch generieren. Alle Fragens studieren wir anhand von oWFN.

It is unlikely that independently developed services fit. Nevertheless, it may be possible in many cases to make services fit through inserting an adapter between them. An adapter could, For instance, reorder and rearrange messages, copy, delete or generate some of them. These capabilities are typically restricted (an adapter should not generate a passwort or money, for instance).
We look for a concept which is as simple as possible but capable of expressing capabilities of an adapter. Based on that concept, we investigate, for which sets of services adapters exist, and construct such adapters automatically. We study these problems in the world of oWFN.

zurück zum Seitenanfang