학술논문
Correct Instantiation of a System Reconfiguration Pattern: A Proof and Refinement-Based Approach
Document Type
Conference
Source
2016 IEEE 17th International Symposium on High Assurance Systems Engineering (HASE) High Assurance Systems Engineering (HASE), 2016 IEEE 17th International Symposium on. :31-38 Jan, 2016
Subject
Language
ISSN
1530-2059
Abstract
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 occur in different reconfiguration situations like failure management or maintenance. 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. Systems are seen as state transition systems. This proposal relies on refinement and proofs. The formal development is conducted with the Event-B method. It consists in defining system substitution as a system composition operator associated to proof obligations. 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. This proposal is illustrated with an electronic commerce service.