Forschungsbereich Computergestützte Verifikation / Research Area Computer Aided Verification
Verifikationstechniken für Petrinetze auf Multicore-Architekturen / Verification Techniques for Petri Nets on Multicore Architectures
gefördert durch:



Laufzeit: 2012-2014

Für eine weitere Steigerung der Leistungsfähigkeit werden Rechner immer häufiger mit Mehrkernprozessoren ausgestattet. Um diese Leistung abzurufen, reichen Compilertechniken für sequentielle Programme nicht aus. Daher erarbeiten wir Algorithmen, die algorithmisch herausfordernde Probleme im Bereich der computergestützten Verifikation von Petrinetzen lösen und dabei von der Arbeit auf  Mehrkernprozessoren profitieren.

Aiming at further increase of computing power, more and more computers are equipped with multicore processors. For benefitting from that power, we cannot rely on compiler technology for sequential programs. Hence, we develop algorithms for solving computationally challenging problems in the area of computer aided verification of Petri nets which benefit from the presence of multicore processors.

Strukturelle Analysetechniken für Petrinetze / Structural Verification Techniques for Petri Nets
gefördert durch / funded by:



Laufzeit: 2009-2011

Ziel der strukturellen Analyse ist es, Systemeigenschaften zu ermitteln, ohne dabei auf die Durchmusterung der erreichbaren Zustände angewiesen zu sein. Wir entwickeln neue und leistungsfähigere Techniken zur strukturellen Analyse von Petrinetzen und validieren diese mittels prototypischen Implementierungen in diversen Fallstudien.

Structural Analysis aims at determining system properties without exploring the set of reachable states. We develop new and powerful methods for structural analysis of Petri nets. The results are implemented in tool prototypes and validated in various case studies.

Zustandsraumverifikation / State Space Verification
gefördert durch / funded by




Laufzeit: 2006-

Unter Zustandsraumverifikation verstehen wir die systematische und erschöpfende Durchmusterung aller erreichbaren Zustände eines Systems mit dem Ziel der Überprüfung einer Systemeigenschaft. Unsere Gruppe trägt Techniken zur Reduktion der Zahl zu betrachtender Zustände bei, wobei der Schwerpunkt auf spezialisierten Techniken für häufig verwendete Standardeigenschaften liegt. Die Ergebnisse werden im Werkzeug LoLA implementiert und in Fallstudien aus unterschiedlichen Gebieten validiert, darunter Geschäftsprozessmodelle, Modelle von Servicekollaborationen, von asynchronen Schaltkreisen, von biochemischen Reaktionsketten, von KI-Planungsproblemen und von Problemen im Zusanmmenhang mit der Verifikation parametrisierter Boolescher Programme.

State space verification refers to the systematic and exhaustive traversal of all reachable states of a given system for the purpose of verifying a system property. Our group contributes techniques for reducing the number of states to be visited. Our focus is on dedicated methods for frequently used standard properties. Our results are available through the tool LoLA . We validate our methods in numerous case studies from different area, including workflow models, models of service collaborations, asynchronous circuits, AI planning problems, biochemical reaction chains, and problems in the context of verification of parameterized Boolean programs.

Forschungsbereich Algorithmen für Services / Research Area Algorithms for Services
Zuverlässig sichere Web Services für Geräte / Reliably Secure Web Services for Devices
gefördert durch / funded by:



Laufzeit: 2010-2012

Werden Geräte über standardisierte Schnittstellen in serviceorientierte Architekturen eingebunden, entstehen besondere Anforderungen an die Sicherheit des Gesamtsystems. Wir untersuchen und formalisieren diese Anforderungen und schlagen Lösungsstrategien vor.

When devices are integrated into service oriented architectures, specific requirements for security arise. We investigate and formalize these requirements and propose solutions.

Synthese von Verhaltensadaptern / Synthesis of Behavioral Adapters
gefördert durch / funded by:



Laufzeit: 2008-2010

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.

Bedienungsanleitungen / Operating guidelines
gefördert durch / funded by:



Laufzeit: 2007-2009

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.

Eine Theorie des Verhaltens von Services / A Theory of Service Behavior
gefördert durch / funded by:



Laufzeit: 2006-

Services dienen der schnellen und losen Kopplung von Komponenten über standardisierte Schnittstellen. Damit die Kopplung funktioniert, müssen die Semantik, das Verhalten und nichtfunktionale Aspekte der beteiligten Services kompatibel sein. Wir bilden Begriffe und studieren Verifikations- und Synthesemethoden, die das Verhalten (also die Abfolge der Kommunikation) zwischen Services betreffen. Resultate werden in Form von Werkzeugen bereitgestellt und anhand realistischer Fallstudien validiert.

Services are made for loosely coupling components using standardized interfaces. For compatibiltiy, semantical, behavioral, and non-functional requirements must be met. We develop concepts and develop methods which are devoted to the verification and synthesis of service behavior (i.e. the correct exchange of messages between services). Our results are made available through tools which are validated in realistic case studies.