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

Date

May 10, 2011

Time

1:00 PM - 2:00 PM

Speaker

Dipl.-Inf. Sascha Klüppelholz

Affiliation

Institut für Theoretische Informatik, Algebraische und logische Grundlagen der Informatik

Language

en

Main Topic

Informatik

Other Topics

Informatik

Description

Betreuer: Prof. Dr. rer. nat. C. Baier; Fachreferent: Prof. Dr.-Ing. habil. H. Vogler Information and communication systems enter an increasing number of areas of daily life. Our reliance and dependence on the functioning of such systems is rapidly growing together with the costs/impact of system failures. At the same time the complexity of hardware and software systems extends to new limits. These two tides/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. Modeling formalism, such as the channel-based exogenous coordination language Reo, support hierarchical modeling in an iterative top-down refinement procedure which is similar to the refinement that is part of any design phase for complex systems. They facilitate reusability, exchangeability, and heterogeneity of components and form the basis to apply formal verification methods. The goal of this thesis is to combine and adapt well known techniques for modeling and verification, and especially model checking of temporal logic formulas, to exogenous coordination models and to develop a holistic approach suitable for compositional modeling of and reasoning about complex system behaviour. The talk provides an overview on the most relevant research that has been done in the area of coordination languages and formal verification and presents an idea of an holistic approach to verify properties such as safety, liveness, controllability, and realizability.

Last modified: May 3, 2011, 9:35:34 AM