This textbook overviews the whole spectrum of formal methods and techniques that are aimed at verifying correctness of software, and how they can be used in practice. It focuses on techniques whereby the user has some control over the properties that are being checked. More specifically, it shows a wide range of techniques covering the whole spectrum: from abstract system design to implementation, from bug finding to full proofs, and from techniques that are push-button by design and give a yes/no answer to techniques that require the user to provide explicit guidance to steer the analysis process.
Topics and features:
- Covers a broad spectrum of software verification techniques, from model checking to annotation checking
- Provides numerous examples to demonstrate the techniques
- Focuses on how techniques can be used (and the main ideas behind how they work), as opposed to how they are implemented
- Explains strengths and weaknesses of the techniques, providing insight into when to use which technique in practice
This unique textbook has been written primarily for master’s level students in computer science studying embedded systems and specializing in software technology. The book will also be of interest for students studying cyber security and data science technology, as well as for system or software developers interested in techniques that offer formal guarantees about software.
Author(s): Marieke Huisman, Anton Wijs
Series: Texts in Computer Science
Edition: 1
Publisher: Springer
Year: 2023
Language: English
Commentary: Publisher PDF
Pages: 257
City: Cham
Tags: Software; Verification; Number Theory; Logic; System Validation; Systems Modelling; Specification
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
