We consider the problem of gathering in finite time and at the same location, not known beforehand, a set of deterministic semi-synchronous robots, starting from an arbitrary initial configuration that may even be bivalent (that is, a configuration where the robots are evenly split on two different locations). This problem is known to be unsolvable when the robots are oblivious, that is, when they cannot remember their past actions. We present two deterministic gathering algorithms where robots may remember and communicate a single bit of memory. This bit may be arbitrarily (and adversarially) set in the initial configuration. Our solutions are thus memory optimal and self-stabilizing. The first algorithm makes use of multiplicity detection, while the second solely uses robot colors. Their proof of correctness is formally certified by the Coq proof assistant using the Pactole framework.

Embedded systems often need to react in a timely manner. Life-critical or mission-critical ones require assurance that they comply with these real-time requirements. In particular, schedulability analysis is both essential and difficult to get right. Formal methods can help as they are a powerful tool for ensuring properties with the highest assurance level. We describe a case study for the FPP and EDF policies providing end-to-end assurance by connecting the schedulability analysis tool Prosa and the real-time OS kernel RT-CertiKOS, both using the Coq proof assistant to prove their results. Analyzing precisely the key ideas underlying this connection, we improve it to make it more generic and reduce the associated proof burden. We thus sketch a refined method which allows for providing formal schedulability guarantees to other OSes or low-level components with minimal effort.

The reliability and security of safety-critical real-time systems are of utmost importance because the failure of these systems could incur severe consequences (e.g., loss of lives or failure of a mission). Such properties require strong isolation between components and they rely on enforcement mechanisms provided by the underlying operating system (OS) kernel. In addition to spatial isolation which is commonly provided by OS kernels to various extents, it also requires temporal isolation, that is, properties on the schedule of one component (e.g., schedulability) are independent of behaviors of other components. The strict isolation between components relies critically on algorithmic properties of the concrete implementation of the scheduler, such as timely provision of time slots, obliviousness to preemption, etc. However, existing work either only reasons about an abstract model of the scheduler, or proves properties of the scheduler implementation that are not rich enough to establish the isolation between different components. In this paper, we present a novel compositional framework for reasoning about algorithmic properties of the concrete implementation of preemptive schedulers. In particular, we use virtual timeline , a variant of the supply bound function used in real-time scheduling analysis, to specify and reason about the scheduling of each component in isolation. We show that the properties proved on this abstraction carry down to the generated assembly code of the OS kernel. Using this framework, we successfully verify a real-time OS kernel, which extends mCertiKOS, a single-processor non-preemptive kernel, with user-level preemption, a verified timer interrupt handler, and a verified real-time scheduler. We prove that in the absence of microarchitectural-level timing channels, this new kernel enjoys temporal and spatial isolation on top of the functional correctness guarantee. All the proofs are implemented in the Coq proof assistant.

Formal verification of real-time systems is attractive because these systems often perform critical operations. Unlike non real-time systems, latency and response time guarantees are of critical importance in this setting, as much as functional correctness. Nevertheless, formal verification of real-time OSes usually stops the scheduling analysis at the policy level: they only prove that the scheduler (or its abstract model) satisfies some scheduling policy. In this paper, we go further and connect together Prosa, a verified schedulability analyzer, and RT-CertiKOS, a verified single-core sequential real-time OS kernel. Thus, we get a more general and extensible schedulability analysis proof for RT-CertiKOS, as well a concrete implementation validating Prosa models. It also showcases that it is realistic to connect two completely independent formal developments in a proof assistant.

The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs.

International audience

Krivine presented in [Krivine, 2011] a methodology to combine Cohen's forcing with the theory of classical realizability and showed that the forcing condition can be seen as a reference that is not subject to backtracks. The underlying classical program transformation was then analyzed by Miquel [Miquel, 2011] in a fully typed setting in classical higher-order arithmetic (PA-omega^+). As a case study of this methodology, we present a method to extract a Herbrand tree from a classical realizer of inconsistency, following the ideas underlying the completeness theorem and the proof of Herbrand's theorem. Unlike the traditional proof based on König's lemma (using a fixed enumeration of atomic formulas), our method is based on the introduction of a particular Cohen real. It is formalized as a proof in PA-omega^+, making explicit the construction of generic sets in this framework in the particular case where the set of forcing conditions is arithmetical. We then analyze the algorithmic content of this proof.

We focus on the problem of finding (the size of) a minimal winning coalition in a multi-player game. We prove that deciding whether there is a winning coalition of size at most k is HP-complete, while deciding whether k is the optimal size is DP -complete. We also study different variants of our original problem: the function problem, where the aim is to effectively compute the coalition; more succinct encoding of the game; and richer families of winning objectives.