Important dates

abstract

Abstract submission

9 May 2019 20 May 2019 AoE

paper

Paper submission

13 May 2019 20 May 2019 AoE

notification

Notification

23 June 2019

camera-ready

Camera-ready

8 July 2019

conference

Conference

27-29 August 2019

Invited speakers

Nathalie Bertrand

Nathalie Bertrand

FORMATS invited speaker

When are dense-time stochastic systems tameable?

Call for papers

Call for papers

Objectives

Control and analysis of the timing of computations is crucial to many domains of system engineering, be it, e. g., for ensuring timely response to stimuli originating in an uncooperative environment, or for synchronising components in VLSI. Reflecting this broad scope, timing aspects of systems from a variety of domains have been treated independently by different communities in computer science and control. Researchers interested in semantics, verification and performance analysis study models such as timed automata and timed Petri nets, the digital design community focuses on propagation and switching delays, while designers of embedded controllers have to take account of the time taken by controllers to compute their responses after sampling the environment, as well as of the dynamics of the controlled process during this span.

Timing-related questions in these separate disciplines do have their particularities. However, there is a growing awareness that there are basic problems (of both scientific and engineering level) that are common to all of them. In particular, all these sub-disciplines treat systems whose behaviour depends upon combinations of logical and temporal constraints; namely, constraints on the temporal distances between occurrences of successive events. Often, these constraints cannot be separated, as the intrinsic dynamics of processes couples them, necessitating models, methods, and tools facilitating their combined analysis. Reflecting this, FORMATS 2019 promotes submissions on hybrid discrete-continuous systems, and will promote a special session on this topic.

Topics of interest

The aim of FORMATS is to promote the study of fundamental and practical aspects of timed systems, and to bring together researchers from different disciplines that share interests in modelling and analysis of timed systems and, as a generalisation, of hybrid systems. In 2019, FORMATS aims at being more inclusive w.r.t. applications, notably real-time systems.

Typical topics include (but are not limited to):

Foundations and Semantics:

Theoretical foundations of timed systems and languages; new models and logics for analysis and comparison of existing models (like automata, Petri nets, max-plus models, network calculus, or process algebras involving quantitative time; hybrid automata; probabilistic automata and logics).

Methods and Tools:

Techniques, algorithms, data structures, and software tools for verification, synthesis, learning, online monitoring and runtime verification of timed or hybrid systems and for resolving temporal constraints (scheduling, worst-case execution time analysis, optimisation, model checking, testing, constraint solving).

Applications:

Adaptation and specialisation of timing technology in application domains in which timing plays an important role (real-time software, embedded control, hardware circuits, biological systems, and problems of scheduling in manufacturing and telecommunications).

Submission

Format and submission

Springer LNCS

submission

FORMATS 2019 solicits high-quality papers reporting research results and/or experience reports related to the topics mentioned above. Submitted papers must contain original, unpublished contributions, not submitted for publication elsewhere. The papers should be submitted electronically in PDF, following the Springer LNCS style and ethical guidelines. In particular, every author has contributed sufficiently to the intellectual scientific work. Submissions should not exceed 15 pages in length (not including the bibliography, which is thus not restricted), but may be supplemented with a clearly marked appendix, which will be reviewed at the discretion of the program committee. Authors should consult Springer’s authors’ guidelines and use their proceedings templates, either for LaTeX or for Word, for the preparation of their papers. Springer encourages authors to include their ORCIDs in their papers. In addition, the corresponding author of each paper, acting on behalf of all of the authors of that paper, must complete and sign a Consent-to-Publish form. The corresponding author signing the copyright form should match the corresponding author marked on the paper. Once the files have been sent to Springer, changes relating to the authorship of the papers cannot be made.

New this year: FORMATS also sollicits tool papers. Tool papers should describe a tool, focusing on its usage rather than on the underlying theory. The tool should be available online and come with a (possibly minimal) documentation.

Each paper will undergo a thorough review process.

Following the tradition started in 2018, FORMATS 2019 will award a best paper award in memory of Oded Maler.

We strongly encourage authors to add line numbers to their submitted paper (for example using the LaTeX lineno package).

Special sessions

FORMATS 2019 will contain two special sessions. Papers submitted into special sessions will undergo the same review process as regular papers, but will be presented in a special slot during the conference.

  1. Special session on data-driven and stochastic approaches to real-time, including monitoring and big data (chaired by Martin Fränzle)
  2. Special session on timed systems and probabilities (chaired by Nathalie Bertrand)

Publication

Publication of the proceedings of FORMATS 2019 will be hosted by Springer in the Lecture Notes in Computer Science series (to be confirmed). During the conference, participants have free online access to the proceedings from a webpage.

Submit your paper

Program

Program

Vintage page sheet background

Show abstracts

Download the program as an ICS file

Tuesday, 27 August, 2019 FORMATS, Euler Room
08:30–09:00 Opening
09:00–10:00
Keynote: Marta Kwiatkovska (room: Turing) (chair: Jos Baeten)
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–11:00
Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata
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
Assessing the Robustness of Arrival Curves Models for Real-time Systems
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
Rehab Massoud, Hoang Le and Rolf Drechsler
Temporal Properties Driven Timestamps Encoding in the Timeprints Context
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
Thomas Ferrère, Oded Maler and Dejan Nickovic
Mixed-Time Signal Temporal Logic
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
Silvano Dal Zilio, Éric Lubat, Didier Le Botlan, Yannick Pencolé and Audine Subias
A State Class Construction for Computing the Intersection of Time Petri Nets Languages
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
Stability and performance bounds in cyclic networks using network calculus
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
ParetoLib: A Python Library for Parameter Synthesis [tool paper]
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: Alessandro Abate)
15:30–16:00
Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty
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
Muhammad Syifa’Ul Mufid, Dieky Adzkiya and Alessandro Abate
Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions
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 for High-Index Linear Differential Algebraic Equations
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/FMICS
17:30–19:00 Drinks (with CONCUR)
Wednesday, 28 August, 2019 FORMATS, Euler Room
08:30–09:00 Opening
09:00–10:00
Keynote: Nathalie Bertrand (room: Euler) (chair: Étienne André)
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
The Timestamp of Timed Automata
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
On the Distance between Timed Automata
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
Martin Tappler, Bernhard K. Aichernig, Kim Guldstrand Larsen and Florian Lorber
Time to Learn - Learning Timed Automata from Tests
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: A Verified Model Checker for Timed Automata [tool paper]
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
Sandboxing Controllers for Stochastic Cyber-Physical Systems
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
Andrea Marin, Carla Piazza and Sabina Rossi
Proportional Lumpability
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
Expected Reachability-Price Games
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

Committees

Program committee

Venue: Amsterdam

Some fancy but useless icons