Laboratoires.Ecoles, Collège et Formation doctorales
Stratégie. Séminaires, colloques. Sciences et société
Réseaux et pôles d'excellence. Investissements d'avenir (Labex)
Holger Hermanns, Saarland University, Germany / LIG
Is it a good idea to ride a bike with a wireless brake ? How to dimension buffer sizes in a NoC ? What availability can be expected for Gallileo IOV ? Might photovoltaic overproduction blow out the European electricity network ? Maybe. Maybe not. Probably ? The era of power-aware, wireless and distributed systems of systems asks for strong quantitative answers to such questions.
This talk introduces a promising attack on this challenge. The approach merges two well-established strands of informatics research and practice : verification of concurrent systems and performance evaluation. Instead of guaranteeing that a system is performing the expected tasks, we are ultimately interested in guaranteeing that the system performs its task within a given time bound and with (energy) costs within a given limit. Or better : that the probability thereof is above a given threshold. This presentation paints the landscape of behavioural models for probability, time, and cost, with a mild focus onconcurrent Markov models and process calculi. It discusses foundational aspects of compositional modelling and model checking such systems, and show how these techniques are applied in different real-life cases.
Updated on:Jan. 1, 2021, midnight
Number of views: