The B method has been successfully used to specify many industrial applications by refinement. Previously, we proposed enriching the B event systms 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 refienement relation by a relationship between transition systems. A result of our study shows that this relation is a special kind of smulation 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.
展开▼
