To Appear

We consider the synthesis problem on timed automata with Büchi objectives, where delay choices made by a controller are perturbed by a small amount.
Usually, the controller needs to avoid punctual guards, such as testing the equality of a clock to a constant. In this work, we extend existing results to a robustness setting that allows for punctual transitions in the automaton to be taken by controller with no perturbation.
In order to characterize cycles that resist perturbations in our setting, we introduce a new structural requirement on the reachability relation along an accepting cycle of the automaton. This property is formulated on the
region abstraction, and generalizes previous characterization of winning cycles in the absence of punctual guards.
We show that the problem remains within PSPACE despite the presence of punctual guards.

Verification of probabilistic infinite-state Markov chains is still a challenge despite several fruitful
numerical or statistical approaches. For decisive Markov chains, there is a simple numerical
algorithm that frames the reachability probability as accurately as required (however with an
unknown complexity). On the other hand when applicable, statistical model checking is in most of
the cases very efficient. Here we study the relation between these two approaches showing first that
decisiveness is a necessary and sufficient condition for almost sure termination of statistical model
checking. Afterwards we develop an approach with application to both methods that substitutes to
a non decisive Markov chain a decisive Markov chain with the same reachability probability. This
approach combines two key ingredients: abstraction and importance sampling (a technique that
was formerly used for efficiency). We illustrate this approach on probabilistic pushdown automata.
This talk is based on joint work with Benoît Barbot and Serge Haddad.

Microarchitectural timing channels are a well-known mechanism for information leakage. “Time protection” has recently been demonstrated as an operating system mechanism able to prevent them. In seL4 (an operating system kernel with a complete formal proof of correctness), we have developed an implementation of time protection that prevents microarchitectural timing channels by selectively partitioning key microarchitectural state either spatially or temporally. This approach has been formally verified for an operating system that meets certain well-defined requirements, and we have developed a proof approach for verifying that the seL4 microkernel meets those requirements. However, seL4’s existing specification and proofs are over a million lines of Isabelle – meaning any changes to its formal abstract specification will create significant work repairing its proofs. I will discuss how we accomplished the task of bending seL4 into the right shape to be able to prove time protection properties about it, while minimising breakages to its existing model and proofs.

Verification of higher-order programs faces challenges due to internal state-space explosion but also due to unknown external functions. To address the latter, program models able to analyse all possible external behaviours are needed. Game semantics is a theory providing such models and has been used to model from higher-order functional/imperative languages with rich type systems to Java programs to C-like code. In this talk we give a brief overview of game semantics and focus on recent applications of game models to program safety and equivalence verification. In the process, we look at automata over infinite alphabets, which naturally rise as machine descriptions of game semantic strategies, analyse some of their algorithmic properties and present tool implementations thereof.

Feedback allows systems to seamlessly and instantaneously adapt their behavior to their environment and is thereby the fundamental principle of life and technology — it lets animals breathe, it stabilizes the climate, it allows airplanes to fly, and the energy grid to operate. During the last century, control technology excelled at using this power of feedback to engineer extremely stable, robust, and reliable technological systems.

With the ubiquity of computing devices in modern technological systems, feedback loops become cyber-physical — the laws of physics governing technological, social or biological processes interact with (cyber) computing systems in a highly nontrivial manner, pushing towards higher and higher levels of autonomy and self-regulation. True autonomy, however, requires complex strategic and reactive decision making to interacting with classical feedback control. While stability, robustness and reliable self-adaptation remain to be of uppermost importance in these systems, the understanding of autonomy-driven strategic feedback loops and their utilization for this purpose is lacking far behind.

In this talk, I will discuss how a control-inspired view on formal methods, in particular reactive synthesis, allows us to move towards the design of robust and adaptable strategic feedback loops in cyber-physical systems. !