On monday, at 2pm - UPEC CMC - Room P2-131

November 30, 2020

Falsification of Cyber-Physical Systems with Constrained Signal Spaces

Benoît Barbot (LACL)

Falsification has garnered much interest recently as a way to validate complex Cyber-Physical Systems (CPS) designs with respect to a specification expressed via temporal logics. Using their quantitative semantics, the falsification problem can be formulated as a robustness minimization problem. To make this infinite-dimensional problem tractable, a common approach is to restrict to classes of signals that can be defined using a finite number of parameters, such as piecewise-constant or piecewise-linear signals with fixed time intervals.

A drawback of this approach is that when the input signals must satisfy non-trivial temporal constraints, encoding these constraints into bounded domains for parameters can be difficult. In this work, to better capture temporal constraints on the input signal space, we use timed automata (TA) and make use of a transformation that allows sampling TA traces by sampling points in the unit box.

We exploit this transformation to efficiently encode constrained CPS signals in the robustness minimization problem. This transformation also allows us to define an effective coverage measure for the constrained signal space so as to provide quantitative guarantees when no falsifying behaviour is found. Additionally, the coverage measure is used to improve the black-box optimisation performance by detecting situations where the search is stuck near a local optimum. The approach is demonstrated on a modulator and a model of a car automatic transmission subject to constraints that describe usual driving patterns.

November 16, 2020

TBA

Régine Laleau (LACL)

November 2, 2020

TBA

Luc Pellissier (LACL)

October 12, 2020

Simulation et synthèse garantie de Systèmes Cyber-Physiques

Adrien Le Coënt (LACL)

Les systèmes cyber-physiques, faisant interagir des éléments informatiques et des éléments physiques, sont un des modèles majeurs de ces dernières années, pour lesquels la modélisation et la vérification formelle sont encore des challenges actuels.

Les difficultés majeures rencontrées actuellement dans l’étude formelle de ces systèmes sont: 1. La complexité des algorithmes de synthèse, limitant fortement la dimension des systèmes que l’on peut concevoir 2. La difficulté du calcul de l’ensemble atteignable, limitant le type de dynamique continue que l’on peut considérer dans ces modèles.

Nous présenterons des études de cas qui illustrent ces difficultés, et proposerons des méthodes qui tentent de répondre à ces difficultés. Plus précisément, nous proposons une méthode de synthèse compositionnelle qui permet de casser la complexité algorithmique de la recherche de contrôleur. Nous présenterons également comment utiliser une méthode de simulation garantie dans un outil de synthèse de contrôleur.