Laufzeit: 2020 - 2022
In einem Zeitraum von zwei Jahren wird daran geforscht, das Syntheseproblem für immer größere Probleminstanzen zu beherrschen.
Durch Synthese eines Petrinetzes werden die in einer sequentiellen Systembeschreibung innewohnenden Möglichkeiten zur Parallelisierung aufgedeckt, die dann zur effizienten Implementierung genutzt werden können. Die Technologie kann zum Beispiel beim Entwurf asynchroner Schaltkreise verwendet werden.
Over two years, researchers will develop new algorithms for the Petri net synthesis problem that are able to solve larger problem instances.
Petri net synthesis reveals inherent parallelism in sequential system descriptions. This information may lead to more efficient implementations. The technology can be applied, among others, for the design of asynchronous circuits.
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.
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.
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.
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.
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.
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.
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.