Invited Tutorial
Laura Nenzi, Ezio Bartocci, Luca Bortolussi, Michele Loreti, and Ennio Visconti: Monitoring Spatio-Temporal Properties
From the formation of traffic jams to the development of troublesome, whirlpool-like spirals in the heart’s electrical activity, spatio-temporal patterns are key in understanding how complex behaviors can emerge in a network of locally interacting dynamical systems. One of the most important and intriguing questions is how to specify spatio-temporal behaviors in a formal and human understandable specification language and how to monitor their onset efficiently.
In this tutorial, we present the spatio-temporal logic STREL and its expressivity to specify and monitor spatio-temporal behaviors over complex dynamical and spatially distributed systems. We demonstrate our formalism’s applicability to different scenarios considering static or dynamic spatial configurations and systems with deterministic or stochastic dynamics.
Tutorial 1
Y. A. Liu and S. D. Stoller Assurance of Distributed Algorithms and Systems: Runtime Checking of Safety and Liveness
This tutorial presents a general framework and methods for complete programming and checking of distributed algorithms at a high level, as in pseudo-code languages, but precisely specified and directly executable, as in formal specification languages and practical programming languages, respectively. The checking framework, as well as the writing of distributed algorithms and specification of their safety and liveness properties, use DistAlgo, a high-level language for distributed algorithms. We give a complete executable specification of the checking framework, with a complete example algorithm and example safety and liveness properties.
Tutorial 2
M. Schwenger, Monitoring Cyber-Physical Systems from Design to Integration
Cyber-physical systems are inherently safety-critical. The deployment of a runtime monitor significantly increases confidence in their safety. The effectiveness of the monitor can be maximized by considering it an integral component during its development. Thus, in this paper, I given an overview over recent work regarding a development process for runtime monitors alongside a cyber-physical system. This process includes the transformation of desirable safety properties into the formal specification language RTLola. A compiler then generates an executable artifact for monitoring the specification. This artifact can then be integrated into the system.
Tutorial 3
J. H. Dawes, M. Han, O. Javed, G. Reger, G. Franzoni, A. Pfeiffer, Analysing the Performance of Python-based Web Services with the VyPR Framework
In this tutorial , we present the current state of VyPR, a framework for the performance analysis of Python-based web services. We begin by summarising our theoretical contributions which take the form of an engineer-friendly specification language; instrumentation and monitoring algorithms; and an approach for explanation of property violations. We then summarise the VyPR ecosystem, which includes an intuitive library for writing specifications and powerful tools for analysing monitoring results. We conclude with a brief description of how VyPR was used to improve our understanding of the performance of a critical web service at the CMS Experiment at CERN.
Tutorial 4
K. Havelund, D. Peled, BDDs for Representing Data in Runtime Verification
A BDD (Boolean Decision Diagram) is a data structure for the compact representation of a Boolean function. It is equipped with efficient algorithms for minimization and for applying Boolean operators. The use of BDDs for representing Boolean functions, combined with symbolic algorithms, facilitated a leap in the capability of model checking for the verification of systems with a huge number of states. Recently BDDs were considered as an efficient representation of data for Runtime Verification (RV). We review here the basic theory of BDDs and summarize their use in model checking and specifically in runtime verification.