STINT Workshop on Runtime Verification and Autonomous Systems
August 26, 2019
Torgny Segerstedt salen (Vasaparken, GU)
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
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
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
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
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.