Publications

We propose a formalism for modelling concurrent systems and for supporting stepwise refinement of concurrent systems. Our formalism allows one to describe the possible behaviours of a concurrent system in an operational manner, and to select from the operational description the desired behaviours using a logical approach. We discuss how our formalism can be used for incremental stepwise development where a high-level specification consisting of little operational aspect and largely logical assertions, is refined gradually into a low-lever specification consisting of mainly operational description and few or no logical dictations. We illustrate this refinement methodology with a simplified version of Lamport’s Bakery algorithm.

The current dominance of the service-based paradigm reflects the success of specific design and archi- tectural principles embodied in terms like SOA and REST. This paper suggests further principles for the design of services exhibiting long-running transactions, whose characteristic feature is that in the case of failure not all system states can be automatically restored: system compensation is required. The principles are expressed at the level of scope-based compensation and fault handling and ensure the con- sistency of data critical to the business logic by demanding (a) either the commitment of all of the 'scope' or nothing in case of failure, and (b) compensation is assured in case of failure in parent scopes. The notion of scope is expressed algebraically and design guidelines are suggested to ensure transactional processes satisfy those principles. To assist validation, the algebra is translated to Coloured Petri Nets; the principles are expressed as CTL formulae; and their bounded versions are checked with the CPN Tools. A simple but typical case study, 'Batch-ATM', is used throughout to illustrate definitions and finally to demonstrate the approach.