This book provides a hands-on introduction to runtime verification which guides the reader from zero to sufficient practical knowledge required to consider and apply it in industry. It starts with almost no assumptions on the knowledge of the reader and provides exercises throughout the book through which the reader builds their own runtime verification tool. All that is required are basic programming skills and a good working knowledge of the object-oriented paradigm, ideally Java. Drawing from years of the authors' real-world experience, the reader progresses from manually writing runtime verification code to instrumenting monitoring using aspect-oriented programming, after which they explore increasing levels of specification abstraction: automata, regular expressions, and linear time temporal logic. A range of other topics is also explored in the book, including real-time properties, concerns of efficiency and persistence, integration with testing and architectural considerations. The book is written for graduate students specializing in software engineering as well as for industry professionals who need an introduction to the topic of runtime verification. While the book focuses on underlying foundations and practical techniques, it additionally provides for each chapter a reading list in the appendix for the interested reader who would like to deepen their knowledge in a particular area.
Author(s): Christian Colombo; Gordon J. Pace
Publisher: Springer Nature
Year: 2022
Language: English
Pages: 209
Contents
Foreword
Preface
Acknowledgements
Chapter 1 The Need for Verification
1.1 The Rise of Algorithms and the Need for their Correctness
1.2 What is at Stake?
1.3 Why is Software Failure so Common?
1.4 Some Pertinent Questions
Chapter 2 What is Runtime Verification
2.1 Testing and Exhaustive Analysis
2.2 What is Runtime Verification?
2.3 Programming Runtime Monitors and Verifiers
2.4 Choices in Runtime Verification
2.5 Conclusions
Chapter 3 FiTS: A Financial Transaction System
3.1 Understanding the Structure of FiTS
3.2 FiTS Repository
3.3 The Modules
3.4 Is FiTS Fit for Purpose?
3.5 The Scenarios and their Execution
3.6 Conclusions
Chapter 4 Manual Monitoring
4.1 Monitoring using Assertions
4.2 Parameterised Properties
4.3 Conclusions
Chapter 5 Aspect-Oriented Programming
5.1 The Basics of Aspect-Oriented Programming
5.1.1 Joinpoints and Pointcuts
5.1.2 Advice and Code Injection
5.1.3 Adding Attributes and Methods
5.2 Using AspectJ for Monitoring
5.3 Advanced AOP Considerations
5.4 Conclusions
Chapter 6 Event Guarded Command Language
6.1 Introduction
6.2 Event Guarded Command Language: The Syntax
6.3 Compiling into AspectJ
6.4 Parameterised Properties in EGCL
6.5 Compiling Parameterised EGCL
6.6 Conclusions
Chapter 7 Symbolic Automata
7.1 Automata for Monitoring
7.2 Symbolic Automata
7.3 Compiling Symbolic Automata
7.4 Parameterised Automata
7.5 Compiling Parameterised Automata
7.6 Conclusions
Chapter 8 Regular Expressions
8.1 Regular Expressions
8.2 Monitoring Regular Expression Scripts
8.3 Verification of Monitoring Regular Expressions
8.3.1 Regular Expressions and Automata
8.3.2 Regular Expression Derivatives
8.4 Regular Expressions as Positive Specifications
8.5 Parameterised Regular Expression Monitoring
8.6 Conclusions
Chapter 9 Linear Temporal Logic
9.1 Syntax and Semantics
9.2 Parsing LTL Formulae
9.3 LTL Runtime Verification
9.4 Parameterised LTL Formulae
9.5 Conclusions
Chapter 10 Monitoring Real-Time Properties
10.1 Monitoring Real-Time Properties
10.2 Timers
10.3 Advanced Timer Features
10.4 Real-Time Issues
10.5 Conclusions
Chapter 11 Reactive Runtime Monitoring
11.1 Runtime-Verification-Triggered Reparations
11.2 Runtime Enforcement
11.3 State Rollback through Checkpointing
11.4 State Rollback through Compensations
11.5 Monitor-Oriented Programming
11.6 Conclusions
Chapter 12 Offline Runtime Verification
12.1 Logging of Events
12.2 Replaying Events for Monitoring
12.3 Dealing with System State
12.4 Asynchronous and Offline Verification: The Fine Print
12.5 Conclusions
Chapter 13 Other Advanced Topics
13.1 Efficiency Considerations in Runtime Verification
13.1.1 Measuring Overheads
13.1.2 Measuring Time
13.1.3 Measuring Memory
13.1.4 Reducing Overheads
13.2 Persistent Runtime Monitors
13.3 Testing and Runtime Verification
13.4 Monitoring Architectures
13.4.1 Distributed FiTS
13.4.2 Specifying Distributed Properties
13.4.3 Distributing Runtime Verification
13.5 Conclusions
Chapter 14 Conclusions
14.1 Runtime Verification Concerns
14.2 Adopting Runtime Verification in the Industry
Appendix A Further Reading
Chapter 1
Chapter 2
Chapter 3
Chapter 4
Chapter 5
Chapter 6
Chapter 7
Chapter 8
Chapter 9
Chapter 10
Chapter 11
Chapter 12
Chapter 13
Chapter 14
References
Index
