Verification of Branching-Time and Alternating-Time Properties for Exogenous Coordination Models

Sascha KlüppelholzSascha Klüppelholz

Sascha Klüppelholz
Verification of Branching-Time and Alternating-Time Properties for Exogenous Coordination Models
Phd thesis

Details
Bibtex

KurzfassungAbstract
Information and communication systems enter an increasing number of areas of daily lives. Our reliance and dependence on the functioning of such systems is rapidly growing together with the costs and the impact of system failures. At the same time the complexity of hardware and software systems extends to new limits as modern hardware architectures become more and more parallel, dynamic and heterogenous. These trends demand for a closer integration of formal methods and system engineering to show the correctness of complex systems within the design phase of large projects. The goal of this thesis is to introduce a formal holistic approach for modeling, analysis and synthesis of parallel systems that potentially addresses complex system behavior at any layer of the hardware/software stack. Due to the complexity of modern hardware and software systems, we aim to have a hierarchical modeling framework that allows to specify the behavior of a parallel system at various levels of abstraction and that facilitates designing complex systems in an iterative refinement procedure, in which more detailed behavior is added successively to the system description. In this context, the major challenge is to provide modeling formalisms that are expressive enough to address all of the above issues and are at the same time amenable to the application of formal methods for proving that the system behavior conforms to its specification. Our focus in this thesis will be on model checking which yields an algorithmic approach to show the correctness of a system with respect to its specification. For the modeling, we are interested in specification formalisms that allow to apply formal verification techniques such that the underlying model checking problems are still decidable within reasonable time and space bounds.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@phdthesis{K2025,
  author = {Sascha Kl{\"{u}}ppelholz},
  title  = {Verification of Branching-Time and Alternating-Time Properties for
            Exogenous Coordination Models},
  year   = {2025}
}