9h-9h30 Olga Kouchnarenko: ADAPT - objectives and work plan
9h30-10h15 Benoît Piranda: Modular robots and their simulation with VisibleSim
10h30-11h15 Frédéric Lassabe : MRs case study: Programmable and interactive Blinky Blocks
11h15-12h Sophie Cerf: On the control of computer systems and software
13h00-13h45 Marius Bozga: A Layered Implementation of DR-BIP Supporting Run-Time Monitoring and Analysis Reconfigurable systems are emerging in many application domains as reconfiguration can be used to cope with unpredictable system environments and adapt by delivering new functionality. The Dynamic Reconfigurable BIP (DRBIP) framework is an extension of the BIP component framework enriched with dynamic exogenous reconfiguration primitives, intended to support modeling and validation of reconfigurable systems. I'll present the two-layered implementation of DRBIP clearly separating between execution of reconfiguration operations and execution of a fixed system configuration and discuss its benefits for analysis and verification.
13h45-14h30h Radu Iosif: Self-Adapting Networks We introduce a simple formal model to reason about the behaviors of self-adapting (reconfigurable) networks. The proofs of correctness of reconfiguration programs are done using a separation logic and a Hoare-style local reasoning proof system that produces proof obligations in the form of logical entailments. In particular, entailments are used to reason about invariance of assertions under interaction events (synchronous communication). In the second part of the talk, I will present some advances in deciding the validity of entailments in the dialect of separation logic used to model distributed networks.
14h30-15h15 Thao Dang: Set-based and trajectory-based analysis of hybrid systems In order to account for non-determinism in hybrid systems, set-based computation has become a de facto approach. Exact reachable set computation is however proven to be impossible for most non-trivial hybrid systems, and alternatively, much research has focused on developing set representations that can be efficiently manipulated to compute sufficiently accurate over-approximation of the reachable set. On the other hand, another approach, called trajectory-based, focuses on generating a number of single trajectories in a way that they allow deriving formal guarantees for all the trajectories of the system. This approach requires a notion of “goodness” of a set of trajectories with respect to the guarantee of interest. In this presentation we give a summary of the main results of these two approaches.
15h30-16h15 Daniel Romero: PowerAPI or How to measure the software power consumption
16h15-17h: Discussion and conclusion
March 15th: FEMTO-ST, Bouloie site, room 404C
Working group WP0: Data collection and aggregation for modular robots and their motifs (leader: FEMTO-ST)
9h00-9h45 Antonios Shokry: On BB-systems' energy consumption: First measuments and observations
9h45-10h30 Nathan Gallone: Aggregate programming and control theorie in the IoT domain, application to Blinky Blocks
