What have we been doing?

While at Waikato, since 2000 I have been working with Steve Reeves, comparing state base and event based notions of refinement between entities that, for want of a word, we will call machines. As there are very many formalisms we needed some common ground upon which to compare them. We were able to view most formalisms as consisting of one, a distinct syntax and two, a distinct denotational semantics. The common ground seemed to be their operational semantics. Event based formalisms are frequently given a LTS labeled transition systems semantics and state based formalisms are frequently given a an operational semantics consisting of NPR a set of named partial relations, the name bing the name of an operation and the relation its operational semantics. As there is a simple isomorphism between the event-based LTS and the state-based NPR we have a common ground between many formalisms from both the state- and event-based worlds.

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.