Name
Title | ||
|---|---|---|
Correct Instantiation of a System Reconfiguration Pattern: A Proof and Refinement-Based Approach |
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. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1109/HASE.2016.47 | 2016 IEEE 17th International Symposium on High Assurance Systems Engineering (HASE) |
Keywords | Field | DocType |
system substitution,system reconfiguration,proof and refinement-based methods,Event-B | Computer science,Context model,Composition operator,Mathematical proof,Refinement,Operator (computer programming),Formal methods,Maintenance engineering,Reliability engineering,Control reconfiguration | Conference |
ISSN | Citations | PageRank |
1530-2059 | 6 | 0.65 |
References | Authors | |
6 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Guillaume Babin | 1 | 16 | 2.42 |
| Yamine Aït Ameur | 2 | 287 | 52.61 |
| Marc Pantel | 3 | 146 | 33.11 |