zbMATH — the first resource for mathematics

Using coupled simulations in non-atomic refinement. (English) Zbl 1028.68541
Bert, Didier (ed.) et al., ZB 2003: Formal specification and development in Z and B. Third international conference of B and Z users, Turku, Finland, June 4-6, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2651, 127-147 (2003).
Summary: Refinement is one of the most important techniques in formal system design, supporting stepwise development of systems from abstract specifications into more concrete implementations. Non-atomic refinement is employed when the level of granularity changes during a refinement step, i.e., whenever an abstract operation is refined into a sequence of concrete operations, as opposed to a single concrete operation.
There has been some limited work on non-atomic refinement in Z, and the purpose of this paper is to extend this existing theory. In particular, we strengthen the proposed definition to exclude certain behaviours which only occur in the concrete specification but have no counterpart on the abstract level. To do this we use coupled simulations: the standard simulation relation is complemented by a second relation which guarantees the exclusion of undesired behaviour of the concrete system. These two relations have to agree at specific points (coupling condition), thus ensuring the desired close correspondence between abstract and concrete specification.
For the entire collection see [Zbl 1020.00016].

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Full Text: Link