Orateur : Olga Kouchnarenko (website, scholar), femto-st & INRIA Lille, project team SPIRALS
Titre : Testing Dynamic Reconfigurations of Component-based Systems w.r.t. Adaptation Policies
Résumé : Component systems are designed as sets of components that may reconfigure themselves according to adaptation policies. Adaptation policies are seen as artifacts that describe desirable behavior of the system without enforcing a specific one. An adaptation policy is designed as a set of rules that indicate, for a given set of configurations, which reconfiguration operations can be triggered, with fuzzy values representing their respective utility.
In this context, we present a model-based testing approach which aims to generate large test suites in order to measure the occurrences of reconfigurations and compare them to their utility values specified in the adaptation rules. This process is based on a usage model of the system used to stimulate the system and provoke reconfigurations. As the system may reconfigure dynamically, this online test generator observes the system responses and evolution in order to decide the next appropriate test step to perform. In the end, the relative frequencies of the reconfigurations are measured in order to determine if the adaptation policy is faithfully implemented. The approach is illustrated by simulations for platoons of (semi-)autonomous vehicles.
Orateur : Rim Saddem ( scholar), LIS, equipe Mofed
Titre : Business Processes Meet Spatial Concerns: the sBPMN Verification Framework.
Résumé : BPMN is the standard for business process modeling. It includes a rich set of constructs for control-flow, inter-process communication, and time-related concerns. However, spatial concerns are left apart while being essential to several application domains. We propose a comprehensive extension of BPMN to deal with this. Our proposal includes an integrated notation, a first-order logic semantics of the extension, and tool-supported verification means through the implementation of the semantics in TLA+. Our tool support and our model database are open-source and freely available online.
Orateur : Julie Parreaux ( website), LIS, equipe Move
Titre : Playing Stochastically in Weighted Timed Games to Emulate Memory.
Résumé : Weighted timed games are two-player zero-sum games played in a timed automaton equipped with integer weights. We consider optimal
reachability objectives, in which one of the players, that we call Min, wants to reach a target location while minimising the
cumulated weight. While knowing if Min has a strategy to guarantee a value lower than a given threshold is known to be undecidable (with two or more clocks), several conditions, one of them being the divergence, have been given to recover decidability. In such weighted timed games (like in untimed weighted games in the presence of negative weights), MinPl may need finite memory to play (close to) optimally. This is thus tempting to try to
emulate this finite memory with other strategic capabilities. In this work, we allow the players to use stochastic decisions, both in the choice of transitions and of timing delays. We give for the first time a definition of the expected value in weighted timed games, overcoming several theoretical challenges. We then show that, in divergent weighted timed games, the stochastic value is indeed equal to the classical (deterministic) value, thus proving that Min can guarantee the same value while only using stochastic choices, and no memory. This work is join with Benjamin Monmege and Pierre-Alain Reynier.