LRDE amphi 0 : comment y aller 14-16 rue Voltaire 94200 Le Kremlin-Bicetre
Abstract : Clearsy has been working with formal method in the railway industry for 20 years. We present here some of this work with Atelier B : formal development, hardware implementation, and formal system analysis.
Abstract : In 2024 at QEST+FORMATS 2024, Rino, Foughali and Asarin proposed a new robustness measure for a subset of STLs based on a new distance on timed signals. We extend this work by implementing the algorithms given there and using this measure to compare different insulin controllers for diabetic patients.
Abstract : Parametric Timed Games (PTG) are an extension of the model of Timed Automata. They allow for the verification and synthesis of real-time systems, reactive to their environment and depending on adjustable parameters. Given a PTG and a reachability objective, we synthesize the values of the parameters such that the game is winning for the controller. We adapt and implement the On-The-Fly algorithm for parameter synthesis for PTG. Several pruning heuristics are introduced, to improve termination and speed of the algorithm. We evaluate the feasibility of parameter synthesis for PTG on two large case studies. Finally, we investigate the correctness guarantee of the algorithm: though the problem is undecidable, our semi-algorithm produces all correct parameter valuations “in the limit”.
