An Event-B formal model for a system reconfiguration pattern and its instantiation: application to Web services compensation

System substitution can be defined as the capability to replace a system by another one that preserves the specification of the original one. It may be used for reconfiguration in various situations like failure management, maintenance or Web services compensation. When substituting a system at runtime, a key requirement is to correctly restore the state of the substituted one. This paper proposes a correct-by-construction generic model for system reconfiguration defined using formal methods, based on a system substitution operator we define. This model provides a formal semantics for Web services compensation seen as a particular case of system substitution. The originality of the proposed approach relies on the fact that it is defined on a family of systems and it provides instantiation mechanisms for particular systems using witnesses. Systems are seen as state transition systems, and the system substitution operation is formalized as a state recovery operation. This proposal is supported by a formal model relying on stepwise refinements and proofs. A generic formal model is developed using Event-B. Specific systems instantiate this generic model using a particular use of refinement based on the definition of witnesses for existential proof obligations. A specific case study, borrowed from an electronic commerce application, is used as a particular instance of the defined generic model.