Temporal property preservation under Z refinement in CSP-OZ specifications

One way to verify the correctness of an implementation under refinement in formal specifications is by verifying the system against a set of properties we wish to have in the final implementation. This is in such a way that the relevant properties are preserved in each development step. The difference here is that we have a separate specification of system properties. These properties are those that are satisfied by the initial specification. As the development of the system progresses from one step to another, the correctness of the concrete specification is verified by checking the satisfaction of the properties. The correctness of the abstract specification is preserved in the concrete specification (or an implementation) if the concrete specification satisfies all properties the abstract specification satisfies [1]. In other words, the properties are preserved and hold in the concrete specification. This paper extends the result on LTL property preservation for Z specifications in [2] to the OZ part of CSP-OZ specifications. This is where Z refinement exists side-by-side with CSP refinement in the CSP part of a CSP-OZ specification.