Damien Pous' Home Page.

Coq formalisation: robust reconfiguration of component assemblies

This page is a web-appendix to this paper, which we wrote with Fabienne Boyer and Olivier Gruber.


One major challenge of reconfigurable component-based systems is to maintain the consistency of the system despite failures occurring at reconfiguration time. This paper presents a reconfiguration protocol that supports any number of failures and provides the guarantee that the resulting system is always consistent. In particular, the proposed protocol supports failures occurring during the failure recovery process. It allows either roll-back or roll-forward recovery, failure permitting. We certified this protocol using the Coq proof assistant.

Coq proof scripts

We entirely formalized and proved the algorithms presented in this paper.

We do not rely on any axiom; the Coq development is split into two modules:

The above links and the table of contents below point to pages where the proofs have been stripped for the sake of readability; see here for the non-stripped version.

The sources are available here, they compile at least with Coq v8.3pl2.

Detailed table of contents

Library Common

Library RobustReconfiguration