20 May
2019
20 May
'19
11:10 a.m.
========================================================================
Séminaire MeFoSyLoMa
http://www.mefosyloma.fr/
Méthodes Formelles pour les Systèmes Logiciels et Matériels
vendredi 24 mai 2019, 14h-16h30
Adresse:
Amphi 3
14-16 rue Voltaire, 94270 Le Kremlin-Bicêtre
Métro Porte d'Italie
Plans d'accès :
https://www.google.com/maps/place/14+Rue+Voltaire,+94270+Le+Kremlin-Bicêtre/
https://www.lrde.epita.fr/~adl/dl/acces-amphi3.png
S'il y en a parmi vous qui comptent venir en voiture, le parking du
centre commercial Okabé est gratuit pendant 3h.
http://www.okabe.com/okabe/fr/okabe-parking
========================================================================
Le séminaire MeFoSyLoMa est animé conjointement par les laboratoires
Cedric (Cnam), IBISC (Univ. Evry), LACL (Univ. Paris 12), LIP6 (UPMC),
LIPN (Univ. Paris 13), LRDE (Epita), LSV (École Normale Supérieure de
Cachan) et LTCI (TELECOM ParisTech). Son objet est de permettre la
confrontation de différentes approches ou points de vue sur
l'utilisation des méthodes formelles dans les domaines du génie
logiciel, de la conception de circuit, des systèmes répartis, des
systèmes temps-réel ou encore des systèmes d'information. Il
s'organise autour de réunions bimestrielles où sont exposés des
travaux de recherche récents sur ce thème.
========================================================================
Programme
14h00-14h45: Benoît Barbot (LACL)
Generation of Signals under Temporal Constraints for CPS Testing
This work is concerned with validation of cyber-physical systems (CPS)
via simulation based on sampling of the input signal space. Such a
space is infinite and in general too difficult to treat symbolically
meaning that the only reasonable option is to sample a finite subset
of it and simulate the corresponding system behaviours. It is thus of
great interest to choose a finite sample so that it best "covers" the
whole space of input signals. We use timed automata to model temporal
constraints, in order to avoid spurious bugs coming from unrealistic
inputs and this can also reduce the input space to explore. We propose
a method for low discrepancy generation of signals with temporal
constraints recognised by timed automata. The discrepancy notion
reflects how uniform the input signal space is sampled and
additionally allows deriving validation and performance guarantees. We
also show how this notion can be used to measure the discrepancy of a
given set of input signals. We describe a prototype tool chain and
demonstrate the proposed methods on a Kinetic Battery Model (KiBaM)
and a Sigma Delta modulator.
14h45-15h30 : Alexandre Duret-Lutz (LRDE)
Generic Emptiness Check for Fun and Profit
Abstract: We present a new algorithm for checking the emptiness of
ω-automata with an Emerson-Lei acceptance condition (i.e., a positive
Boolean formula over sets of states or transitions that must be
visited infinitely or finitely often). The algorithm can also solve
the model checking problem of probabilistic positiveness of MDP under
a property given as a deterministic Emerson-Lei automaton. Although
these problems are known to be NP-complete and our algorithm is
exponential in general, it runs in polynomial time for simpler
acceptance conditions like generalized Rabin, Streett, or parity. In
fact, the algorithm provides a unifying view on emptiness checks for
these simpler automata classes. We have implemented the algorithm in
Spot and PRISM and our experiments show improved performance over
previous solutions.
Joint work with C. Baier, F. Blahoudek, J. Klein, D. Müller, and
J. Strejček.
15h30-16h00: pause café
16h00-16h30: vie du groupe
========================================================================
--
Alexandre Duret-Lutz
