Formal Methods for Software Engineering: Languages, Methods, Application Domains

✍ Scribed by Markus Roggenbach; Antonio Cerone; Bernd-Holger Schlingloff; Gerardo Schneider; Siraj Ahmed Shaikh

• Publisher: Springer Nature
• Year: 2022
• Tongue: English
• Leaves: 538
• Series: Texts in Theoretical Computer Science
• Category: Library

✦ Synopsis

Software programs are formal entities with precise meanings independent of their programmers, so the transition from ideas to programs necessarily involves a formalisation at some point. The first part of this graduate-level introduction to formal methods develops an understanding of what constitutes formal methods and what their place is in Software Engineering. It also introduces logics as languages to describe reasoning and the process algebra CSP as a language to represent behaviours. The second part offers specification and testing methods for formal development of software, based on the modelling languages CASL and UML. The third part takes the reader into the application domains of normative documents, human machine interfaces, and security. Use of notations and formalisms is uniform throughout the book. Topics and features: Explains foundations, and introduces specification, verification, and testing methods Explores various application domains Presents realistic and practical examples, illustrating concepts Brings together contributions from highly experienced educators and researchers Offers modelling and analysis methods for formal development of software Suitable for graduate and undergraduate courses in software engineering, this uniquely practical textbook will also be of value to students in informatics, as well as to scientists and practical engineers, who want to learn about or work more effectively with formal theories and methods. Markus Roggenbach is a Professor in the Dept. of Computer Science of Swansea University. Antonio Cerone is an Associate Professor in the Dept. of Computer Science of Nazarbayev University, Nur-Sultan. Bernd-Holger Schlingloff is a Professor in the Institut für Informatik of Humboldt-Universität zu Berlin. Gerardo Schneider is a Professor in the Dept. of Computer Science and Engineering of University of Gothenburg. Siraj Ahmed Shaikh is a Professor in the Institute for Future Transport and Cities of Coventry University. The companion site for the book offers additional resources, including further material for selected chapters, prepared lab classes, a list of errata, slides and teaching material, and virtual machines with preinstalled tools and resources for hands-on experience with examples from the book. The URL is: https://sefm-book.github.io

✦ Table of Contents

