• search hit 4315 of 4395
Back to Result List

Symbolische LTL-Verifikation von Petrinetzen

  • Diese Arbeit widmet sich der Verifikation nebenläufiger Systeme unter Verwendung von Modelcheckingverfahren. Es wurden Modelcheckingverfahren betrachtet und entwickelt, welche die drei Gebiete: Petrinetze als Modellierungssprache, linear-time temporale Logik zur Spezifikation von Systemeigenschaften und binäre Entscheidungsgraphen zur Repräsentation großer Zustandsmengen verbinden. Bei der Entwicklung von Modelcheckingverfahren wurde darauf geachtet, dass durch die Kombination der einzelnen Gebiete deren Vorteile erhalten bleiben und die sich zwischen den Gebieten ergebendnen Synergien ausgenutzt werden. Den wesentlichen innovativen Teil der Arbeit stellt die Entwicklung eines LTL-Modelcheckingverfahrens dar, welches eine symbolische Repräsentierung der Zustände mit einem on-the-fly Verifikationsverfahren verbindet und dabei eine zeitliche Komplexität der klassischen LTL-Modelcheckingverfahren erreicht.
  • This thesis is devoted to studying the problem of verifying parallel systems using a model checking approach. We have looked at and developed model checking approaches, which combine the three topics: Petri nets as a modelling language, linear-time temporal logic to capture system properties, and binary decision diagrams to represent huge state spaces. During the development of the model checking approaches we especially have focused on keeping the advantages of the different areas and on achieving benefits by combining them.The major contribution of the thesis is the development of a LTL-based model checking approach, which combines the symbolic representation of reachable states with an on-the-fly model checking approach by having the same time complexity of the classical LTL-based model checking approaches.

Download full text files

Export metadata

Additional Services

Search Google Scholar Stastistics
Metadaten
Author: Jochen Spranger
URN:urn:nbn:de:kobv:co1-000000179
Referee / Advisor:Prof. Dr. Monika Heiner
Document Type:Doctoral thesis
Language:German
Year of Completion:2001
Date of final exam:2001/12/07
Release Date:2007/03/06
Tag:Modelchecking; Nebenläufiges System; Petrinetz; Stelle/Transitionsnetz; Verifikation
GND Keyword:Komplexes System ; Nebenläufigkeit; Petri-Netz; Spezifikationssprache; Model checking; Temporale Logik
Institutes:Fakultät 1 MINT - Mathematik, Informatik, Physik, Elektro- und Informationstechnik / FG Datenstrukturen und Softwarezuverlässigkeit
Institution name at the time of publication:Fakultät für Mathematik, Naturwissenschaften und Informatik (eBTU) / LS Informatik / Datenstrukturen und Softwarezuverlässigkeit
Einverstanden ✔
Diese Webseite verwendet technisch erforderliche Session-Cookies. Durch die weitere Nutzung der Webseite stimmen Sie diesem zu. Unsere Datenschutzerklärung finden Sie hier.