nach oben

2018 | Buch

Kapitel lesen Erstes Kapitel lesen

Lectures on Runtime Verification

Introductory and Advanced Topics

herausgegeben von: Ezio Bartocci, Yliès Falcone

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

The idea of this volume originated from the need to have a book for students to support their training with several tutorials on different aspects of RV. The volume has been organized into seven chapters and the topics covered include an introduction on runtime verification, dynamic analysis of concurrency errors, monitoring events that carry data, runtime error reaction and prevention, monitoring of cyber-physical systems, runtime verification for decentralized and distributed systems and an industrial application of runtime verification techniques in financial transaction systems.

Inhaltsverzeichnis

Frontmatter

Introduction to Runtime Verification

Abstract

The aim of this chapter is to act as a primer for those wanting to learn about Runtime Verification (RV). We start by providing an overview of the main specification languages used for RV. We then introduce the standard terminology necessary to describe the monitoring problem, covering the pragmatic issues of monitoring and instrumentation, and discussing extensively the monitorability problem.

Ezio Bartocci, Yliès Falcone, Adrian Francalanza, Giles Reger

Discovering Concurrency Errors

Abstract

Lots of concurrent software is being developed for the now ubiquitous multicore processors. And concurrent programming is difficult because it is quite easy to introduce errors that are really hard to diagnose and fix. One of the main obstacles to concurrent programming is that threads are scheduled nondeterministically and their interactions may become hard to predict and to devise. This chapter addresses the nature of concurrent programming and some classes of concurrency errors. It discusses the application of dynamic program analysis techniques to detect, locate and diagnose some common concurrency errors like data races, atomicity violations and deadlocks. This chapter also mentions some techniques that can help with quality assurance of concurrent programs, regardless of any particular class of concurrency errors, like noise injection and systematic testing, and it is closed by some prospects of concurrent software development.

João M. Lourenço, Jan Fiedor, Bohuslav Křena, Tomáš Vojnar

Monitoring Events that Carry Data

Abstract

Very early runtime verification systems focused on monitoring what we can refer to as propositional events: just names of events. For this, finite state machines, standard regular expressions, or propositional temporal logics were sufficient formalisms for expressing properties. However, in practice there is a need for monitoring events that in addition carry data arguments. This adds complexity to both the property specification languages, and monitoring algorithms, which is reflected in the many alternative such approaches suggested in the literature. This chapter presents five different formalisms and monitoring approaches that support specifications with data, in order to illustrate the challenges and various solutions.

Klaus Havelund, Giles Reger, Daniel Thoma, Eugen Zălinescu

Runtime Failure Prevention and Reaction

Abstract

This chapter describes how to use in-the-field runtime techniques to improve the dependability of software systems. In particular, we first present an overall vision of the problem of ensuring highly-dependable behaviours at runtime based on the concept of autonomic monitor, and then we present the two families of relevant approaches for this purpose. First, we present techniques related to runtime enforcement that can prevent the system producing bad behaviours. Second, we describe healing techniques that can detect if the system has produced a bad behaviour and react to the situation accordingly (e.g., moving the system back to a correct state).

Yliès Falcone, Leonardo Mariani, Antoine Rollet, Saikat Saha

Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications

Abstract

The term Cyber-Physical Systems (CPS) typically refers to engineered, physical and biological systems monitored and/or controlled by an embedded computational core. The behaviour of a CPS over time is generally characterised by the evolution of physical quantities, and discrete software and hardware states. In general, these can be mathematically modelled by the evolution of continuous state variables for the physical components interleaved with discrete events. Despite large effort and progress in the exhaustive verification of such hybrid systems, the complexity of CPS models limits formal verification of safety of their behaviour only to small instances. An alternative approach, closer to the practice of simulation and testing, is to monitor and to predict CPS behaviours at simulation-time or at runtime. In this chapter, we summarise the state-of-the-art techniques for qualitative and quantitative monitoring of CPS behaviours. We present an overview of some of the important applications and, finally, we describe the tools supporting CPS monitoring and compare their main features.

Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donzé, Georgios Fainekos, Oded Maler, Dejan Ničković, Sriram Sankaranarayanan

Runtime Verification for Decentralised and Distributed Systems

Abstract

This chapter surveys runtime verification research related to distributed systems. We report solutions that study how to monitor system with some distributed characteristic, solutions that use a distributed platform for performing a monitoring task, and foundational works that present semantics for decomposing monitors or expressing specifications amenable for distributed systems.

We will identify some characteristics that distinguish distributed monitoring from centralised monitoring, and characteristics that allow to classify distributed runtime verification works based on features of the executing platforms, the specification language and the system description. Then, we will use these characteristics to describe and compare the distributed runtime verification solutions proposed in the research literature.

Adrian Francalanza, Jorge A. Pérez, César Sánchez

Industrial Experiences with Runtime Verification of Financial Transaction Systems: Lessons Learnt and Standing Challenges

Abstract

The chapter will focus on experiences the authors had in applying runtime verification in industrial settings, in particular on financial transaction systems. We discuss how runtime verification can be introduced in the software development lifecycle and who are the people to be involved and when. Furthermore, we investigate what kind of properties have been found useful in practise and how these were monitored to keep intrusion to a minimum. Next, we describe two significant case studies which have been successfully carried out in the past, and conclude by outlining a number of challenges which we believe still need to be addressed for runtime verification to become more mainstream in industrial settings.

Christian Colombo, Gordon J. Pace

Backmatter

Titel: Lectures on Runtime Verification
herausgegeben von: Ezio Bartocci
Yliès Falcone
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-75632-5
Print ISBN: 978-3-319-75631-8
DOI: https://doi.org/10.1007/978-3-319-75632-5

Springer Professional

Über dieses Buch

Inhaltsverzeichnis

Frontmatter

Introduction to Runtime Verification

Discovering Concurrency Errors

Monitoring Events that Carry Data

Runtime Failure Prevention and Reaction

Specification-Based Monitoring of Cyber-Physical Systems: A Survey on Theory, Tools and Applications

Runtime Verification for Decentralised and Distributed Systems

Industrial Experiences with Runtime Verification of Financial Transaction Systems: Lessons Learnt and Standing Challenges

Backmatter

Premium Partner