STINT Workshop on Runtime Verification and Autonomous Systems

August 26, 2019
Torgny Segerstedt salen (Vasaparken, GU)
Gothenburg, Sweden

Organizer: Gerardo Schneider

A STINT collaboration workshop beteween the Department of Computer Science, Universidad de Buenos Aires (Argentina) and the Department of Computer Science and Engineering at the University of Gothenburg (Sweden).

============================================

PROGRAMME

============================================

08:55 Welcome
09:00 A very gentle introduction to Runtime Verification (Gerardo Schneider, GU)
09:30 Stream Runtime Verification (César Sánchez, IMDEA, Spain)
10:00 TeSSLa - from monitoring to control (Martin Leucker, Univ. of Lübeck, Germany)

10:30 Coffee Break

11:00 Runtime Synthesis for Adaptive Synthesis (Sebastián Uchitel, UBA)
11:30 Reactive Synthesis on Unmanned Aerial Vehicles (UAVs) (Sebastián Zudaire, UBA)
12:00 Dynamic Update of Discrete Event Controllers (Leandro Nahabedian, UBA)

12:30-13:30 Lunch Break

13:30 Environmentally-Friendly GR(1) Synthesis (Nir Piterman, GU)
14:00 Testing and validating end user programmed calculated fields (Diego Garbervetsky, UBA)
14:30 Making robots usable in everyday life (Patrizio Pelliccione, University of L'Aquila, Italy, and Chalmers, Sweden)

15:00 Coffee Break

15:30 Generating Structurally Rich Random Algebraic Data Type Values (Alejandro Russo, Chalmers)
16:00- 17:00 Discussion


============================================

TALKS' ABSTRACTS

============================================

Title: A very gentle introduction to Runtime Verification
Speaker: Gerardo Schneider (GU)
Abstract: In this talk I will give a very high-level introduction to Runtime Verification.

===========================

Title: Stream Runtime Verification
Speaker: César Sánchez (IMDEA, Spain)
Abstract: Stream Runtime Verification is behavioral specification language for runtime verification, where a monitor is described by expressing the dependencies between the output streams of values in terms of the input streams of observations. The classical approaches to runtime verification borrow specification languages from static verification, like linear temporal logic (LTL), LTL for finite traces, regular expressions, etc. In comparison, stream runtime verification is based on the observation that many monitoring algorithms can be generalized from Booleans to rich data domains. Stream runtime verification provides a friendly language (with a programming look and feel) to express these dependencies and automatically generate monitors that compute streams of values from streams of observations. At the same time, one can translate automatically logical specifications into stream runtime verification specifications with a correctness guarantee. In this lecture I will briefly introduce runtime verification focusing on its potential as a building block in reliable UAV software.

===========================

Title: TeSSLa - from monitoring to control
Speaker: Martin Leucker (University of Lübeck, Germany)
Abstract: TeSSLa is designed as a temporal stream-based specification language for formalizing the behaviour of cyber-physical systems. Formally, TeSSLa allows the constructive mathmatical formulation of functions from a set of functions from a time domain to a data domain - input streams - to a set of corresponding output streams. While TeSSLa is currently mainly used for runtime verification purposes, it can equally be used for building self-X-applications. More precisely, the TeSSLa input may be obtained from a system and the computed output may be retransmitted to system for steering it, or, in other words, for controlling it. This presentation gives a short introduction to TeSSLa and its use for decribing the intended behaviour of cyber-physical systems. Moreover, we show how several well-known controllers from control theory can be formalized in TeSSLa making it a vivid tool for building self-X-applications.

===========================

Title: Runtime Synthesis for Adaptive Synthesis
Speaker: Sebastián Uchitel (UBA, Argentina)
Abstract: How can we design systems that have ability to automatically react to changes in their environment, capabilities and goals without having to guess at design time what these changes might be? In this talk I will argue that runtime synthesis of discrete event controllers can be a key enabler for adaptation. I will briefly cover what discrete event control is, how it can fit into a adaptive software architecture, our experiences using it in the robotics domain, and some of the challenges that we face.

===========================

Title: Reactive Synthesis on Unmanned Aerial Vehicles (UAVs)
Speaker: Sebastián Zudaire (UBA, Argentina)
Abstract: Over the last decades there has been an increasing interest in using synthesis as a way to automatically generate plans for robots from mission specifications. The main challenge is to use an abstraction for the synthesis problem that is detailed enough to specify a great number of missions, but not too much that the problem becomes impossible to compute. This is especially complicated in the reactive large scale scenario present in many UAV applications. I will explain how we managed these issues and implemented an end-to-end framework for the UAV, validated in typical robotic missions.

===========================

Title: Dynamic Update of Discrete Event Controllers
Speaker: Leandro Nahabedian (UBA, Argentina)
Abstract: Discrete event controllers are at the heart of many software systems that require continuous operation. Changing these controllers at runtime to cope with changes in its execution environment or system requirements change is a challenging open problem. In this talk I present a technique for automatically computing a controller that handles the transition from the old to the new specification, assuring that the system will reach a state in which such a transition can correctly occur and in which the underlying system architecture can reconfigure. The solution uses discrete event controller synthesis to automatically build a controller that guarantees both progress towards update and safe update. Recently, the presented technique makes impact in the business process domain where a process that was defined to guarantee some business requirements has to be updated because there are new requirements to guarantee.

===========================

Title: Environmentally-Friendly GR(1) Synthesis
Speaker: Nir Piterman (GU)
Abstract: Many problems in reactive synthesis are stated using two formulas ---an environment assumption and a system guarantee--- and ask for an implementation that satisfies the guarantee in environments that satisfy their assumption. Reactive synthesis tools often produce strategies that formally satisfy such specifications by actively preventing an environment assumption from holding. While formally correct, such strategies do not capture the intention of the designer. I will discuss some of the issues that arise in such cases and some of the remedies that exist.

===========================
Title: Testing and validating end user programmed calculated fields.
Speaker: Diego Garbervetsky (UBA, Argentina)
Abstract: We present an approach for systematically generating test data from production databases for end user calculated field program via a novel combination of symbolic execution and database queries. We discuss the opportunities and challenges that this specific domain poses for symbolic execution and shows how database queries can help complement some of symbolic execution's weaknesses, namely in the treatment of loops and also of path conditions that exceed SMT solver capabilities.

===========================

Title: Generating Structurally Rich Random Algebraic Data Type Values
Speaker: Alejandro Russo (Chalmers)
Abstract: Automatic generation of random values described by algebraic data types (ADTs) is often a hard task. State-of-the-art random testing tools can automatically synthesize random data generators based on ADTs definitions. In that manner, generated values comply with the structure described by ADTs, something that proves useful when testing software which expects complex inputs. However, it sometimes becomes necessary to generate structural richer ADTs values in order to test deeper software layers. In this work we propose to leverage static information found in the codebase as a manner to improve the generation process. Namely, our generators are capable to consider how programs branch on input data as well as how ADTs values are built via interfaces. We implement a tool, responsible for synthesizing generators for ADTs values while providing compile time guarantees about their distributions. Using compile-time predictions, we provide a heuristic that tries to adjust the distribution of generators to what developers might want. We report on preliminary experiments where our approach shows encouraging results. This talk is based on a joint work with Agustín Mista.

===========================