Talk:Event Model Decomposition

From Event-B
Jump to navigationJump to search

Dear the author of the article,

I do not clearly understand why shared variables and events must have a restriction that they cannot be refined in a sub-model. Suppose, we have a shared variable 's' of type BOOL. After the decomposition, this variable is data-refined with three new variables 's1', 's2' and 's3' such that 's' disappears. In this case we provide a gluing invariant, e.g. s = bool(s1=TRUE or s2=TRUE and s3=TRUE). Although 's' vanishes, we still can use it as the interface between sub-models since we have defined it as a shared variable and it still exists as the communication channel between the sub-models. Furthermore, the glueing invariant forms the precise interface between these sub-models such that it can be used to provide the required value and, therefore, no rule is broken.

Decomposition.jpg

Best regards, Sergey



Dear Sergey

The restriction is there to ensure that the shared variables are not being refined differently in sub-models. This ensures the compositionality of the sub-models. Recently, there is a proposal to encapsulate the shared variables in a separate module, allowing the shared variables to be refined.

Best regards, Son



Dear Son,

Thank you! That would be nice to allow for refining the shared variables since many (less formal) languages support refinement of the interface.

Best regards, Sergey