But using either LTS or NPR only defines part of the semantics of machines. For the transition on a LTS can be used to represent handshake, broadcast or even method calling actions in addition they can be give a partially/totally correct interpretation and each operation can be given a guarded/undefined interpretation outside of its precondition. How to interpret a LTS (or NPR) specification can, as is common in the literature, be given by defining refinement.
By taking the event based notion of testing semantics we defined a general notion of refinement (ICFEM03) that is parameterized by (Ξ ,O) that is: Ξ - the set of contexts in which the machine can be placed and O - what can be observed when executing the machine context pair. We then showed that this general definition of refinement could be used to define refinement from some of the standard special models from both the event- and state-based literature simply by fixing (Ξ ,O).
Subsequently in Flexible Refinement we extended our general model by defining how to refine (implement) one special models using another special model that gives the operational semantics a distinct interpretation. As an example implementing handshake interation using broadcast interaction.
When defining how atomic component s could be modeled we showed the advantage of using a nonstandard definition of choice that originated from category theory. In addition we defined how to hide internal actions so as to give divergence a non-chaotic interpretation, thus giving NDFD a simple operational semantics.
We extended our general notion of refinement by defining vertical refinement thus allowing LTS at one layer to represent handshake actions while at a lower level they might be implemented on broadcast actions.
We found that the usual handshake model of processes such as CSP or CCS can not actually be implemented. Indeed Occam a partial implementation of CSP is forced to let the compiler resolve some nondeterminism that can not be removed from a specification with out completely rewriting the specification.
This led us to look at the use of simple use case specifications of process algebra style machines. We found that such specifications could suddenly require the redefinition of what constituted an atomic action and this occurred when process algebra machines were not implementable.