Abschlussarbeiten

Offene Themen

Bereich Verifikation

Verteilte Algorithmen

Problemstellung Anwendungen und Organisation rechnergestützter Systeme sind zunehmend verteilt. Damit werden verteilte Algorithmen immer wichtiger. In dieser Arbeit modellieren Sie einen verteilten Algorithmus aus der Literatur mit Petrinetzen, Temporaler Logik, Abstract State Machines, Z oder einer anderen Spezifikationstechnik, beweisen seine wichtigsten Eigenschaften und vergleichen die gewählte Technik mit Alternativen.
Ziele - Modellierung eines verteilten Algorithmus mit einer Spezifikationstechnik
- Beweis von Eigenschaften
- Vergleich der gewählten Technik mit Alternativen
Voraussetzungen Teilnahme an mindestens einer der Vorlesungen Methoden und Modelle des Systementwurfs bzw. Verteilte Algorithmen
Beginn sofort
Ansprechpartner Prof. Dr. Wolfgang Reisig

Komposition von Petrinetzen

Problemstellung Große Systemmodelle werden systematisch durch Komposition kleinerer Modelle kkonstruiert. Für Petrinetz-Modelle braucht man deshalb geeignete Kompositions-Operationen. In der Literatur werden zahlreiche solche Operationen vorgestellt. Sie sind oft intuitiv einfach, aber formal doch vergleichsweise aufwendig.
Ziele Vor dem Hintergrund ganz neuer Vorschläge werden in dieser Diplomarbeit bekannte Konstruktionen neu bewertet, neu formuliert und aufeinander bezogen. Neue Varianten werden systematisch hergeleitet und untersucht.
Voraussetzungen Grundkenntnisse zu Petrinetzen, wie sie in den Vorlesungen „Methoden und Modelle des Systementwurfs“ und „Verteilte Algorithmen“ vermittelt werden.
Dieses Thema erfordert Interesse an guten, einfach verständlichen und dennoch präzisen formalen Darstellungen.
Beginn sofort
Ansprechpartner Prof. Dr. Wolfgang Reisig
Umfang/Rahmen eine Diplomarbeit

