Forschungsbereich ComputergestĂŒtzte Verifikation / Research Area Computer Aided Verification

 

 

gefördert durch / funded by: 2006-

 

Zustandsraumverifikation / State Space Verification

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 Booelscher 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 Booelan programs.

Nach oben

 

gefördert durch / funded by: 2009-2011

Strukturelle Analysetechniken fĂŒr Petrinetze / Structural Verification Techniques for Petri Nets

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.

Nach oben

gefördert durch: 2012-2014

 

Verifikationstechniken fĂŒr Petrinetze auf Multicore-Architekturen / Verification Techniques for Petri Nets on Multicore Architectures

 

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.

Forschungsbereich Algorithmen fĂŒr Services / Research Area Algorithms for Services

 

 

gefördert durch / funded by: 2006-

 

Eine Theorie des Verhaltens von Services / A Theory of Service Behavior

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.

Nach oben

 

gefördert durch / funded by: 2007-2009

Bedienungsanleitungen / Operating guidelines

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.

Nach oben

 

gefördert durch / funded by: 2008-2010

Synthese von Verhaltensadaptern / Synthesis of Behavioral Adapters

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.

Nach oben

 

gefördert durch / funded by: 2010-2012

ZuverlĂ€ssig sichere Web Services fĂŒr GerĂ€te / Reliably Secure Web Services for Devices

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.

Nach oben