Seminars

Systems that interact synchronously with an unpredictable environment are usually captured by zero-sum concurrent games. In such games, randomised strategies are in general more powerful than deterministic ones. Such systems, however, do not capture faithfully decentralised systems that cannot resort to a common private source of randomness. In this talk, I will introduce dicey games, a model for games played by teams, where the structure of randomness sources accessible to each player is explicitly specified.

Abstract: Event-B provides a rigorous method for ensuring functional safety of cyber-physical systems. However, it lacks native support for temporal aspects. Therefore, we propose a novel methodology using Parametric Timed Automata (PTA) as a formalism to systematically generate Event-B models with integrated temporal constraints. This generated model captures the temporal aspects and a partial functional specification, which is then improved with the remaining functional requirements. This approach significantly reduces manual effort in developing formally verified cyber-physical systems while ensuring both functional correctness and temporal safety properties through automated constraint synthesis and formal proof obligations.