The use of internal operations in Z is not new, representative examples include [55,205,168,197,209,67]. For example, Strulo [197] considers the use of Z in network management and describes the need for both observable and internal operations in this application area. A particular example is described of a network manager's view of a router within a network. There, alarm notifications are a typical example of internal events which are specified as usual but with informal commentary describing which operations are observable and which are internal. A similar approach and application area is described by Wezeman and Judge in [205] and Rafsanjani in [168].
Cusack and Wezeman in [55] adopt a number of conventions for the use of Z for the specification of OSI network management standards. In particular, they make the distinction between internal and observable operations according to whether an operation has input/output, all operations without input or output variables are considered internal, all others are observable. Their work is placed in an object-oriented setting and they consider notions of subtyping based upon conformance instead of refinement.
Evans in [81] considers the use of Z for the specification of parallel systems, and in particular discusses issues of liveness and fairness in dynamic specifications. Informal commentary partitions the specification into internal and observable operations, and Evans considers the refinement relations needed for Z specifications of concurrent systems.
Similar work to that described in this chapter has appeared in other state-based formalisms. For example, Butler [43] considers the specification and refinement of internal actions in the B method. The email specification in Example 11.2.5above is adapted from a B specification given in [45]. Additional work in this area also includes the work of Lano, e.g., [142], and the time service example has been specified in B in [143]. The work described in this chapter first appeared in [69,68].
Other formalisms, such as TLA and automata, have a long history of using stuttering steps to verify refinements involving internal actions, see, for example, [1,185]. These languages take a different approach to the introduction of livelock by using fairness criteria on the observable operations. For example, in [185] liveness conditions are used to describe which executions of the automaton are considered to represent a properly working system. The use of such liveness conditions or fairness criteria provide a language which is strictly more expressive than Z, since we cannot write a Z specification with an infinitely often enabled internal operation that does not involve livelock.
In [185] Sogaard-Andersen, Lynch and Lampson demonstrate the correctness of reliable at-most-once message delivery protocols using timed I/O automata. In particular, two protocol refinements are verified: a clock-based protocol and a five-packet handshake protocol. The verification of these refinements is split into a number of stages, with the two implementations being downward simulations of an intermediate description, which itself is an upward simulation of the original problem specification.
In addition to its size, the case study is interesting because it is necessary to use an upward simulation in the verification. It also verifies a timed model (the clock protocol) against the untimed problem statement by using various embedding results to move between the models. The specifications in Example 11.4.1are simplified versions of parts of this case study.
Stuttering steps have also been used in action systems [13,12] to verify refinements with internal actions. Back and von Wright in [14] define refinement in terms of the execution traces of an action system. Forward and backward simulation methods are then described which explicitly deal with internal (i.e., stuttering) actions.