Formal Modeling and Analysis of Timed Systems

Hybrid systems are a powerful formalism for modeling and reasoning about cyber-physical systems. They mix the continuous and discrete natures of the evolution of computerized systems. Switched systems are a special kind of hybrid systems, with restricted discrete behaviours: those systems only have finitely many different modes of (continuous) evolution, with isolated switches between modes. Such systems provide a good balance between expressiveness and controllability, and are thus in widespread use in large branches of industry such as power electronics and automotive control. The control law for a switched system defines the way of selecting the modes during the run of the system. Controllability is the problem of (automatically) synthesizing a control law in order to satisfy a desired property, such as safety (maintaining the variables within a given zone) or stabilisation (confinement of the variables in a close neighborhood around an objective point). In order to compute the control of a switched system, we need to compute the solutions of the differential equations governing the modes. Euler’s method is the most basic technique for approximating such solutions. We present here an estimation of the Euler’s method local error, using the notion of “one-sided Lispchitz constant” for modes. This yields a general control synthesis approach which can encompass several features such as bounded disturbance and compositionality.

Networks of timed automata are a widely used formalism to model timed systems. Models are often concise and convenient since timed automata abstract from many details of actual implementations. One such abstraction is that the semantics of networks of timed automata introduces an implicit global scheduler which blocks edges which are sending on a channel until a matching receiving edge is enabled. When models are used a priori, that is, to develop, e.g., a communication protocol which is supposed to have a (non-shared memory) distributed implementation, a corresponding global scheduler is not desired.

To facilitate distributed implementations of timed automata models, we introduce a new class of networks of timed automata whose behaviour does not depend on the blocking of sending edges. We show that the membership problem for this new class of networks of timed automata is decidable and evaluate our new decision procedure.

This paper studies optimal time-bounded control in multi-mode systems with discrete costs. Multi-mode systems are an important subclass of linear hybrid systems, in which there are no guards on transitions and all invariants are global. Each state has a continuous cost attached to it, which is linear in the sojourn time, while a discrete cost is attached to each transition taken. We show that an optimal control for this model can be computed in NExpTime and approximated in PSpace. We also show that the one-dimensional case is simpler: although the problem is NP-complete (and in LogSpace for an infinite time horizon), we develop an FPTAS for finding an approximate solution.

Zonotopes are a useful set representation for bounded time reach set computation of affine hybrid systems because of their closure under Minkowski sum and matrix multiplication operations. For unbounded time reach set approximation of arbitrarily switched affine hybrid systems, template complex zonotopes and a corresponding invariant computation procedure were introduced, which utilized the possibly complex eigenstructure of the affine maps. But a major hurdle in extending the technique for computing invariants of more general affine hybrid systems, where switching is state dependent and controlled by linear constraints, is that the class of template complex zonotopes is not closed under intersection with linear constraints. In this paper, we use a more expressive set representation called augmented complex zonotopes, for which we propose an algebraic over-approximation of the intersection with linear constraints. This over-approximation is then used to derive a set of second order conic constraints for computing an augmented complex zonotopic positive invariant for discrete time affine hybrid systems with additive disturbance input and linear safety constraints. We demonstrate the efficiency of this approach by experimenting on some benchmark examples.

Despite researchers’ efforts in the last couple of decades, reachability analysis is still a challenging problem even for linear hybrid systems. Among the existing approaches, the most practical ones are mainly based on bounded-time reachable set over-approximations. For the purpose of unbounded-time analysis, one important strategy is to abstract the original system and find an invariant for the abstraction. In this paper, we propose an approach to constructing a new kind of abstraction called conic abstraction for affine hybrid systems, and to computing reachable sets based on this abstraction. The essential feature of a conic abstraction is that it partitions the state space of a system into a set of convex polyhedral cones which is derived from a uniform conic partition of the derivative space. Such a set of polyhedral cones is able to cut all trajectories of the system into almost straight segments so that every segment of a reach pipe in a polyhedral cone tends to be straight as well, and hence can be over-approximated tightly by polyhedra using similar techniques as HyTech or PHAVer. In particular, for diagonalizable affine systems, our approach can guarantee to find an invariant for unbounded reachable sets, which is beyond the capability of bounded-time reachability analysis tools. We implemented the approach in a tool and experiments on benchmarks show that our approach is more powerful than SpaceEx and PHAVer in dealing with diagonalizable systems.

A promising technique for the formal verification of embedded and cyber-physical systems is flow-pipe construction, which creates a sequence of regions covering all reachable states over time. Flow-pipe construction methods can check whether specifications are met for all states, rather than just testing using a finite and incomplete set of simulation traces. A fundamental challenge when using flow-pipe construction on high-dimensional systems is the cost of geometric operations, such as intersection and convex hull. We address this challenge by showing that it is often possible to remove the need to perform high-dimensional geometric operations by combining two model transformations, direct time-triggered conversion and dynamics scaling. Further, we prove the overapproximation error in the conversion can be made arbitrarily small. Finally, we show that our transformation-based approach enables the analysis of a drivetrain system with up to 51 dimensions.

We consider the problem of model-checking a subset of probabilistic CTL, interpreted over (discrete-time) Markov reward models, allowing the specification of lower bounds on the probability of the set of paths satisfying a cost-bounded path formula. We first consider a reduction to fixed-point computations on a graph structure that encodes a division of the problem into smaller sub-problems by explicit unfolding of the given formula into sub-formulae. Although correct, the size of the graph constructed is highly dependent on the size of the cost bound. To this end, we provide a symbolic extension, effectively ensuring independence between the size of the graph and the cost-bound.

In this paper we propose a (sub)distribution-based bisimulation for labelled Markov processes and compare it with earlier definitions of state and event bisimulation, which both only compare states. In contrast to those state-based bisimulations, our distribution bisimulation is weaker, but corresponds more closely to linear properties. We construct a logic and a metric to describe our distribution bisimulation and discuss linearity, continuity and compositional properties.

Signal regular expressions can specify sequential properties of real-valued signals based on threshold conditions, regular operations, and duration constraints. In this paper we endow them with a quantitative semantics which indicates how robustly a signal matches or does not match a given expression. First, we show that this semantics is a safe approximation of a distance between the signal and the language defined by the expression. Then, we consider the robust matching problem, that is, computing the quantitative semantics of every segment of a given signal relative to an expression. We present an algorithm that solves this problem for piecewise-constant and piecewise-linear signals and show that for such signals the robustness map is a piecewise-linear function. The availability of an indicator describing how robustly a signal segment matches some regular pattern provides a general framework for quantitative monitoring of cyber-physical systems.