Abgeschlossene Arbeiten

    2015

  • Dewender, Johannes
    An Optimized Implementation for a Trace-Based Characterization of b-Bounded Responsiveness
    Diplomarbeit, may 2015
    close
  • Heiden, Simon
    Language-Based Characterization of Responsive Systems
    Diplomarbeit, feb 2015
    close
  • Triebel, Marvin
    Stabile Ungleichungen in Petrinetzen
    Diplomarbeit, jan 2015
    close

    2014

  • Dewender, Johannes
    Improving an Implementation for Deciding b-Conformance
    Studienarbeit, may 2014
    close
  • Heiden, Simon
    Ein Überblick über Programm- und Controller-Synthese
    Studienarbeit, mar 2014
    close

    2013

  • Misch, Sebastian

    Studienarbeit, dec 2013
    close
  • Schuh, Hannes
    Modellierung des lpSystems
    Studienarbeit, jul 2013
    close

  • Verteilung von Service-Adaptern
    Studienarbeit, jan 2013
    close
  • Völlinger, Kim
    Einsatz des Beweisassistenten Coq zur deduktiven Programmverifikation
    Diplomarbeit, aug 2013
    close

    2012

  • Ott, Janine

    Studienarbeit, jul 2012
    close
  • Kulagina, Svetlana
    A Survey on Automated Generation of Adapters for Web Services
    Studienarbeit, oct 2012
    close

    2011

  • Rohrmoser, Maxim
    Verteilende Transitionsverfeinerung
    Studienarbeit, nov 2011
    close
  • Schulz, Alexander
    Adaption szenario-basierter Modelle zur Laufzeit
    Diplomarbeit, apr 2011
    close

    2010

  • Prüfer, Robert
    Optimierung der Sweep-Line-Methode
    Diplomarbeit, apr 2010
    close
  • Müller, Richard
    Formal Characterisation of Partners of an Open Net
    Diplomarbeit, jun 2010
    close

    2009

  • Herzog, Mike
    Modellierung kommunizierender Systeme
    Studienarbeit, mar 2009
    close
  • Prüfer, Robert
    Optimierung der Sweeplinemethode
    Studienarbeit, mar 2009
    close
  • Sürmeli, Jan
    Strukturelle Analyse von Servicenetzen
    Diplomarbeit, feb 2009
    close
  • Müller, Richard
    Strukturelle Reduktion von Verhaltensadaptern
    Studienarbeit, dec 2009
    close

    2008


  • Synthese offener Workflownetze aus Serviceautomaten
    Diplomarbeit, jan 2008
    close
    close
  • Wolf, Manja

    Diplomarbeit, sep 2008
    close
    close
  • Swist, Konstanze
    Modellierung des Workflows der Task Force Erdbeben des GFZ mit Petrinetzen
    Studienarbeit, oct 2008
    close
  • Gierds, Christian
    Strukturelle Reduktion von Bedienungsanleitungen
    Diplomarbeit, jan 2008
    close
    close
  • Janusz, Daniel
    Implementierung zweier Algorithmen zur Abstraktion von Petrinetzen
    Studienarbeit, apr 2008
    close
  • Pillat, Thomas

    Diplomarbeit, mar 2008
    close
    close


  • Diplomarbeit, mar 2008
    close
    close
  • Bergmann, Rico
    Vergleich von Werkzeugen zur computergestützten Verifikation von Petrinetzmodellen
    Studienarbeit, jul 2008
    close
  • Liske, Nanette
    Laufzeitersetzung offener Workflownetze
    Diplomarbeit, jul 2008
    close

    2007

  • Wolf, Manja
    Synchrone und asynchrone Kommunikation in offenen Workflownetzen
    Studienarbeit, may 2007
    close
  • Bretschneider, Jan
    Produktbedienungsanleitungen zur Charakterisierung austauschbarer Services
    Diplomarbeit, mar 2007
    close
    close
  • Kleine, Jens
    Transformation von offenen Workflow-Netzen zu abstrakten WS-BPEL-Prozessen
    Diplomarbeit, jul 2007
    close
    close
  • Julius, Alexandra

    Diplomarbeit, may 2007
    close
    close
  • Liske, Nannette
    Laufzeitersetzbarkeit von Services
    Studienarbeit, apr 2007
    close
  • Kerlin, Andreas

    Diplomarbeit, jan 2007
    close
  • Gierds, Christian

    Studienarbeit, oct 2007
    close
    close
  • Schulz, Alexander
    Zielgerichtete Strategien
    Studienarbeit, jul 2007
    close

  • Strukturelle Analyse von offenen Workflow-Netzen hinsichtlich Bedienbarkeit
    Studienarbeit, jan 2007
    close
  • Laufer, Peter
    Public-View-Generierung
    Diplomarbeit, nov 2007
    close
    close

    2006

  • Kaschner, Kathrin
    BDD-basiertes Matching von Services
    Diplomarbeit, mar 2006
    close
    close
  • Laufer, Peter

    Studienarbeit, may 2006
    close
    close
  • Bretschneider, Jan
    Modellierung und Synthese eines geschwindigkeitsinvarianten GALS-Wrappers
    Studienarbeit, feb 2006
    close
    close
  • Kaschner, Kathrin
    Repräsentation von Bedienungsanleitungen durch BDDs
    Studienarbeit, jan 2006
    close
  • Fahland, Dirk
    Unfoldings for Timed Automata
    Diplomarbeit, July 2006
    In this thesis we develop a state space reduction technique for networks of timed automata based on unfoldings to alleviate the state space explosion problem due to concurrently enabled actions. For the purpose of verifying a system, standard model checking techniques construct its sequential state space that suffers an exponential growth when applied to distributed systems because of concurrently enabled, independent actions: during the construction of the state space these actions are ordered arbitrarily to simulate concurrency in the sequential model. For untimed systems, state space reduction techniques like stubborn sets that omit the construction of redundant information, and unfoldings that represent concurrent events in a partial order have successfully been applied to alleviate the exponential growth. These techniques apply a simple syntactical criterion to identify independent actions. This criterion is not applicable to networks of timed automata as simple examples show, which renders the existing techniques unapplicable. But networks of timed automata face the state space explosion problem as well which raises the demand for a specific reduction technique for these systems. In this thesis, we consider a special, but practically relevant class of networks of timed automata as a formal model for discrete, distributed, timed systems. We develop a novel technique that constructs a complete, finite representation of such a system's state space. This representation is the complete, finite prefix of an unfolding in which concurrently enabled actions are partially ordered. We show that this technique is capable of reducing the size of the state space by magnitude. We are presently not aware of any state space reduction technique for timed automata with similar results.
    close
    close
  • Kleine, Jens

    Studienarbeit, oct 2006
    close
    close

    2005

  • Lohmann, Niels

    Diplomarbeit, sep 2005
    close
    close
  • Salecker, Elke, Toussaint, Nora
    Gegenbeispielgesteuerte Abstraktionsverfeinerung in High-Level-Petrinetzen
    Diplomarbeit, sep 2005
    close
  • Julius, Alexandra
    Entwurf und VHDL-Modellierung von mesochronen GALS-Schaltungen
    Studienarbeit, dec 2005
    close
    close
  • Brade, Alexander

    Diplomarbeit, sep 2005
    close
    close
  • Frenkler, Carsten

    Diplomarbeit, jul 2005
    close
    close
  • Hinz, Sebastian

    Diplomarbeit, mar 2005
    close
    close
  • Glausch, Andreas
    Varianten des ASM-Theorems
    Diplomarbeit, jun 2005
    close
    close
  • Lohmann, Niels

    Studienarbeit, jun 2005
    close
    close
  • Brade, Alexander
    ASMs und die Struktur und Dynamik von Web Services
    Studienarbeit, jan 2005
    close

    2004

  • Fahland, Dirk
    Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines
    Studienarbeit, aug 2004
    close
    close
  • Weinberg, Daniela
    Analyse der Bedienbarkeit
    Diplomarbeit, oct 2004
    close
    close

  • Semantische Fundierung der Web-Service-Beschreibungssprache WSCI
    Diplomarbeit, nov 2004
    close
    close
  • Stahl, Christian
    Transformation von BPEL4WS in Petrinetze
    Diplomarbeit, apr 2004
    close
    close
  • Kuhtz, Lars
    TLDA und Petrinetze
    Studienarbeit, apr 2004
    close
  • Massuthe, Peter
    Verfeinerungstechniken der Temporal Logic of Distributed Actions TLDA
    Diplomarbeit, mar 2004
    close
    close
  • Gabriel, Yvonne
    Anbindung externer Werkzeuge an den Petrinetz-Kern am Beispiel des Integrated Net Analyser
    Studienarbeit, apr 2004
    close
  • Frenkler, Carsten

    Studienarbeit, feb 2004
    close

    2003

  • Massuthe, Peter
    Parallele Komposition in TLA
    Studienarbeit, sep 2003
    close
    close
  • Heidinger, Thomas
    Statische Analyse von BPEL4WS-Prozessmodellen
    Studienarbeit, dec 2003
    close
  • Weinberg, Daniela

    Studienarbeit, aug 2003
    close

  • Komposition von Web Services
    Studienarbeit, jun 2003
    close
    close
  • Hain, Dirk, Stahl, Christian
    Komposition von Web Services
    Studienarbeit, apr 2003
    close
    close
  • Glausch, Andreas
    Abstract-State Machines - Eine Sammlung didaktischer Beispiele
    Studienarbeit, feb 2003
    Diese Studienarbeit versucht durch eine Vielzahl von Beispielen den Begriff Abstract-State Machine und sequenzieller Algorithmus didaktisch sinnvoll darzustellen. Es werden dabei sowohl Beispiele als auch Gegenbeispiele angegeben, um Umfang und Grenzen dieser Begriffe aufzuzeigen.
    close
    close

    2002

  • Richter, Wolf

    Diplomarbeit, 2002
    close

    2001

  • Richter, Wolf
    Syntaktische Erkennung von Modellierungsfehlern in Web Services
    Studienarbeit, dec 2001
    close

    2000

  • Abdourahaman
    DAWN-ILF Tool. Modelchecking Anwendung
    Diplomarbeit, sep 2000
    close

    1999

  • Unger, S.

    Diplomarbeit, oct 1999
    close
  • Runge, D.

    Diplomarbeit, jun 1999
    close

    1998

  • Dehnert, Juliane, Schwenzer, Ines
    Dialogmodellierung mit Petrinetzen - Das FAN-Dialogmodell
    Diplomarbeit, aug 1998
    close

    1997

  • Martens, Axel
    Software-Engineering von Workflow-Applikationen mit Petrinetzen
    Diplomarbeit, aug 1997
    close

  • Arc-Typed-Petrinetze. Verifikation eines Datenbankmanagementsystems mit Datenreplikation
    Diplomarbeit, may 1997
    close
  • Weber, Michael
    unless-Aspekte und ihr Beitrag zur Verifikation von mit Petrinetzen modellierten Systemen
    Diplomarbeit, jan 1997
    close

    1996



  • Diplomarbeit, sep 1996
    close


  • Diplomarbeit, jul 1996
    close
  • Vesper, Tobias

    Diplomarbeit, mar 1996
    close