Synopsis
I. Discrete Event System Verification.- 1. Overview of Verification.- 1.Bugs.- 1.1 Concurrency bugs.- 1.2 An example.- 1.3 A real-life concurrency bug.- 2.The Mathematical Approach.- 2.1 Easy objections.- 2.2 The real objection.- 3. A Selective History.- 3.1 Early 1960's.- 3.2 Late 1960's.- 3.3 1970's.- 3.4 Late 1960's.- 3.5 1980's.- 3.6 Late 1980's.- 3.7 1990's.- 2. General Purpose Theorem Proving Methods in the Verification of Digital Hardware and Software.- 1. Introduction.- 1.1 Formal models.- 1.2 Lessons.- 1.3 A spectrum of choices.- 1.4 Outline of this presentation.- 2. The ACL2 Theorem Prover.- 2.1 NQTHM: the Boyer-Moore System.- 2.2 A simple example of ACL2.- 2.3 A more interesting example.- 2.4 Five key ideas in ACL2.- 3. Using ACL2 to Model Digital Systems.- 4. Industrial Scale Applications of ACL2.- 4.1 AMD floating point arithmetic.- 4.2 Motorola CAP digital signal processor.- 4.3 Summary of ACL2 applications.- 5. Other General-Purpose Systems.- 5.1 HOL.- 5.2 PVS.- 6. Conclusion.- 3. Temporal Logic and Model Checking.- 1. Reactive Systems and Temporal Properties.- 1.1 Example: The alternating bit protocol.- 1.2 Temporal properties.- 1.3 Formalizing temporal properties.- 1.4 Model theory for temporal logic.- 1.5 Proofs in temporal logic.- 2. Model Checking (Clarke/Emerson, Queille/Sifakis).- 2.1 Example: Modeling a protocol in CSP (Hoare).- 3. Branching Time and CTL Model Checking.- 3.1 CTL model checking.- 3.2 Example: The ABP revisited.- 4. Expressiveness Issues.- 4.1 Linear vs. branching time.- 4.2 Data independence.- 5. Summary.- 4. Model Checking Using Automata Theory.- 1. ?-Automata.- 2. Specification Using ?-Automata.- 3. Operations on BÜchi Automata.- 4. Checking Emptiness.- 5. Other Acceptance Conditions.- 6. Translating LTL into Automata.- 6.1 Linear temporal logic.- 6.2 The translation algorithm.- 6.3 Improvements to the algorithm.- 7. The Expressive Power of BÜchi Automata.- 8. The Complexity of LTL Model Checking.- 5. Complexity Issues in Automata Theoretic Verification.- 1. Introduction.- 1.1 About u;-automata based verification.- 2. About the COSPAN Verification Tool.- 2.1 Introduction.- 2.2 Modeling hardware.- 2.3 Specification and proof.- 2.4 Handling the complexity theoretic lowerbounds.- 3. The Theoretical Foundations: Boolean Algebra, Languages, and Selection-Resolution.- 3.1 Boolean algebra, automata and languages.- 3.2 Some words about Boolean algebras.- 3.3 L-automaton and L-process.- 3.4 Selection/resolution model.- 3.5 Verification based on L-processes and L-automata.- 4. Reduction Methodologies.- 4.1 Homomorphic reduction and refinement based topdown methodology.- 4.2 Inductive abstraction.- 6. Symbolic Model Checking.- 1. Introduction.- 2. Binary Decision Diagrams.- 2.1 Apply algorithm.- 2.2 The quantification algorithm.- 2.3 Circuit width and OBDD size.- 2.4 Variable ordering.- 3. Representing Sets and Relations.- 3.1 Char acter ist ic functions of sets.- 3.2 Characteristic functions of relations.- 3.3 Forward and reverse image.- 3.4 Reachability analysis using OBDD's.- 4. Fixed Point Characterization of CTL.- 4.1 Fixed points of monotonic functions.- 4.2 Characterization of EG.- 4.3 Complexity of OBDD based model checking.- 5. The SMV System.- 5.1 SMV language.- 5.2 Example - a synchronous arbiter circuit.- 5.3 Example - distributed cache coherence protocol.- 6. The Mu-calculus and Symbolic Model Checking.- 6.1 Propositional mu-calculus.- 6.2 Mu-calculus and CTL.- 6.3 Relational mu-calculus and symbolic model checking.- 7. Summary.- 7. Compositional Systems and Methods.- 1. Introduction.- 2. A Framework for Compositional Minimization.- 2.1 Framework.- 2.2 An example framework.- 2.3 Application: Decoupled processor Controller.- 2.4 Hierarchical minimization.- 3. Assume/Guarantee Style Reasoning.- 3.1 Frameworkk.- 3.2 An example framework.- 3.3 Why not ordinary CTL?.- 3.4 Application example - CPU Controller revisitedn.- 4. Conclusion.- 8. Symmetry and Model Checking.- 1. Symmetr
Les informations fournies dans la section « Synopsis » peuvent faire référence à une autre édition de ce titre.
