Colombo Christian, Pace Gordon J. - Runtime Verification. A Hands-On Approach In Java.pdf

(2913 KB) Pobierz
Christian Colombo
Gordon J. Pace
Runtime
Verification
A Hands-On Approach in Java
Runtime Verification
Christian Colombo • Gordon J. Pace
Runtime Verification
A Hands-On Approach in Java
Christian Colombo
Department of Computer Science
Faculty of Information
and Communications Technology
University of Malta
Msida, Malta
Gordon J. Pace
Department of Computer Science
Faculty of Information
and Communications Technology
University of Malta
Msida, Malta
ISBN 978-3-031-09266-4
ISBN 978-3-031-09268-8 (eBook)
https://doi.org/10.1007/978-3-031-09268-8
© Springer Nature Switzerland AG 2022
This work is subject to copyright. All rights are reserved by the Publisher, whether the whole or part
of the material is concerned, specifically the rights of translation, reprinting, reuse of illustrations,
recitation, broadcasting, reproduction on microfilms or in any other physical way, and transmission or
information storage and retrieval, electronic adaptation, computer software, or by similar or dissimilar
methodology now known or hereafter developed.
The use of general descriptive names, registered names, trademarks, service marks, etc. in this
publication does not imply, even in the absence of a specific statement, that such names are exempt
from the relevant protective laws and regulations and therefore free for general use.
The publisher, the authors, and the editors are safe to assume that the advice and information in this
book are believed to be true and accurate at the date of publication. Neither the publisher nor the
authors or the editors give a warranty, expressed or implied, with respect to the material contained herein
or for any errors or omissions that may have been made. The publisher remains neutral with regard to
jurisdictional claims in published maps and institutional affiliations.
This Springer imprint is published by the registered company Springer Nature Switzerland AG
The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland
Contents
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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Manual Monitoring
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.1 Monitoring using Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2 Parameterised Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
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 . . . . . . . . . . . . . . . . . . . .
1
1
3
4
6
9
9
10
12
13
15
17
17
18
19
24
26
27
29
29
34
38
41
42
42
43
44
v
2
3
4
5

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin