Muutke küpsiste eelistusi

E-raamat: Verification of Reactive Systems: Formal Methods and Algorithms

3.50/5 (2 hinnangut Goodreads-ist)
Teised raamatud teemal:
  • Formaat - PDF+DRM
  • Hind: 55,56 €*
  • * hind on lõplik, st. muud allahindlused enam ei rakendu
  • Lisa ostukorvi
  • Lisa soovinimekirja
  • See e-raamat on mõeldud ainult isiklikuks kasutamiseks. E-raamatuid ei saa tagastada.
Verification of Reactive Systems: Formal Methods and AlgorithmsSuurem pilt
Teised raamatud teemal:

DRM piirangud

  • Kopeerimine (copy/paste):

    ei ole lubatud

  • Printimine:

    ei ole lubatud

  • Kasutamine:

    Digitaalõiguste kaitse (DRM)
    Kirjastus on väljastanud selle e-raamatu krüpteeritud kujul, mis tähendab, et selle lugemiseks peate installeerima spetsiaalse tarkvara. Samuti peate looma endale  Adobe ID Rohkem infot siin. E-raamatut saab lugeda 1 kasutaja ning alla laadida kuni 6'de seadmesse (kõik autoriseeritud sama Adobe ID-ga).

    Vajalik tarkvara
    Mobiilsetes seadmetes (telefon või tahvelarvuti) lugemiseks peate installeerima selle tasuta rakenduse: PocketBook Reader (iOS / Android)

    PC või Mac seadmes lugemiseks peate installima Adobe Digital Editionsi (Seeon tasuta rakendus spetsiaalselt e-raamatute lugemiseks. Seda ei tohi segamini ajada Adober Reader'iga, mis tõenäoliselt on juba teie arvutisse installeeritud )

    Seda e-raamatut ei saa lugeda Amazon Kindle's. 

Reactive systems are becoming more and more important for essentially all areas of technical and professional activities as well as for many areas of everyday life. The design of these systems is a great challenge and requires sound compromises between safety and time-to-market. To meet these needs, early design phases nowadays include verification of given specifications against system descriptions to find potential design errors as early as possible. This book is devoted to the foundation of the most popular formal methods for the specification and verification of reactive systems. In particular, the µ-calculus, omega-automata, and temporal logics are covered in full detail; their relationship and state-of-the-art verification procedures based on these formal approaches are presented. Furthermore, the advantages and disadvantages of the formalisms from particular points of view are analyzed. Most results are given with detailed proofs, so that the presentation is almost self-contained.



This book is targeted to advanced students, lecturers and researchers in the area of formal methods.

Arvustused

From the reviews:









"The book starts with an introduction to formal methods in system design, talking about taxonomy and a classification of formal methods and systems. Then the author introduces what he calls a unified specification language, which is propositional µ-calculus based on Kripke structure simulation, bisimulation and also quotient structures and products of Kripke structures. it is a very helpful book that can be used both as a basis for a lecturer and as a handbook for learning about verification issues." (Manfred Broy, Mathematical Reviews, 2006 d)



"Verification of Reactive Systems deals very much with the fundamental theory of its subject matter, namely automata, temporal logic, and model checking. is focused systematic, and thorough. This makes it very suitable for a graduate course on selected topics on formal methods. It would also be highly useful as a general reference in logic and automata theory . is a remarkable achievement, and fills, in book-form, a glaring gap in the literature. I heartily recommend it to every serious formal methods theoretician. (Joel Ouaknine, Software Testing, Verification and Reliability, Vol. 15 (3), 2005)



"This book is in the series on theoretical computer science. The book classifies systems into transformational systems, interactive systems, and reactive systems. can be kept as a reference for theories on verification of computing systems, especially finite state formalisms. The book is complete with respect to its concepts, and explanations. The research oriented readers can find the book useful . For theory oriented readers, the flow of chapters is smooth. On the whole, the book is well written ." (Maulik A. Dave, SIGACT News, Vol. 37 (4), 2006)

Muu info

Springer Book Archives
1 Introduction
1(44)
1.1 Formal Methods in System Design
1(15)
1.1.1 General Remarks and Taxonomy
1(3)
1.1.2 Classification of Formal Methods
4(6)
1.1.3 Classification of Systems
10(6)
1.2 Genealogy of Formal Verification
16(24)
1.2.1 Early Beginnings of Mathematical Logic
16(4)
1.2.2 Automated Theorem Proving
20(3)
1.2.3 Beginnings of Program Verification
23(1)
1.2.4 Dynamic Logics and Fixpoint Calculi
24(4)
1.2.5 Temporal Logics
28(5)
1.2.6 Decidable Theories and w-Automata
33(5)
1.2.7 Summary
38(2)
1.3 Outline of the Book
40(5)
2 A Unified Specification Language
45(44)
2.1 Kripke Structures as Formal Models of Reactive Systems
45(23)
2.1.1 Simulation and Bisimulation of Kripke Structures
53(8)
2.1.2 Quotient Structures
61(5)
2.1.3 Products of Kripke Structures
66(2)
2.2 Syntax of the Specification Logic spec
68(9)
2.3 Semantics of the Specification Logic spec
77(7)
2.4 Normal Forms
84(5)
3 Fixpoint Calculi
89(94)
3.1 Partial Orders, Lattices and Fixpoints
90(8)
3.2 The Basic μ-Calculus
98(5)
3.3 Monotonicity of State Transformers
103(5)
3.4 Model Checking of the Basic μ-Calculus
108(10)
3.4.1 A Naive Model Checking Procedure
108(3)
3.4.2 Optimization by the Alternation Depth
111(7)
3.5 Vectorized μ-Calculus
118(41)
3.5.1 State Transformers of Vectorized Fixpoint Expressions
119(5)
3.5.2 Decomposing Equation Systems
124(5)
3.5.3 Model Checking Vectorized Fixpoint Expressions
129(9)
3.5.4 Comparing Basic and Vectorized μ-Calculus Model Checking
138(4)
3.5.5 Dependency-Triggered Evaluations
142(6)
3.5.6 The Cleaveland-Steffen Algorithm
148(11)
3.6 Reducing the Alternation Depth w.r.t. Structures
159(5)
3.7 Computing Fair States
164(5)
3.8 Final Remarks on Completeness and Expressiveness
169(14)
3.8.1 Bisimilarity and the Future Fragment
169(4)
3.8.2 Relationship to w-Tree Automata and Games
173(2)
3.8.3 Dynamic Logic
175(8)
4 Finite Automata
183(96)
4.1 Regular Languages, Regular Expressions and Automata
186(3)
4.2 The Logic of Automaton Formulas
189(5)
4.3 Boolean Closure
194(8)
4.4 Converting Automaton Classes
202(7)
4.5 Determinization and Complementation
209(27)
4.5.1 The Rabin-Scott Subset Construction
210(3)
4.5.2 Determinization of NDetF
213(2)
4.5.3 Determinization of NDetG
215(4)
4.5.4 Determinization of NDetFG
219(4)
4.5.5 Reducing NDetGF to DetRabin
223(13)
4.6 The Hierarchy of w-Automata and the Borel Hierarchy
236(16)
4.7 Automata and Monoids
252(12)
4.7.1 Finite Semigroups and Monoids
252(5)
4.7.2 Automata and Their Monoids
257(7)
4.8 Decision Procedures for w-Automata
264(15)
4.8.1 Flattening w-Automata
265(2)
4.8.2 Translating w Model Checking to μ Model Checking
267(3)
4.8.3 Translating Automata to Vectorized μ-Calculus
270(9)
5 Temporal Logics
279(126)
5.1 Introduction
279(5)
5.2 Branching Time Logics -- Sublanguages of CTL*
284(15)
5.2.1 CTL, LTL and CTL*
285(7)
5.2.2 Adding Syntactic Sugar to CTL
292(7)
5.3 Translating Temporal Logics to the μ-Calculus
299(30)
5.3.1 CTL and FairCTL as Fragments of the μ-Calculus
300(2)
5.3.2 CTL2 as a Fragment of the μ-Calculus
302(2)
5.3.3 Eliminating Quantified Boolean Expressions
304(6)
5.3.4 Adding Path Quantifiers
310(3)
5.3.5 Translating LeftCTL* to Vectorized μ-Calculus
313(16)
5.4 Translating Temporal Logics to w-Automata
329(46)
5.4.1 The Basic Translation from LTLp to NDetStreett
331(12)
5.4.2 Exploitation of Monotonicity
343(5)
5.4.3 Borel Classes of Temporal Logic
348(7)
5.4.4 Reducing Temporal Borel Classes to Borel Automata
355(10)
5.4.5 Reductions to CTL/LeftCTL* Model Checking
365(10)
5.5 Completeness and Expressiveness of Temporal Logic
375(18)
5.5.1 Noncounting Automata and Temporal Logic
376(7)
5.5.2 Completeness of the Borel Classes
383(4)
5.5.3 Completeness of the Future Fragments
387(6)
5.6 Complexities of the Model Checking Problems
393(7)
5.7 Reductions by Simulation and Bisimulation Relations
400(5)
6 Predicate Logic
405(50)
6.1 Introduction
405(3)
6.2 Predicate Logics
408(20)
6.2.1 Syntax and Semantics
408(2)
6.2.2 Basics of Predicate Logic
410(5)
6.2.3 Fragments with Decidable Satisfiability Problem
415(6)
6.2.4 Embedding Modal Logics in Predicate Logic
421(3)
6.2.5 Predicate Logic on Linearly Ordered Domains (on N)
424(4)
6.3 Monadic Second Order Logic of Linear Order MSO<
428(14)
6.3.1 Equivalence of SIS and MSO<
428(6)
6.3.2 Translating MSO< to w-Automata
434(5)
6.3.3 Buchi's Decision Procedure: Normal Forms for S1S
439(3)
6.4 Monadic First Order Logic of Linear Order MFO<
442(10)
6.5 Non-Monadic Characterizations
452(3)
7 Conclusions
455(4)
A Binary Decision Diagrams
459(28)
A.1 Basic Definitions
459(7)
A.2 Basic Algorithms on BDDs
466(5)
A.3 Minimization of BDDs Using Care Sets
471(6)
A.4 Computing Successors and Predecessors
477(6)
A.5 Variable Reordering
483(3)
A.6 Final Remarks
486(1)
B Local Model Checking and Satisfiability Checking for the μ-Calculus
487(40)
B.1 A Partial Local Model Checking Procedure
488(5)
B.2 A Complete Local Model Checking Procedure
493(7)
B.3 Satisfiability of μ-Calculus Formulas
500(27)
C Reduction of Structures
527(34)
C.1 Galois Connections and Simulations
527(7)
C.1.1 Basic Properties of Galois Connections
528(3)
C.1.2 Galois Simulation
531(3)
C.2 Abstract Structures and Preservation Results
534(3)
C.3 Optimal and Faithful Abstractions
537(5)
C.4 Data Abstraction
542(9)
C.4.1 Abstract Interpretation of Structures
544(5)
C.4.2 Abstract Specifications
549(2)
C.5 Symmetry and Model Checking
551(10)
C.5.1 Symmetries of Structures
552(5)
C.5.2 Symmetries in the Specification
557(4)
References 561(30)
Index 591
Klaus Schneider is working since 10 years on the specification and verification of reactive systems. Starting as a research assistant in 1992 at the university of Karlsruhe, he worked on the verification of hardware circuits with higher order logic theorem provers. After receiving his PhD in 1996, he focused his research topics on design, specification, and verification of reactive systems. His research group made a lot of important contributions to still active research areas. The book is based on his habilitation in 2001. Since 2002, the author is professor in computer science at the university of Kaiserslautern.
Lisainfo e-raamatute kohta Lisainfo e-raamatute kohta
Püsilink: https://www.kriso.ee/db/97836621077822e.html
Märksõnad: