arXiv subjects

Étienne André

Publications and source records attributed to Étienne André.

At least 37 records · Page 2Linked to original sources

arXiv2024

Parameterized Verification of Disjunctive Timed Networks

We introduce new techniques for the parameterized verification of disjunctive timed networks (DTNs), i.e., networks of timed automata (TAs) that communicate via location guards that enable a transition only if there is another process in a given location. This computational model has been considered in the literature before, example applications are gossiping clock synchronization protocols or planning problems. We address the minimum-time reachability problem (Minreach) in DTNs, and show how to efficiently solve it based on a novel zone graph algorithm. We further show that solving Minreach allows us to construct a summary TA capturing exactly the possible behaviors of a single TA within a DTN of arbitrary size. The combination of these two results enables the parameterized verification of DTNs, while avoiding the construction of an exponential-size cutoff system required by existing results. Additionally, we develop sufficient conditions for solving Minreach and parameterized verification problems even in certain cases where locations that appear in location guards can have clock invariants, a case that has usually been excluded in the literature. Our techniques are also implemented, and experiments show their practicality.

cs.LO↗

arXiv2023

Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata

Timing information leakage occurs whenever an attacker successfully deduces confidential internal information by observing some timed information such as events with timestamps. Timed automata are an extension of finite-state automata with a set of clocks evolving linearly and that can be tested or reset, making this formalism able to reason on systems involving concurrency and timing constraints. In this paper, we summarize a recent line of works using timed automata as the input formalism, in which we assume that the attacker has access (only) to the system execution time. First, we address the following execution-time opacity problem: given a timed system modeled by a timed automaton, given a secret location and a final location, synthesize the execution times from the initial location to the final location for which one cannot deduce whether the secret location was visited. This means that for any such execution time, the system is opaque: either the final location is not reachable, or it is reachable with that execution time for both a run visiting and a run not visiting the secret location. We also address the full execution-time opacity problem, asking whether the system is opaque for all execution times; we also study a weak counterpart. Second, we add timing parameters, which are a way to configure a system: we identify a subclass of parametric timed automata with some decidability results. In addition, we devise a semi-algorithm for synthesizing timing parameter valuations guaranteeing that the resulting system is opaque. Third, we report on problems when the secret has itself an expiration date, thus defining expiring execution-time opacity problems. We finally show that our method can also apply to program analysis with configurable internal timings.

cs.LO↗

arXiv2022

Efficient Convex Zone Merging in Parametric Timed Automata

Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. We present here different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while preserving the correctness of verification and synthesis results. We perform extensive experiments, and identify the best heuristics in practice, bringing a significant decrease in the computation time on a benchmarks library.

cs.FL↗

arXiv2022

strategFTO: Untimed control for timed opacity

We introduce a prototype tool strategFTO addressing the verification of a security property in critical software. We consider a recent definition of timed opacity where an attacker aims to deduce some secret while having access only to the total execution time. The system, here modeled by timed automata, is deemed opaque if for any execution time, there are either no corresponding runs, or both public and private corresponding runs. We focus on the untimed control problem: exhibiting a controller, i.e., a set of allowed actions, such that the system restricted to those actions is fully timed-opaque. We first show that this problem is not more complex than the full timed opacity problem, and then we propose an algorithm, implemented and evaluated in practice.

cs.CR↗

arXiv2022

Guaranteeing Timed Opacity using Parametric Timed Model Checking

Information leakage can have dramatic consequences on systems security. Among harmful information leaks, the timing information leakage occurs whenever an attacker successfully deduces confidential internal information. In this work, we consider that the attacker has access (only) to the system execution time. We address the following timed opacity problem: given a timed system, a private location and a final location, synthesize the execution times from the initial location to the final location for which one cannot deduce whether the system went through the private location. We also consider the full timed opacity problem, asking whether the system is opaque for all execution times. We show that these problems are decidable for timed automata (TAs) but become undecidable when one adds parameters, yielding parametric timed automata (PTAs). We identify a subclass with some decidability results. We then devise an algorithm for synthesizing PTAs parameter valuations guaranteeing that the resulting TA is opaque. We finally show that our method can also apply to program analysis.

cs.CR↗

arXiv2022

Timed automata as a formalism for expressing security: A survey on theory and practice

Timed automata are a common formalism for the verification of concurrent systems subject to timing constraints. They extend finite-state automata with clocks, that constrain the system behavior in locations, and to take transitions. While timed automata were originally designed for safety (in the wide sense of correctness w.r.t. a formal property), they were progressively used in a number of works to guarantee security properties. In this work, we review works studying security properties for timed automata in the last two decades. We notably review theoretical works, with a particular focus on opacity, as well as more practical works, with a particular focus on attack trees and their extensions. We derive main conclusions concerning open perspectives, as well as tool support.

cs.CR↗

arXiv2022

Zone extrapolations in parametric timed automata

Timed automata (TAs) are an efficient formalism to model and verify systems with hard timing constraints, and concurrency. While TAs assume exact timing constants with infinite precision, parametric TAs (PTAs) leverage this limitation and increase their expressiveness, at the cost of undecidability. A practical explanation for the efficiency of TAs is zone extrapolation, where clock valuations beyond a given constant are considered equivalent. This concept cannot be easily extended to PTAs, due to the fact that parameters can be unbounded. In this work, we propose several definitions of extrapolation for PTAs based on the M-extrapolation, and we study their correctness. Our experiments show an overall decrease of the computation time and, most importantly, allow termination of some previously unsolvable benchmarks.

cs.FL↗

arXiv2022

Exemplifying parametric timed specifications over signals with bounded behavior

Specifying properties can be challenging work. In this paper, we propose an automated approach to exemplify properties given in the form of automata extended with timing constraints and timing parameters, and that can also encode constraints over real-valued signals. That is, given such a specification and given an admissible automaton for each signal, we output concrete runs exemplifying real (or impossible) runs for this specification. Specifically, our method takes as input a specification, and a set of admissible behaviors, all given as a subclass of rectangular hybrid automata, namely timed automata extended with arbitrary clock rates, signal constraints, and timing parameters. Our method then generates concrete runs exemplifying the specification.

cs.FL↗

arXiv2022

Reachability and liveness in parametric timed automata

We study timed systems in which some timing features are unknown parameters. Parametric timed automata (PTAs) are a classical formalism for such systems but for which most interesting problems are undecidable. Notably, the parametric reachability emptiness problem, i.e., the emptiness of the parameter valuations set allowing to reach some given discrete state, is undecidable. Lower-bound/upper-bound parametric timed automata (L/U-PTAs) achieve decidability for reachability properties by enforcing a separation of parameters used as upper bounds in the automaton constraints, and those used as lower bounds. In this paper, we first study reachability. We exhibit a subclass of PTAs (namely integer-points PTAs) with bounded rational-valued parameters for which the parametric reachability emptiness problem is decidable. Using this class, we present further results improving the boundary between decidability and undecidability for PTAs and their subclasses such as L/U-PTAs. We then study liveness. We prove that: (1) deciding the existence of at least one parameter valuation for which there exists an infinite run in an L/U-PTA is PSpace-complete; (2) the existence of a parameter valuation such that the system has a deadlock is however undecidable; (3) the problem of the existence of a valuation for which a run remains in a given set of locations exhibits a very thin border between decidability and undecidability.

cs.LO↗

arXiv2021

Parametric schedulability analysis of a launcher flight control system under reactivity constraints

The next generation of space systems will have to achieve more and more complex missions. In order to master the development cost and duration of such systems, an alternative to a manual design is to automatically synthesize the main parameters of the system. In this paper, we present an approach for the specific case of the scheduling of the flight control of a space launcher. The approach requires two successive steps: (1) the formalization of the problem to be solved in a parametric formal model and (2) the synthesis of the model parameters with a tool. We first describe the problem of the scheduling of a launcher flight control, then we show how this problem can be formalized with parametric stopwatch automata; we then present the results computed by the parametric timed model checker IMITATOR. We enhance our model by taking into consideration the time for switching context, and we compare the results to those obtained by other tools classically used in scheduling.

cs.SE↗

arXiv2021

A Benchmarks Library for Extended Parametric Timed Automata

Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. In order to test the efficiency of new algorithms, a fair set of benchmarks is required. We present an extension of the IMITATOR benchmarks library, that accumulated over the years a number of case studies from academic and industrial contexts. We extend here the library with several dozens of new benchmarks; these benchmarks highlight several new features: liveness properties, extensions of (parametric) timed automata (including stopwatches or multi-rate clocks), and unsolvable toy benchmarks. These latter additions help to emphasize the limits of state-of-the-art parameter synthesis techniques, with the hope to develop new dedicated algorithms in the future.

cs.LO↗

arXiv2021

Parametric updates in parametric timed automata

We introduce a new class of Parametric Timed Automata (PTAs) where we allow clocks to be compared to parameters in guards, as in classic PTAs, but also to be updated to parameters. We focus here on the EF-emptiness problem: "is the set of parameter valuations for which some given location is reachable in the instantiated timed automaton empty?". This problem is well-known to be undecidable for PTAs, and so it is for our extension. Nonetheless, if we update all clocks each time we compare a clock with a parameter and each time we update a clock to a parameter, we obtain a syntactic subclass for which we can decide the EF-emptiness problem and even perform the exact synthesis of the set of rational valuations such that a given location is reachable. To the best of our knowledge, this is the first non-trivial subclass of PTAs, actually even extended with parametric updates, for which this is possible.

cs.FL↗

arXiv2021

Robust optimal periodic control using guaranteed Euler's method

In this paper, we consider the application of optimal periodic control sequences to switched dynamical systems. The control sequence is obtained using a finite-horizon optimal method based on dynamic programming. We then consider Euler approximate solutions for the system extended with bounded perturbations. The main result gives a simple condition on the perturbed system for guaranteeing the existence of a stable limit cycle of the unperturbed system. An illustrative numerical example is provided which demonstrates the applicability of the method.

eess.SY↗

arXiv2020

Parametric non-interference in timed automata

We consider a notion of non-interference for timed automata (TAs) that allows to quantify the frequency of an attack; that is, we infer values of the minimal time between two consecutive actions of the attacker, so that (s)he disturbs the set of reachable locations. We also synthesize valuations for the timing constants of the TA (seen as parameters) guaranteeing non-interference. We show that this can reduce to reachability synthesis in parametric timed automata. We apply our method to a model of the Fischer mutual exclusion protocol and obtain preliminary results.

cs.FL↗

arXiv2020

Robust optimal control using dynamic programming and guaranteed Euler's method

Set-based integration methods allow to prove properties of differential systems, which take into account bounded disturbances. The systems (either time-discrete, time-continuous or hybrid) satisfying such properties are said to be "robust". In the context of optimal control synthesis, the set-based methods are generally extensions of numerical optimal methods of two classes: first, methods based on convex optimization; second, methods based on the dynamic programming principle. Heymann et al. have recently shown that, for certain systems of low dimension, the second numerical method can give better solutions than the first one. They have built a solver (Bocop) that implements both numerical methods. We show in this paper that a set-based extension of a method of the second class which uses a guaranteed Euler integration method, allows us to find such good solutions. Besides, these solutions enjoy the property of robustness against uncertainties on initial conditions and bounded disturbances. We demonstrate the practical interest of our method on an example taken from the numerical Bocop solver. We also give a variant of our method, inspired by the method of Model Predictive Control, that allows us to find more efficiently an optimal control at the price of losing robustness.

eess.SY↗

arXiv2020

Guaranteed phase synchronization of hybrid oscillators using symbolic Euler's method: The Brusselator and biped examples

The phenomenon of phase synchronization was evidenced in the 17th century by Huygens while observing two pendulums of clocks leaning against the same wall. This phenomenon has more recently appeared as a widespread phenomenon in nature, and turns out to have multiple industrial applications. The exact parameter values of the system for which the phenomenon manifests itself are however delicate to obtain in general, and it is interesting to find formal sufficient conditions to guarantee phase synchronization. Using the notion of reachability, we give here such a formal method. More precisely, our method selects a portion $S$ of the state space, and shows that any solution starting at $S$ returns to $S$ within a fixed number of periods $k$. Besides, our method shows that the components of the solution are then (almost) in phase. We explain how the method applies on the Brusselator reaction-diffusion and the biped walker examples.

eess.SY↗

arXiv2020

Automated synthesis of local time requirement for service composition

Service composition aims at achieving a business goal by composing existing service-based applications or components. The response time of a service is crucial especially in time critical business environments, which is often stated as a clause in service level agreements between service providers and service users. To meet the guaranteed response time requirement of a composite service, it is important to select a feasible set of component services such that their response time will collectively satisfy the response time requirement of the composite service. In this work, we use the BPEL modeling language, that aims at specifying Web services. We extend it with timing parameters, and equip it with a formal semantics. Then, we propose a fully automated approach to synthesize the response time requirement of component services modeled using BPEL, in the form of a constraint on the local response times. The synthesized requirement will guarantee the satisfaction of the global response time requirement, statically or dynamically. We implemented our work into a tool, Selamat, and performed several experiments to evaluate the validity of our approach.

cs.SE↗

arXiv2020

Language Preservation Problems in Parametric Timed Automata

Parametric timed automata (PTA) are a powerful formalism to model and reason about concurrent systems with some unknown timing delays. In this paper, we address the (untimed) language- and trace-preservation problems: given a reference parameter valuation, does there exist another parameter valuation with the same untimed language, or with the same set of traces? We show that these problems are undecidable both for general PTA and for the restricted class of L/U-PTA, even for integer-valued parameters, or over bounded time. On the other hand, we exhibit decidable subclasses: 1-clock PTA, and 1-parameter deterministic L-PTA and U-PTA. We also consider robust versions of these problems, where we additionally require that the language be preserved for all valuations between the reference valuation and the new valuation.

cs.LO↗