Atomic actions, and their refinements to isolated protocols

Inspired by the properties of the refinement development of the Mondex Electronic Purse, we view an isolated atomic action as a family of transitions with a common before-state, and different after-states corresponding to different possible outcomes when the action is attempted. We view a protocol for an atomic action as a computation DAG, each path of which achieves in several steps one of the outcomes of the atomic action. We show that in this picture, the protocol can be viewed as a relational refinement of the atomic action in a number of ways. Firstly, it yields a `big diagram' simulation `a la ASM. Secondly, it yields a `small diagram' simulation, in which the atomic action is synchronised with an individual step along each path through the protocol, and all the other steps of the path simulate skip. We show that provided each path through the protocol contains one step synchronised with the atomic action, the choice of synchronisation point can be made freely. We descr...

• Type: Journal
• Year: 2010
• Where: FAC
• Authors: Richard Banach, Gerhard Schellhorn
• Keywords: Atomic Action, Computer Networks, FAC 2010, Isolated Atomic Action, Mondex Electronic Purse