Options
2005
Doctoral Thesis
Titel
Formal specification and verification. Structures and techniques
Abstract
This thesis is about mathematical structures and techniques related to formal specification and verification. We mainly focus on structures and techniques related to both concurrent systems and formal semantics of specification languages. We provide an abstract unifying framework for various different models of transition systems such as unlabeled transition systems, labeled transition systems, algebraic transition systems, and concurrent transition systems. An abstract simulation theory based on forward and backward simulation relations is defined and correctness proof are given. Concurrent transition systems are defined as an abstract model for concurrency. Sufficient conditions are derived that guarantee a global, partially ordered causality relation associated with concurrent transition systems. We analyze the notion of calculus and its associated proof principle 'calculus closure induction'. The relations between calculi and algebraic closure operators, compact derivation relations and algebras are analyzed. We define a temporal logic and an abstract refinement concept for new and generic models for concurrency called concurrent runs. A formal definition of ASMs embedded into the proposed framework as special algebraic transition systems is given. Case studies provide applications of both the introduced temporal logic and the refinement concept. The formal semantics of SDL-2000 approved by the ITU in November 2000 is illustrated.
ThesisNote
Zugl.: Kaiserslautern, TU, Diss., 2005