Ready-simulation is not ready to express a modular refinement relation

Abstract

The B method has been successfully used to specify many industrial applications by refinement. Previously, we proposed enriching the B event systems by formulating its dynamic properties in LTL. This enables us to combine model-checking with theorem-proving verification technologies. The model-checking of LTL formulae necessitates that the B event system semantics is a transition system. In this paper, we express the refinement relation by a relationship between transition systems. A result of our study shows that this relation is a special kind of simulation allowing us to exploit the partition of the reachable state space for a modular verification of LTL formulae. The results of the paper allow us to build a bridge between the above view of the refinement and the notions of observability characterized as simulation relations by Milner, van Glabbeek, Bloom and others. The refinement relation we define in the paper is a ready-simulation generalization which is similar to the refusal simulation of Ulidowsky. The way the relation is defined allows us to obtain a compositionality result w.r.t. parallel composition operation. For complex systems, it is important in practice to associate a design by refinement with a design by a parallel composition of their components. This refinement relation has two main applications: –it allows the splitting of the refined transition system into modules; –it allows the construction of complex systems by a parallel composition of components. It makes sense to qualify the refinement relation as being modular.