We define a new notion of satisfaction of a temporal logic formula \(\varphi \) by a behavior w. This notion, denoted by \((w,t,t')\,\models \, \varphi \), is characterized by two time parameters: the position t from which satisfaction is considered, and the end of the (finite) behavior \(t'\) which indicates how much do we know about the behavior. We define this notion in dense time where \(\varphi \) is a formula in the future fragment of metric temporal logic (MTL) and w is a Boolean signal of bounded variability. We show that the set of all pairs \((t,t')\) such that \((w,t,t')\,\models \, \varphi \) can be expressed as a finite union of two-dimensional zones and give an effective procedure to compute it.

The timed pattern matching problem is an actively studied topic because of its relevance in monitoring of real-time systems. There one is given a log w and a specification \(\mathcal {A}\) (given by a timed word and a timed automaton in this paper), and one wishes to return the set of intervals for which the log w, when restricted to the interval, satisfies the specification \(\mathcal {A}\). In our previous work we presented an efficient timed pattern matching algorithm: it adopts a skipping mechanism inspired by the classic Boyer–Moore (BM) string matching algorithm. In this work we tackle the problem of online timed pattern matching, towards embedded applications where it is vital to process a vast amount of incoming data in a timely manner. Specifically, we start with the Franek-Jennings-Smyth (FJS) string matching algorithm—a recent variant of the BM algorithm—and extend it to timed pattern matching. Our experiments indicate the efficiency of our FJS-type algorithm in online and offline timed pattern matching.

In a recent work we proposed an algorithm for reachability analysis in distributed systems modeled as networks of automata. The main interest of this algorithm is that it performs its analysis in a lazy way: decision is done by only taking into account the automata potentially involved in a path to the reachability goal. This new work extends the approach to networks of timed automata, lazily considering the automata but also lazily adding the clocks to the analysis, which implies not only to consider clocks tested along the paths to the goal, but also to deal with the special issues due to urgency and shared clocks. We have implemented our approach as a tool and provide some interesting experimental results, in a comparison with the model-checker Uppaal.

To solve the reachability problem for timed automata, model checkers usually apply forward search and zone abstraction. To ensure efficiency and termination, the computed zones are generalized using maximal constants obtained from guards either by static analysis or lazily for a given path. In this paper, we propose a lazy method based on zone abstraction that, instead of the constants in guards, considers the constraints themselves. The method is a combination of forward search, backward search and interpolation over zones: if the zone abstraction is too coarse, we propagate a zone representing bad states backwards using backward search, and use interpolation to extract a relevant zone to strengthen the current abstraction. We propose two refinement strategies in this framework, and evaluate our method on the usual benchmark models for timed automata. Our experiments show that the proposed method compares favorably to known methods based on efficient lazy non-convex abstractions.

Delays in feedback control loop, as induced by networked distributed control schemes, may have detrimental effects on control performance. This induces an interest in safety verification of delay differential equations (DDEs) used as a model of embedded control. This article explores reachable-set computation for a class of DDEs featuring a local homeomorphism property. This topological property facilitates construction of over- and under-approximations of their full reachable sets by performing reachability analysis on the boundaries of their initial sets, thereby permitting an efficient lifting of reach-set computation methods for ODEs to DDEs. Membership in this class of DDEs is determined by conducting sensitivity analysis of the solution mapping with respect to the initial states to impose a bound constraint on the time-lag term. We then generalize boundary-based reachability analysis to such DDEs. Our reachability algorithm is iterative along the time axis and the computations in each iteration are performed in two steps. The first step computes an enclosure of the set of states reachable from the boundary of the step’s initial state set. The second step derives an over- and under-approximations of the full reachable set by including (excluding, resp.) the obtained boundary enclosure from certain convex combinations of points in that boundary enclosure. Experiments on two illustrative examples demonstrate the efficacy of our algorithm.

In this paper, we present an algorithm for synthesizing certificates for safety of continuous time dynamical systems, so-called barrier certificates. Unlike the usual approach of using constraint solvers to compute the certificate from the system dynamics, we synthesize the certificate from system simulations. This makes the algorithm applicable even in cases where the dynamics is either not explicitly available, or too complicated to be analyzed by constraint solvers, for example, due to the presence of transcendental function symbols.

The algorithm itself allows the usage of heuristic techniques in which case it does not formally guarantee correctness of the result. However, in cases that do allow rigorous constraint solving, the computed barrier certificate can be rigorously verified, if desired. Hence, in such cases, our algorithm reduces the problem of finding a barrier certificate to the problem of formally verifying a given barrier certificate.

TESL addresses the specification of the temporal aspects of an architectural composition language that allows the composition of timed subsystems. TESL specifies the synchronization points between events and time scales. Methodologically, subsystems having potentially different models of execution are abstracted to their interfaces expressed in terms of timed events.

In this paper, we present an operational semantics of TESL for constructing symbolic traces that can be used in an online-test scenario: the symbolic trace containing a set of constraints over time-stamps and occurrences of events is matched against concrete runs of the system.

We present the operational rules for building symbolic traces and illustrate them with examples. Finally, we show a prototype implementation that generates symbolic traces, and its use for testing.

Today’s Real-Time Systems’ (RTSs) increasing speed and complexity make debugging of timing related faults one of the most challenging engineering tasks. Debugging starts with capturing the fault symptoms, which requires continuous cycle-accurate execution traces. However, due to limitations of on-chip buffers’ area and output ports’ throughput, these cannot be obtained easily.

This paper introduces an approach that divides the tracing into two tasks, monitoring on-chip execution to retrieve accurate timing information and high level functional simulation to retrieve signal contents. A semi-formal cycle-accurate reconstruction method uses these two sources to retrieve a complete, cycle-accurate trace of a given signal. An experiment illustrates how this method allows the cycle-accurate reconstruction of on-chip traces of a Real-Time Autonomous-Guided-Vehicle software.