Foreword by Manfred Broy
Preface
Audience, Prerequisites, and Chapter Dependencies
Book Use and Online Supporting Materials
Book History
Author Team
Acknowledgments
Contents
Contributors
List of Examples
Formal Methods
1.1 What Is a Formal Method?
1.1.1 An Application in Space Technologies
1.1.2 An Everyday Application
1.2 Formal Methods in Software Development
1.2.1 The Software Life Cycle
1.2.2 Formal Methods: When and Where
1.2.3 A Classification Scheme for Formal Methods
1.2.4 Tool Support for Formal Methods
1.3 Formal Methods in Practice
1.3.1 Comparative Surveys and Case Studies
1.3.2 Industrial Practice
1.3.3 How to Get Started
1.4 Closing Remarks
1.4.1 Current Research Directions
References
Part I Languages
Logics for Software Engineering
2.1 Logic in Computer Science
2.2 Propositional Logic—An Archetypical Modelling Language
2.2.1 Example: Car Configuration
2.2.2 Syntax and Semantics of Propositional Logic
2.2.3 Propositional Methods
2.3 A Framework for Logics
2.3.1 Specification
2.4 First- and Second-Order Logic
2.4.1 FOL
2.4.2 Second-Order Logic
2.4.3 The Logic of Casl
2.5 Non-Classical Logics
2.5.1 Modal and Multimodal Logics
2.5.2 Deontic Logic
2.5.3 Temporal Logic
2.6 Closing Remarks
2.6.1 Annotated Bibliography
2.6.2 Current Research Directions
References
The Process Algebra CSP
3.1 Introduction
3.2 Learning Csp
3.2.1 ATM Example: Csp Syntax
3.2.2 Understanding the Semantics—Modelling a Jet Engine Controller
3.2.3 Understanding Refinement—Modelling Buffers
3.3 The Children's Puzzle or What Csp Tools Can Do
3.3.1 The Arithmetic Side of the Puzzle
3.3.2 An Asynchronous Model of the Puzzle in Csp
3.3.3 Analysing the Csp Model with Tool Support
3.3.4 A Transformational Approach to Implementation
3.4 Semantics and Analysis
3.4.1 The Three Standard Models
3.4.2 Algebraic Laws
3.4.3 Foundations: Fixed Points
3.4.4 Checking for General Global Properties
3.5 Closing Remarks
3.5.1 Annotated Bibliography
3.5.2 Current Research Directions
References
Part II Methods
Algebraic Specification in CASL
4.1 Introduction
4.2 A First Example: Modelling, Validating, Consistency Checking, and Testing a Telephone Database
4.2.1 Modelling
4.2.2 Validating
4.2.3 Consistency Checking
4.2.4 Testing Java Implementations
4.2.5 The Story so Far
4.3 Verification of Ladder Logic Programs
4.3.1 Programmable Logic Controllers (PLCs)
4.3.2 Ladder Logic
4.3.3 The Automaton of a Ladder Logic Formula
4.3.4 Inductive Verification of Ladder Logic Programs
4.4 Structuring Specifications
4.4.1 Extension
4.4.2 Union
4.4.3 Renaming
4.4.4 Libraries
4.4.5 Parameterisation and Instantiation
4.4.6 Hiding
4.5 Closing Remarks
4.5.1 Annotated Bibliography
4.5.2 Current Research Directions
References
Specification-Based Testing
5.1 The Role of Testing in Software Design
5.2 State-Based Testing
5.2.1 Modelling Stateful Systems
5.2.2 Test Generation for State-Based Systems
5.2.3 Monitoring of Execution Traces
5.2.4 Test Generation Methods and Coverage Criteria
5.3 Conformance Testing
5.4 Using Algebraic Specifications for Testing
5.5 Tool Support for Testing
5.6 Closing Remarks
5.6.1 Annotated Bibliography
5.6.2 Current Research Directions
References
Part III Application Domains
Specification and Verification of Normative Documents
6.1 Contracts: Help or Trouble?
6.2 What Are Contracts?
6.2.1 On the Notion of Contract
6.2.2 Motivating Examples
6.3 A Framework for Specification and Analysis of Contracts
6.4 The mathcalCL Language
6.4.1 Syntax
6.4.2 Semantics
6.5 Verification of mathcalCL Contracts
6.5.1 Conflict Analysis of mathcalCL Contracts
6.5.2 The AnaCon Framework
6.5.3 Runtime Verification of Contracts
6.5.4 Model Checking Contracts
6.6 Closing Remarks
6.6.1 Annotated Bibliography
6.6.2 Current Research Directions
References
Formal Methods for Human-Computer Interaction
7.1 Human Errors and Cognition
7.1.1 Background
7.2 Human Memory and Memory Processes
7.2.1 Short-Term Memory and Closure
7.2.2 Long-Term Memory
7.3 Human Behaviour and Interaction
7.3.1 Input as Perceptions and Output as Actions
7.3.2 Cognitive Control: Attention and Goals
7.3.3 Automatic Control
7.3.4 Deliberate Control
7.3.5 Operator's Deliberate Behaviour
7.3.6 Switching Process Control
7.4 Interface/System Model
7.4.1 Experiential Knowledge and Expectations
7.4.2 Environment and Overall System
7.5 Model Checking Analyses
7.5.1 Overall System Verification
7.5.2 Task Failures Analysis
7.6 Closing Remarks
7.7 Annotated Bibliography
7.7.1 Current Research Directions
References
Formal Verification of Security Protocols
8.1 Introduction
8.2 Basic Principles
8.2.1 Cryptography
8.2.2 Principles of Security
8.2.3 Security Protocols
8.3 Needham-Schroeder Protocol for Authentication
8.4 Formal Specification of Protocols and Properties
8.4.1 Protocol Abstraction Through Use of Symbolic Data
8.4.2 Message Space
8.4.3 Protocol Participants in a Reliable Network
8.4.4 Modelling the Intruder and the Network
8.4.5 Formalising Authentication
8.5 Protocol Analysis by Model Checking
8.5.1 Encoding the Message Space in CspM
8.5.2 Protocol Encoding
8.5.3 Encoding the Intruder in CspM
8.5.4 Encoding and Verifying the Security Properties
8.6 Protocol Analysis by Theorem Proving
8.6.1 Rank Functions
8.6.2 The Rank Function Theorem
8.6.3 Applying the Rank Function Theorem
8.7 Closing Remarks
8.7.1 Annotated Bibliography
8.7.2 Current Research Directions
References
Part IV Wrapping up
Origins and Development of Formal Methods
9.1 Where do Formal Methods for Software Engineering Come From?
9.2 Logic
9.3 Specifying Programming Languages and Programs
9.4 Specifications of Data
9.5 Reasoning and Proof
9.6 Concurrency
9.7 Formal Methods Enter Specialist Areas
9.8 In Conclusion
References
Correction to: Formal Methods for Software Engineering
Correction to: M. Roggenbach et al., Formal Methods for Software Engineering, Texts in Theoretical Computer Science. An EATCS Series, https://doi.org/10.1007/978-3-030-38800-3
Authors' Conclusion
Appendix A Syntax of the Logics in this Book
A.1 Regular Expressions
A.2 Propositional Logic
A.3 First- and Second-Order Logic
A.4 Non-Classical Logics
Appendix B Language Definition of CSP
B.1 Syntax
B.1.1 Processes
B.1.2 Operator Precedences
B.1.3 Process Equations
B.2 Semantics
B.2.1 Static Semantics
B.2.2 Syntactic Sugar
B.2.3 Core Language
B.3 Operational Semantics
B.4 Denotational Semantics
B.4.1 The Traces Model mathcalT
B.4.2 The Failures/Divergences Model mathcalN
B.4.3 The Stable Failures Model mathcalF
Appendix C Concrete CASL Syntax
C.1 Specifications
C.2 Signature Declarations
C.3 Formulae
C.4 Sort Generation Constraints
Index