|
Tuesday, 27 August, 2019
|
FORMATS, Euler Room
|
|
08:30–09:00
|
Opening
|
|
09:00–10:00
|
Computing systems are becoming ever more complex, with decisions increasingly often based on deep learning components. A wide variety of applications are being developed, many of them safety-critical, such as self-driving cars and medical diagnosis. Since deep learning is unstable with respect to adversarial perturbations, there is a need for rigorous software development methodologies that encompass machine learning components. This lecture will describe progress with developing automated verification techniques for deep neural networks to ensure safety and robustness of their decisions with respect to input perturbations. The techniques exploit Lipschitz continuity of the networks and aim to approximate, for a given set of inputs, the reachable set of network outputs in terms of lower and upper bounds, in anytime manner, with provable guarantees. We develop novel algorithms based on feature-guided search, games, global optimisation and Bayesian methods, and evaluate them on state-of-the-art networks. The lecture will conclude with an overview of the challenges in this field.
|
|
10:00–10:30
|
Coffee break
|
|
10:30–12:30
|
Special session on data-driven and stochastic approaches to real-time, including monitoring and big data (Chair: Martin Fränzle)
|
|
10:30–10:32
|
|
|
10:32–11:00
|
Monitoring of a signal plays an essential role in the runtime verification of cyber-physical systems. Qualitative timed pattern matching is one of the mathematical formulations of monitoring, which gives a Boolean verdict for each sub-signal according to the satisfaction of the given specification. There are two orthogonal directions of extension of the qualitative timed pattern matching. One direction on the result is quantitative: what engineers want is often not a qualitative verdict but the quantitative measurement of the satisfaction of the specification. The other direction on the algorithm is online checking: the monitor returns some verdicts before obtaining the entire signal, which enables to monitor a running system. It is desired from application viewpoints. In this paper, we conduct these two extensions, taking an automata-based approach. This is the first quantitative and online timed pattern matching algorithm to the best of our knowledge. More specifically, we employ what we call timed symbolic weighted automata to specify quantitative specifications to be monitored, and we obtain an online algorithm using the shortest distance of a weighted variant of the zone graph and dynamic programming. Moreover, our problem setting is semiring-based and therefore general. Our experimental results confirm the scalability of our algorithm for specifications with a time-bound.
|
|
11:00–11:30
|
Mahmoud Salem, Gonzalo Carvajal*, Tong Liu and Sebastian Fischmeister
Design of real-time systems is prone to uncertainty due to software and hardware changes throughout their deployment. In this context, both industry and academia have shown interest in new trace mining approaches for diagnosis and prognosis of complex embedded systems. Trace mining techniques construct empirical models that mainly target achieving high accuracy in detecting anomalies. However, when applied to safety-critical systems, such models lack in providing theoretical bounds on the system resilience to variations from these anomalies.
The paper presents the first work to derive robustness criteria on a trace mining approach that constructs arrival-curves models from datasets of traces collected from real-time systems. Through abstracting arrival-curves models to the demand-bound functions of a sporadic task under an EDF scheduler, the paper enables designers to quantify the permissible change to the parameters of a given task model by relating to the variation expressed within the empirical model. We evaluate the approach on an industrial cyber-physical system that generates traces of timestamped QNX events.
|
|
11:30–12:00
|
Timeprints are temporal regularly-logged signatures, describing a signal’s temporal behavior.
They have been recently used in on-chip signals tracing and temporal properties checking.
Timeprints are generated by aggregations of encoded timestamps marking where signal changes took place.
This paper describes different timestamps encoding mechanisms, and shows how some system’s temporal properties can be used to create more efficient timestamps.
The efficiency of a timestamps-encoding is introduced in terms of the number of collisions in the timeprints-reconstruction solution space.
We show how using property-based timestamps encoding reduces the number of such collisions leading to faster reconstruction and less properties checking time.
|
|
12:00–12:30
|
We present Mixed-time Signal Temporal Logic (MX-STL), a specification formalism which extends STL by capturing
the discrete/continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal designs.
In MX-STL, properties of components with continuous dynamics are
expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we parameterize
the logic with a sampling period T and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that MX-STL has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring MX-STL formulas and illustrate the approach using a mixed-signal example.
|
|
12:30–13:30
|
Lunch break
|
|
13:30–15:00
|
Timed systems (Chair: Didier Lime)
|
|
13:30–14:00
|
We propose a new method for computing the language intersection of
two Time Petri nets (TPN); that is the sequence of labels
in timed traces common to the execution of two TPN. Our approach is
based on a new product construction between nets and relies on the State
Class construction, a widely used method for checking the behavior of
TPN. We prove that this new construct does not add additional expressive
power, and yet that it can leads to very concise representation of the
result. We have implemented our approach in a new tool, called Twina.
We report on some experimental results obtained with this tool and show
how to apply our approach on two interesting problems: first, to define
an equivalent of the twin-plant diagnosability methods for TPN; then as
a way to check timed properties without interfering with a system.
|
|
14:00–14:30
|
Anne Bouillard*
With the development of real-time networks and of new wireless communication technologies having strong requirements on latencies and reliability, there is a need to compute deterministic performance bounds. This paper focuses on the performance guarantees and stability conditions in networks with cyclic dependencies in the network calculus framework.
Two kinds of techniques exist: backlog-based techniques compute backlog bounds for each server, and obtain good stability bounds at the detriments of the performance bounds; flow-based techniques compute performance bounds for each flow and obtain better performance bounds for low bandwidth usage, but poor stability conditions.
In this article, we propose a unified framework that combines the two techniques and improve at the same time stability conditions and performance bounds. To do this, we first propose an algorithm that computes tight backlog bounds in trees for a set of flows at a server, and then develop a linear program based on this algorithm that computes performances bounds for cyclic networks. An implementation of these algorithms is provided in the Python package NCBounds and is used for numerical experiments showing the efficiency of the approach.
|
|
14:30–15:00
|
Alexey Bakhirkin, Nicolas Basset, Oded Maler and José-Ignacio Requeno Jarabo*
This paper presents ParetoLib, a Python library that implements a new method for inferring the Pareto front in multi-criteria optimization problems. The tool can be applied in the parameter synthesis of temporal logic predicates where the influence of parameters is monotone. ParetoLib currently provides support for the parameter synthesis of standard (STL) and extended (STLe) Signal Temporal Logic specifications. The tool is easily upgradeable for synthesizing parameters in other temporal logics in the near future. An example illustrates the usage and performance of our tool. ParetoLib is free and publicly available on Internet.
|
|
15:00–15:30
|
Coffee break
|
|
15:30–17:00
|
Linear and non-linear systems (Chair: Majid Zamani)
|
|
15:30–16:00
|
Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation
for nonlinear systems with polynomial dynamics, which leverages a combination of
barrier certificates. PBT has advantages over traditional time-step based methods
in dealing with those nonlinear dynamical systems in which there is a large difference
in speed between trajectories, producing an overapproximation that is time
independent.
However, the existing approach for PBT is not efficient due to
the application of interval methods for enclosure-box computation, and it can only deal
with continuous dynamical systems without uncertainty. In this paper, we extend the
approach with the ability to handle both continuous and hybrid dynamical systems
with uncertainty that can reside in parameters and/or noise.
We also improve the efficiency of the method significantly, by avoiding
the use of interval-based methods for the enclosure-box computation without loosing soundness.
We have developed a C++ prototype implementing the proposed approach and
we evaluate it on several benchmarks. The experiments show that
our approach is more efficient and precise than other methods in the literature.
|
|
16:00–16:30
|
This paper introduces the abstraction of max-plus linear (MPL) systems via predicates. Predicates are automatically selected from system matrix, as well as from the specifications under consideration. We focus on verifying time-diference specifcations, which encompass the relation between successive events in MPL systems. We implement a bounded model checking (BMC) procedure over a predicate abstraction of the given MPL system, to verify the satisfaction of time-difference specifications. Our predicate abstractions are experimentally shown to improve on existing MPL abstractions algorithms. Furthermore, with focus on the BMC algorithm, we can provide an explicit upper bound on the completeness threshold by means of the transient and the cyclicity of the underlying MPL system.
|
|
16:30–17:00
|
Hoang-Dung Tran, Luan Nguyen, Nathaniel Hamilton, Weiming Xiang and Taylor Johnson*
Reachability analysis is a fundamental problem for safety verification and falsification of Cyber-Physical Systems (CPS) whose dynamics follow physical laws usually represented as differential equations. In the last two decades, numerous reachability analysis methods and tools have been proposed for a common class of dynamics in CPS known as ordinary differential equations (ODE). However, there is lack of methods dealing with differential algebraic equations (DAE) which is a more general class of dynamics that is widely used to describe a variety of problems from engineering and science such as multibody mechanics, electrical circuit design, incompressible fluids, molecular dynamics and chemical process control. Reachability analysis for DAE systems is more complex than ODE systems, especially for high-index DAEs because they contain both a differential part (i.e., ODE) and algebraic constraints (AC). In this paper, we propose a scalable reachability analysis for a class of high-index large linear DAEs. In our approach, a high-index linear DAE is first decoupled into one ODE and one or several AC subsystems based on the well-known Marz decoupling method utilizing admissible projectors. Then, the discrete reachable set of the DAE, represented as a list of star-sets, is computed using simulation. Unlike ODE reachability analysis where the initial condition is freely defined by a user, in DAE cases, the consistency of the initial condition is an essential requirement to guarantee a feasible solution. Therefore, a thorough check for the consistency is invoked before computing the discrete reachable set. Our approach successfully verifies (or falsifies) a wide range of practical, high-index linear DAE systems in which the number of state variables varies from several to thousands.
|
|
17:00–17:30
|
Check your emails or take a nap or attend CONCUR
|
|
17:30–19:00
|
Drinks (with CONCUR)
|
|
Wednesday, 28 August, 2019
|
FORMATS, Euler Room
|
|
08:30–09:00
|
Opening
|
|
09:00–10:00
|
When are dense-time stochastic systems tameable?
Many applications, such as communication protocols, require models
which integrate both real-time constraints, and randomization. The
verification of such models is a challenging task since they combine
dense-time and probabilities. To verify stochastic real-time systems,
we propose a framework to perform the analysis of general stochastic
transition systems (STSs). This methodology relies on two pillars: a
decisiveness and abstraction.
Decisiveness was introduced for denumerable Markov
chains [ABM07], and roughly speaking, it allows one to lift
most analysis techniques from finite Markov chains to denumerable
ones, and therefore to adapt existing verification algorithms to
infinite-state models. We explain how to generalize this central
notion to dense-time stochastic models.
In order to exploit decisiveness, we define a notion of abstraction,
and we give general transfer properties from the abstract model to
the concrete one. These are central to come up with qualitative and
quantitative verification algorithms for STS.
Our methodology applies for instance to stochastic timed automata
(STA) and generalized semi-Markov processes (GSMP), two existing
models combining dense-time and probabilities. This allows us on the
one hand to recover existing results from the literature on these two
models --with less effort and a unified view-- and on the other hand
to derive new approximation algorithms for STA and GSMP.
The interested reader can refer to a joint article with Patricia
Bouyer, Thomas Brihaye and Pierre Carlier for further details.
Bio: Nathalie Bertrand obtained her PhD from ENS Cachan in 2006, supervised by
Philippe Schnoebelen. She spent a year at TU Dresden working with Christel
Baier, and was in 2007 hired junior research scientist at Inria Rennes. Her
expertise is in model checking specifically for probabilistic systems.
|
|
10:00–10:30
|
Coffee break
|
|
10:30–12:30
|
Timed automata (chair: Martin Fränzle)
|
|
10:30–11:00
|
Amnon Rosenmann*
Let eNTA be the class of non-deterministic timed automata with silent transitions. Given an automaton A in eNTA, we effectively compute its timestamp: the set of all pairs (time value, action) of all observable timed traces of A. We show that the timestamp is eventually periodic and that one can compute a simple deterministic timed automaton with the same timestamp as that of A. As a consequence, we have a partial method, not bounded by time or number of steps, for the general language non-inclusion problem for eNTA. We also show that the language of A is periodic with respect to suffixes.
|
|
11:00–11:30
|
Amnon Rosenmann*
Some fundamental problems in the class of non-deterministic timed automata, like the problem of inclusion of the language accepted by timed automaton A (e.g., the implementation) in the language accepted by B (e.g., the specification) are, in general, undecidable. However, one can effectively construct deterministic approximate timed automata, that differ from the original automata by at most 1/2 time unit on each occurrence of an event, compare their languages and project the results to the original automata. We define the distance between timed automata as the limit on how far away a timed trace of one timed automaton can be from the closest timed trace of the other timed automaton. We then show how one can decide under some restriction whether the distance between two timed automata is infinite.
|
|
11:30–12:00
|
Model learning has gained increasing interest in recent years. It derives behavioural models from test data of black-box systems. The main advantage offered by such techniques is that they enable model-based analysis without access to the internals of a system. Applications range from fully automated testing over model checking to system understanding. Current work focuses on learning variations of finite state machines. However, most techniques consider discrete time. In this paper, we present a novel method for learning timed automata, finite state machines extended with real-valued clocks. The learning method generates a model consistent with a set of timed traces collected via testing. This generation is based on genetic programming, a search-based technique for automatic program creation. We evaluate our approach on 44 timed systems, comprising of four systems from the literature (two industrial and two academic) and 40 randomly generated examples.
|
|
12:00–12:30
|
Simon Wimmer*
Munta is a mechanically verified model checker for timed automata, a popular formalism for modeling real-time systems.
Our goal is two-fold: first, we want to provide a reference implementation that is fast enough to test other model checkers against it on reasonably sized benchmarks; second, the tool should be practical enough so that it can easily be used for experimentation.
Munta can be compiled to Standard ML or OCaml and additionally features a web-based GUI.
Its modeling language has a simple semantics but provides the most commonly used timed automata modeling features.
|
|
12:30–13:15
|
Lunch break
|
|
13:15–21:00
|
Excursion and banquet (with CONCUR)
|
|
Thursday, 29 August, 2019
|
FORMATS, Euler Room
|
|
08:30–09:00
|
Opening
|
|
09:00–10:00
|
Keynote: Kim G. Larsen (room: Turing) (chair: Mariëlle Stoelinga)
UPPAAL Stratego is a recent branch of the verification tool UPPAAL
allowing for synthesis of safe and optimal strategies for stochastic
timed (hybrid) games. We describe newly developed learning methods,
allowing for synthesis of significantly better strategies and with
much improved convergence behaviour. Also, we describe novel use of
decision trees for learning orders-of-magnitude more compact
strategy representation. In both cases, the seek for optimality
does not compromise safety.
|
|
10:00–10:30
|
Coffee break
|
|
10:30–12:00
|
Special session on timed systems and probabilities (chair: Nathalie Bertrand)
|
|
10:30–11:00
|
Current cyber-physical systems (CPS) are expected to accomplish complex tasks. To achieve this goal, high performance, but unverified controllers (e.g. deep neural network, black-box controllers from third parties) are applied, which makes it very challenging to keep the overall CPS safe. By sandboxing these controllers, we are not only able to use them but also to enforce safety properties over the controlled physical systems at the same time. However, current available solutions for sandboxing controllers are just applicable to deterministic (a.k.a. non-stochastic) systems, possibly affected by bounded disturbances. In this paper, for the first time we propose a novel solution for sandboxing unverified complex controllers for CPS operating in noisy environments (a.k.a. stochastic CPS). Moreover, we also provide probabilistic guarantees on their safety. Here, the unverified control input is observed at each time instant and checked whether it violates the maximal tolerable probability of reaching the unsafe set. If this probability exceeds a given threshold, the unverified control input will be rejected, and the advisory input provided by the optimal safety controller will be used to maintain the probabilistic safety guarantee. The proposed approach is illustrated empirically and the results indicate that the expected safety probability is guaranteed.
|
|
11:00–11:30
|
We deal with the lumpability approach to cope with the state-space explosion problem inherent to the computation of the performance indices of large stochastic models using a state aggregation technique. The lumpability method applies to Markov chains exhibiting some structural regularity and allows one to efficiently compute the exact values of the performance indices when the model is actually lumpable. The notion of quasi-lumpability is based on the idea that a Markov chain can be altered by relatively small perturbations of the transition rates in such a way that the new resulting Markov chain is lumpable. In this case only upper and lower bounds on the performance indices can be derived.
In this paper we introduce a novel notion of quasi lumpability, named proportional lumpability, which extends the original definition of lumpability but, differently than the general definition of quasi lumpability, it allows one to derive exact performance indices for the original process.
|
|
11:30–12:00
|
Abstract: Probabilistic timed automata(PTA) model real-time systems with non-deterministic and stochastic behavior. They extend Alur-Dill timed automata by allowing probabilistic transitions and a price structure on the locations and transitions. Thus, a PTA can be considered as a Markov decision process (MDP) with uncountably many states and transitions. Expected reachability-price games are turn-based games where two games, Player MIN and Player MAX, move a token along the infinite configuration space of PTA. The objective of player MIN is to minimize the expected price to reach a target location, while the goal of the MAX player is the opposite. The undecidability of computing the value in the expected reachability-price games follows form the undecidability of the corresponding problem on timed automata. The key contribution of this work is to recover decidability for 1-clock binary-priced PTA.
|
|
12:00–12:15
|
Closing session
|
|
12:30–13:30
|
Lunch break
|
