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.
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.