Runtime Verification: A Hands-On Approach in Java

Description

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. 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