[tlaplus] Multi-level refinement

[Dmitry Kulagin <dmitry.kulagin@xxxxxxxxx>]

Hello,

I have a set of models on different abstraction layers - from requirements to architecture and implementation.

Number of levels varies but let it be three: A, B, C

"A" is the most abstract and C is very close to the implementation. Let their variable sets be: vars_a, vars_b, vars_c

I would like to specify refinement between levels: B => A, and C => B. 

To do so I add auxiliary variables into B and establish mapping to vars_a: (vars_b + aux_vars_b -> vars_a).

That is good for B, but then I would like to specify that C refines B.

If there was no B => A refinement, it would be enough to match vars_b variables only: (vars_c + aux_vars_c0) -> vars_b. 

But now as aux_vars_b were added I also have to provide mapping for them as well: (vars_c + aux_vars_c1) -> (vars_b + aux_vars_b).

It also means that aux_vars_c1 (typically) has more variables than aux_vars_c0.

It is inconvenient and becomes even more verbose if there are more than three levels.

I would like to keep models at each level as clean as possible, so I adopted the following approach:

* All models (A, B, C) do not have any auxiliary variables

* To refine A, new model B_Ref is created by extending B and adding auxiliary variables. This model has a refinement B_Ref -> A. The important property: B_Ref is equivalent to B modulo auxiliary variables

* To refine B, C_Ref is created so that C <=> C_Ref and C_Ref => B (to refine B it is enough to map only vars_b)

So only *_Ref models have auxiliary variables. The whole scheme:

A <= B_Ref /\ B_Ref <=> B /\ B <= C_Ref /\ C_Ref <=> C

Such approach allows to keep models free from auxiliary variables and refinement takes care only about two levels, so that the number of auxiliary variables is as small as possible.

The problem is that I see no way to mechanically prove C <=> C_Ref. It is easy to show C_Ref => C with TLC, but not the other direction.

At the same time, given how these (history) auxiliary variables introduced, it seems "obvious" that C => C_Ref is also true.

* Is it right approach to the problem of multi-level refinement?

* Is there a way to automate proofs like C => C_Ref?

* What alternatives exist?

Thank you,

Dmitry

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2345448c-9dde-45e4-9e86-7768ade61687n%40googlegroups.com.