Verification of Reactive Systems

Formal Methods and Algorithms

Paperback Engels 2010 9783642055553
Verwachte levertijd ongeveer 9 werkdagen

Samenvatting

This book is a solid foundation of the most important formalisms used for specification and verification of reactive systems. In particular, the text presents all important results on m-calculus, w-automata, and temporal logics, shows the relationships between these formalisms and describes state-of-the-art verification procedures for them. It also discusses advantages and disadvantages of these formalisms, and shows up their strengths and weaknesses. Most results are given with detailed proofs, so that the presentation is almost self-contained.

Includes all definitions without relying on other material

Proves all theorems in detail

Presents detailed algorithms in pseudo-code for verification as well as translations to other formalisms

Specificaties

ISBN13:9783642055553
Taal:Engels
Bindwijze:paperback
Aantal pagina's:602
Uitgever:Springer Berlin Heidelberg
Druk:0

Lezersrecensies

Wees de eerste die een lezersrecensie schrijft!

Inhoudsopgave

1 Introduction.- 2 A Unified Specification Language.- 3 Fixpoint Calculi.- 4 Finite Automata.- 5 Temporal Logics.- 6 Predicate Logic.- 7 Conclusions.- A Binary Decision Diagrams.- A.1 Basic Definitions.- A.2 Basic Algorithms on BDDs.- A.3 Minimization of BDDs Using Care Sets.- A.4 Computing Successors and Predecessors.- A.5 Variable Reordering.- A.6 Final Remarks.- B.1 A Partial Local Model Checking Procedure.- B.2 A Complete Local Model Checking Procedure.- C Reduction of Structures.- C.1 Galois Connections and Simulations.- C.1.1 Basic Properties of Galois Connections.- C.1.2 Galois Simulation.- C.2 Abstract Structures and Preservation Results.- C.3 Optimal and Faithful Abstractions.- C.4 Data Abstraction.- C.4.1 Abstract Interpretation of Structures.- C.4.2 Abstract Specifications.- C.5 Symmetry and Model Checking.- C.5.1 Symmetries of Structures.- C.5.2 Symmetries in the Specification.- References.

Managementboek Top 100

Rubrieken

    Personen

      Trefwoorden

        Verification of Reactive Systems