Multi-level refinement

37 views
Skip to first unread message

Dmitry Kulagin

unread,
Jun 24, 2021, 10:46:53 AM6/24/21
to tlaplus
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


Leslie Lamport

unread,
Jun 24, 2021, 1:28:20 PM6/24/21
to tlaplus
If B_ref is obtained from B by adding an auxiliary variable (meaning that B_ref with the auxiliary variable hidden is equivalent to B), then proving B_ref => A proves that B => A.  And similarly for C, C_ref, and B.  So proving B_ref => A and C_ref => B proves C => A.  Therefore, it suffices to check B_ref => A and C_ref => B.

Theorem 1 of the paper  Auxiliary Variables in TLA+ (lamport.azurewebsites.net)   gives the condition that must be satisfied for a history variable.  It is pretty straightforward and, if you want to be sure that you haven't made a mistake, they should be easy for TLAPS to check.

Leslie

Dmitry Kulagin

unread,
Jun 24, 2021, 5:21:29 PM6/24/21
to tlaplus
Thank you, Leslie! That is helpful
Reply all
Reply to author
Forward
0 new messages