Verification and refinement with fine-grained action-based concurrent objects

Action-based concurrent object-oriented programs express autonomous behavior of objects through actions that, like methods, are attached to objects but, in contrast to methods, may execute autonomously whenever their guard is true. The promise is a streamlining of the program structure by eliminating the distinction between processes and objects and a streamlining of correctness arguments. In this paper we illustrate the use of action-based object-oriented programs and study their verification and their refinement from specifications, including the issue of non-atomic operations.