Preservation of Correctness in Event-B Refinement

This section aims to demonstrate an attempt to prove the consistency, the relative com-pleteness, and the domain evolution described in Lemma 1 by discharging Event-B proof obligations. If Lemma 1 can be shown by discharging the proof obligations on Event-B models defined by Definition 10 and Definition 11, we can imply the preservation of correctness of requirements through Event-B refinement.

3.3.1 Consistency

The definitions of consistency are defined independently by the evolutionary framework and Event-B. The consistency of the evolutionary framework can be shown by proving R ∪D 6|= ⊥. This consistency means an internal consistency in the sense that R and D must be at he same step of the evolution. Event-B also generates a set of proof obligations to ensure Event-B’s consistency inside a machine description seeing one or more contexts [Abr10]. Proof obligation generation rules for Event-B’s consistency are separately defined for abstract models and concrete models (Definition 3 and Definition 4) as mentioned in Section 2.1.

From the proof obligations for abstract model consistency (Definition 3), we conclude the following theorem:

Theorem 2 (Consistent Abstract Model). Let R and D be sets representing an Event-B abstract machine and a context respectively. By assuming that axioms, invariants and guards are consistent, if proof obligations generated according to Definition 3 can be dis-charged, then R∪D6|=⊥ holds.

Proof. Since each event is free from each other, let the set:

{A, I_i, I∧G_i∧BA_i}

be a subset ofR∪D representing an event of an Event-B abstract model.

We assume that A∧I ∧G_i holds. If F IS is successfully discharged, then there exists

a state v⁰_i in which BA_i holds. Consequently, if IN V is discharged, then I_i holds. This implies that

{A, I_i, I∧G_i∧BA_i}

is consistent, which also means every event described in R∪D is consistent.

Therefore,R∪D6|=⊥ holds.

According to the above theorem, we need to assume that axioms, invariants and guards are consistent to conduct the proof. In facts, there is no proof obligation directly ensures that A ∧ I ∧ G_i holds. We have to write axioms, invariants and guards correctly by ourselves in Event-B.

In the case of the concrete model, the following theorem can be concluded from Defini-tion 4 from SecDefini-tion 2.1.

Theorem 3 (Consistent Concrete Model). Let R and D be sets representing Event-B a concrete machine and a context respectively. Event-By assuming that axioms, invariants and guards are consistent, if proof obligations generated according to Definition 4 can be discharged, then R∪D6|=⊥ holds.

Proof. Since each event is free from each other, let the set:

{A, J_j, I∧J ∧H_j ∧W_j ∧BA2_j}

be a subset of R ∪D representing an event of an Event-B concrete model. We assume that A∧I∧J∧H_j holds. If F IS_ref is successfully discharged, then there exists a state w⁰_j in which BA2_j holds. Consequently, if W F IS is discharged, then there is a state v⁰_j in which W_j holds. Then, by discharging IN V_ref, J_j holds. Finally, this implies that

{A, J_j, I∧J ∧H_j ∧W_j ∧BA2_j}

is consistent, which also means every event described in R∪D is consistent. Therefore, R∪D6|=⊥ holds.

This theorem also needs the assumption representing that axioms, invariants, and guards are consistent.

From Theorem 2 and 3, we finally provedR∪D6|=⊥ in the conversion of Event-B into evolutionary framework.

3.3.2 Relative Completeness

In the Event-B refinement, Event-B generates a set of proof obligations to ensure that a concrete model preserves the original properties and behavior of an abstract model [Abr10].

In other words, invariants of the abstract model must also hold in the concrete model, and when a concrete event is triggered, the abstract event must be triggered as well.

Here, we try to prove R_i+1∪D_i+1 |=R_i that is the relative completeness of evolutionary framework, by discharging the proof obligations of the model refinement. Definition 5 from Section 2.1 defines the proof obligation generation rules for the model refinement

A result from Definition 5 can be expressed in the following theorem:

Theorem 4 (Relative Completeness). Let R_i ∪D_i and R_i+1 ∪D_i+1 be consecutive evo-lution steps representing an abstract model and a concrete model of Event-B respectively.

By assuming that both models are consistent, if proof obligations generated according to Definition 5 can be discharged, then R_i+1∪D_i+1 |=R_i holds.

Proof. Let a subset

{I∧G_i∧BA_i} be an abstract event of R_i and a subset:

{A, I∧J ∧H_j ∧W_j ∧BA2_j}

be a concrete event of Ri+1∪Di+1 which refines the abstract event. Assuming that each subset is consistent, this implies thatA∧I∧J∧H_j∧W_j∧BA2_j holds, soI holds trivially.

If GRD holds, then G_i holds. If SIM holds, then BA_i holds.

Because I, Gi, and BAi hold, this implies that the subset {A, I∧J ∧H_j ∧W_j ∧BA2_j} can conclude the subset

{I∧Gi∧BAi} Therefore,R_i+1∪D_i+1 |=R_i holds.

Theorem 4 shows that the relative completeness of the evolutionary framework can be proved in term of the Event-B refinement.

3.3.3 Domain Evolution

The last proof needed to be shown is the domain evolution which can be expressed by the following theorem:

Theorem 5 (Context Evolution). Let D_i and D_i+1 be a consecutive evolution steps of domains representing

Event-B contexts. If we assume that axioms of each context are consistent, thenDi+1 |=Di

holds.

Since we assume that axioms are consistent and we can only extend the context, the proof of this theorem is straightforward: the extending context can directly infer to the extended context.

3.3.4 Extension and results

Although we already showed the proof of Lemma 1 of the evolutionary framework on Event-B model, we omitted some Event-B components and some proof obligations for simplifying the proofs. In this section, we only show an idea to demonstrate that the omitted parts can be supported by the conversion as well.

Proof obligations in Event-B are always of the following form:

Hypos⇒Goal

where Hyposis the set of hypotheses (predicates) and Goal is a goal that can be proved from the hypotheses. In order to support the omitted parts, we change the Event-B model by adding the Goal parts of the proof obligation directly into the model. For example, consider the proof obligation:

V AR:A∧I∧G_i∧BA_i ⇒n_i(s, c, v_i⁰)< n_i(s, c, v_i)

where n_i(s, c, v_i) is a variant, which means a mathematical expressions to guarantee that the execution of a corresponding event can be terminated. The termination can be shown by V AR to ensure that it is always decreased by the event. We may express an event related to a variant by a subset:

{A, I ∧Gi∧BAi, ni(s, c, v_i⁰)< ni(s, c, vi)}

Then, V ARcan be discharged in this subset because the goals of these proof obligations are added into it.

We can see from Theorem 2, 3, 4, and 5 that the conversion of Event-B into the evolutionary framework results in the fact that Event-B preserves the correctness of re-quirements in the evolution by discharging proof obligations under the assumption that axioms, invariants, and guards are consistent.