دانلود کتاب Concise Guide to Software Verification. From Model Checking to Annotation Checking

فهرست مطالب :

Contents
1 Introduction
2 First-Order Logic and Set Theory
2.1 Booleans
2.2 Propositional Logic
2.3 First-Order Logic
2.4 Set Theory
2.5 Functions and Relations
3 System Modelling
3.1 History and Background
3.2 Finite State Machines
3.3 Finite State Machines in NUSMV
3.3.1 Defining NUSMV Modules
3.3.2 Composition of Multiple Modules
3.4 Finite State Machines in PROMELA
3.4.1 Defining PROMELA Processes
3.4.2 Composition of Multiple Processes
3.5 Kripke Structures
3.6 A Modelling Case Study—An Elevator System
3.7 Further Reading
4 Functional System Properties in Temporal Logic
4.1 History and Background
4.2 Safety Versus Liveness Properties
4.3 Kripke Structures
4.4 Linear Temporal Logic—Syntax and Semantics
4.5 Fairness
4.6 Fairness as an LTL Formula
4.7 Computation Tree Logic—Syntax and Semantics
4.8 Fairness as a CTL Formula?
4.9 Comparison of LTL and CTL
4.10 Further Reading
5 Model Checking Algorithms
5.1 CTL Model Checking in NUSMV
5.2 CTL Model Checking in NUSMV Under Fairness
5.3 Tableau-Based LTL Model Checking in NUSMV
5.4 Checking Safety Properties in SPIN
5.5 Automata-Based LTL Model Checking in SPIN
5.6 Further Reading
6 Analysing Software
6.1 The Relation Between Code and Model
6.1.1 Encoding a Program in NUSMV
6.1.2 Challenges for Software Model Checking
6.1.3 Software Analysis Approaches
6.2 Runtime Monitoring of Software
6.2.1 Implementation of LARVA
6.2.2 Monitor Specifications in LARVA
6.2.3 From Temporal Logic Formula to LARVA Automata
6.3 Bounded Model Checking Using CBMC
6.3.1 SAT-Based Bounded Model Checking of Safety Properties
6.3.2 Unrolling the Transition Relation in CBMC
6.3.3 Properties in CBMC
6.3.4 Modular Verification with CBMC
6.3.5 Further Reading
6.4 Bounded Symbolic Execution Using CIVL
6.4.1 Symbolic Execution
6.4.2 Bounded Symbolic Execution
6.4.3 CIVL Details
6.5 Counter-Example-Guided Abstraction-Refinement
6.5.1 Abstraction
6.5.2 Repeated Abstraction and Refinement with CEGAR
6.5.3 Non-Termination of CEGAR
6.5.4 Other Approaches Using Abstraction and Refinement
6.6 Automatic Test Suite Generation Using CBMC
6.6.1 Further Reading
7 Design by Contract Specification Languages
7.1 History and Background
7.2 Function Contracts
7.2.1 Ingredients of a Function Contract
7.2.2 Behaviours
7.2.3 Various Details on Function Contracts
7.3 Data Specifications
7.4 Multiple Function Behaviours
7.5 Inheritance of Method Specifications in JML
7.6 Specifying Exceptional Behaviour in JML
7.7 Conclusions
8 Abstract Specifications
8.1 Using Functions in Contracts
8.2 Model Variables
8.2.1 Model Variables and Interfaces
8.2.2 Model Variables for Mathematical Abstraction
8.3 Ghost Variables
8.4 Model Versus Ghost Variables
9 Runtime Annotation Checking
9.1 History and Background
9.2 Manually Validating Specifications
9.3 Requirements for a Runtime Annotation Checker
9.4 Executing a Runtime Annotation Checker
9.5 Monitoring Behavioural Properties
9.6 Further Reading
10 Static Annotation Checking
10.1 History and Background
10.2 Hoare Logic and Weakest Preconditions
10.3 Reasoning About Function Calls
10.4 Statement Annotations—Helping the Verifier
10.5 Termination
10.6 Further Reading
Appendix References
Appendix Index