Formal Modeling and Analysis of Timed Systems

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.

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.

This paper presents the first work that derives robustness criteria on a trace mining approach that constructs arrival-curves models from dataset 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 analysis presented in 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. The result is a methodology to evaluate a system to dynamically changing workloads. We evaluate the proposed approach on an industrial cyber-physical system that generates traces of timestamped QNX events.

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 better chances capturing unexpected behaviors.

We present Mixed-time Signal Temporal Logic (\(\textsc {STL-mx}\)), 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 electronic designs. In \(\textsc {STL-mx}\), 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 evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example.

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 behaviour 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.

With the development of real-time systems and of new wireless communication technologies having strong requirements on latencies and reliability, there is a need to compute deterministic performance bounds in networks. This paper focuses on the performance guarantees and stability conditions of 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 to the detriment 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.

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.

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.

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-difference specifications, 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.

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.

Let \(\mathrm {eNTA}\) be the class of non-deterministic timed automata with silent transitions. Given \(A \in \mathrm {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 \(\mathrm {eNTA}\). We also show that the language of A is periodic with respect to suffixes.

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. In order to tackle this disturbing problem we show how to effectively construct deterministic timed automata \({A}_d\) and \({B}_d\) that are discretizations (digitizations) of the non-deterministic timed automata A and B and differ from the original automata by at most \(\frac{1}{6}\) time units on each occurrence of an event. Language inclusion in the discretized timed automata is decidable and it is also decidable when instead of \(\mathfrak {L}(B)\) we consider \(\overline{\mathfrak {L}(B)}\), the closure of \({\mathfrak {L}(B)}\) in the Euclidean topology: if \(\mathfrak {L}({A}_d) \nsubseteq \mathfrak {L}({B}_d)\) then \(\mathfrak {L}(A) \nsubseteq \mathfrak {L}(B)\) and if \(\mathfrak {L}({A}_d) \subseteq \mathfrak {L}({B}_d)\) then \(\mathfrak {L}(A) \subseteq \overline{\mathfrak {L}(B)}\).

Moreover, if \(\mathfrak {L}({A}_d) \nsubseteq \mathfrak {L}({B}_d)\) we would like to know how far away is \(\mathfrak {L}({A}_d)\) from being included in \(\mathfrak {L}({B}_d)\). For that matter we define the distance between the languages of 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 finite or infinite.

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 \(\mathbf {44}\) timed systems, comprised of four systems from the literature (two industrial and two academic) and \(\mathbf {40}\) randomly generated examples.

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.

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.

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 players, player \(\text {Min}\) and player \(\text {Max}\), move a token along the infinite configuration space of PTA. The objective of player \(\text {Min}\) is to minimize the expected price to reach a target location, while the goal of the \(\text {Max}\) player is the opposite. The undecidability of computing the value in the expected reachability-price games follows from the undecidability of the corresponding problem on timed automata. A key contribution of this work is a characterization of sufficient conditions under which an expected reachability-price game can be reduced to a stochastic game on a stochastic generalization of corner-point abstraction (a well-known finitary abstraction of timed automata). Exploiting this result, we show that expected reachability-price games for PTA with single clock and price-rates restricted to \(\{ 0, 1 \}\) are decidable.