Séminaires
Séminaire du 24 mai 2019
Lieu
LRDE amphi 3 : comment y aller 14-16 rue Voltaire 94200 Le Kremlin-Bicetre
Programme
14h00-14h45: Benoît Barbot (LACL): Generation of Signals under Temporal Constraints for CPS Testing
Abstract : 
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.