In this thesis, we show how to specify and verify safety as well as secrecy in workflow systems with arbitrarily many participating agents. We rely on First-order Transition Systems as a formal model and formalize their properties in First-order HyperLTL. We provide approaches to automatically verify rich classes of First-order transition systems and prove the problem undecidable for the general case. Beyond verification, we extend our algorithms to synthesis questions on First-order Safety Games.
«
In this thesis, we show how to specify and verify safety as well as secrecy in workflow systems with arbitrarily many participating agents. We rely on First-order Transition Systems as a formal model and formalize their properties in First-order HyperLTL. We provide approaches to automatically verify rich classes of First-order transition systems and prove the problem undecidable for the general case. Beyond verification, we extend our algorithms to synthesis questions on First-order Safety Game...
»
Übersetzte Kurzfassung:
Wir modellieren Sicherheits- sowie Geheimhaltungseigenschaften von Workflow-Systemen mit einer unbeschränkten Anzahl von beteiligten Agenten. Als formales Modell nutzen wir prädikatenlogische Transitionssysteme und formalisieren deren Eigenschaften in First-order HyperLTL. Wir entwickeln Methoden um Klassen von Transitionssystemen vollautomatisch zu verifizieren und zeigen Unentscheidbarkeit für Systeme ausserhalb dieser Klassen. Darüber hinaus entwickeln wir Synthese-methoden für prädikatenlogische Systeme.
«
Wir modellieren Sicherheits- sowie Geheimhaltungseigenschaften von Workflow-Systemen mit einer unbeschränkten Anzahl von beteiligten Agenten. Als formales Modell nutzen wir prädikatenlogische Transitionssysteme und formalisieren deren Eigenschaften in First-order HyperLTL. Wir entwickeln Methoden um Klassen von Transitionssystemen vollautomatisch zu verifizieren und zeigen Unentscheidbarkeit für Systeme ausserhalb dieser Klassen. Darüber hinaus entwickeln wir Synthese-methoden für prädikatenlogi...
»