Gandalf 2018

Title Rigorous System Design: The BIP Framework

Abstract Rigorous system design requires the use of a single powerful component framework allowing the representation of the designed system at different levels of detail, from application software to its implementation. This is essential for ensuring the overall coherency and correctness. This talk introduces a rigorous design flow based on the BIP (Behavior, Interaction, Priority) component framework. This design flow relies on several, tool-supported, source-to-source transformations allowing to progressively and correctly transform high level application software towards efficient implementations for specific platforms.

Title On the Synthesis of Equilibria in Graph Games

Abstract In this invited talk, we focus on games played on graphs by several players who aim at satisfying their objective. We survey and discuss several solution concepts useful for the synthesis of systems, the most famous one being the notion of Nash equilibrium. We present several results about their existence (possibly constrained by some conditions on the payoffs), the objectives of the players being qualitative or quantitative. We also provide some illustrative examples as well as intuitions on the proofs.

Title Energy Timed Automata and Games

Abstract The first part of the talk will provide an overview of the results obtained over the last 10 years when considering Timed Automata and Timed Games extended with continuous variables (cost) that may evolve with different (positive or negative) weights with particular interest in infinite energy-bounded runs/strategies. In the second part we review recent results obtained for a subclass called Segmented Energy Timed Games, where we have decidability, thus allowing for the automatic synthesis of robust and optimal energy-aware controllers. We prove decidability of the energy-constrained infinite run problem in settings with both certainty and uncertainty of the energy-rates. We also consider the optimization problem of identifying the minimal upper bound that will permit existence of infinite energy constrained runs. Our algorithms are based on quantifier elimination for linear real arithmetic. Using Mathematica and Mjollnir, we illustrate our framework through a real industrial example of a hydraulic oil pump. Compared with previous approaches our method is completely automated and provides significantly improved results.

Title Battery-Aware Scheduling in Low Orbit - The GomX-3 Case

Abstract For a satellite in orbit all resources are sparse and the most critical resource of all is power. It is therefore crucial to have detailed knowledge on how much power is available for an energy harvesting satellite in orbit at every time – especially when in eclipse, where it draws its power from onboard batteries. This paper addresses this problem by a two-step procedure to perform task scheduling for low-earth-orbit (LEO) satellites exploiting formal methods. It combines cost-optimal reachability analyses of priced timed automata networks with a realistic kinetic battery model capable of capturing capacity limits as well as stochastic fluctuations. The procedure has been used for the automatic and resource-optimal day-ahead scheduling of GomX-3, a power-hungry nanosatellite currently orbiting the earth. We explain how this approach has overcome existing problems, has led to improved designs, and has provided new insights.