Concise Guide to Software Verification : From Model Checking to Annotation Checking

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. Formal methods employ a variety of theoretical computer science fundamentals, including logic calculi, formal languages, automata theory, control theory, program semantics, type systems, and type theory. This book gives an overview of a range of techniques, captured by this term formal methods, that are aimed at the analysis of software, and it describes how these techniques can be used to improve the reliability and robustness of software. Formal methods for the analysis of hardware are not in the scope of this book. When we refer to formal methods in this book, we implicitly rule out techniques aimed specifically at hardware analysis. In this book, our aim is to give an overview of this whole spectrum of formal methods and techniques, and how they can be used in practice. We focus in particular on techniques where the user has some control over the properties that are being checked. We show how we have a wide range of techniques available that cover the whole spectrum from abstract system design to implementation, from bug finding to full proofs, and from techniques that are push-button and give a yes/no answer, to techniques that require the user to provide explicit guidance to steer the analysis process. 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 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.