Library Common
- Various utilities
- List sorting
- Finite/ordered/foldable sets
- Topological sorting on acyclic relations on finite sets
Library RobustReconfiguration
- Modelisation: architectures, invariants, algorithms
- architectural invariants, to be preserved
- lifecycle FSM
- V-ordering of reconfiguration operations
- Incrementally Consistent Sequences (ICS)
- propagation algorithm, to saturate "apply down sets"
- architectural diff to generate apply up/down sets
- final commit session algorithm, without considering failures
- Proofs
- comparing architecures
- miscellaneous lemmas
- sufficient conditions for operations to preserve consistency
- applying consistent down sequences containing particular operations actually perform these operations
- abstract characterisation of saturated down sets
- key lemma: sorting a saturated down set results in an incrementally consistent sequence
- the propagation algorithms produce saturated down sets
- analysis of the xpropagate_stop function
- analysis of the down_diff function
- correctness of the up phase
- correctness of the session commit algorithm, in the failure free case
- Handling failures
This page has been generated by coqdoc