Abstract The current dominance of the service-based paradigm reflects the success of specific design and architectural principles embodied in terms like SOA and REST. This paper suggests further principles for the design of services exhibiting long-running transactions (that is, 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 consistency of data critical to the business logic. They do so by demanding (a) either the commitment of all of the transaction or none of it, and (b) that compensation is assured in case of failure in ‘parent’ transactions. The notion of scope is captured algebraically (rather than semantically) in order to express design guidelines which ensure that a given transaction satisfies those principles. Transactional processes are constructed by parallel composition of services, and transactions with scopes in a single service are dealt with as a special case. The system semantics is formalised as a transition system (in Z) and the principles are expressed as formulae in linear temporal logic over runs of the transition system. That facilitates the model checking (using SAL) of their bounded versions. Two simple examples are used throughout to illustrate definitions and finally to demonstrate the approach.

Wireless systems have a wide range of applications recently. To explore complex features of such systems, formalisms are proposed to specify and reason about them. This paper presents a case study of routing protocol in wireless networks. We formalize the route discovery process of AODV routing protocol using Object-Z. Network topology and local variables of nodes are defined by relations and functions. The broadcast communication is modelled by operations which change local variables of the sender and all of its connected receivers simultaneously. We show the proof of loop freedom property for established routes based on the specification. Further, the specification is modified by adding mobility of nodes and loop freedom under a dynamic network topology is discussed, showing the scalability of our approach.

Self-organising systems have become important relatively recently. It is frequently claimed that their complex nature necessitates new formalisms to express and reason about them. In this paper the opposite view is taken. Following Back's use of action systems to express a distributed system as an initialised possibly nonterminating loop, here two simple but representative case studies of self-organising systems are explored using only conventional techniques. The first deals with the configuration of an ad hoc network and shows how safety and liveness can be accurately expressed with an initialised loop. The second involves, like many self-organising systems, probabilistic behaviour and it is shown that existing techniques suffice to establish the system behaviour. In conclusion, the techniques illustrated can be used to provide a higher level of assurance than is possible with simulation alone.

Abstract Emergent behaviour—system behaviour not determined by the behaviours of system components when considered in isolation—is commonplace in multi-agent systems, particularly when agents adapt to environmental change. This article considers the manner in which Formal Methods may be used to authenticate the trustworthiness of such systems. Techniques are considered for capturing emergent behaviour in the system specification and then the incremental refinement method is applied to justify design decisions embodied in an implementation. To demonstrate the approach, one and two-dimensional cellular automata are studied. In particular an incremental refinement of the ‘glider’ in Conway’s Game of Life is given from its specification.

Complex software systems typically involve features like time, concurrency and probability, where probabilistic computations play an increasing role. It is challenging to formalize languages comprising all these features. We have integrated probability, time and concurrency in one single model (called PTSC), where the concurrency feature is modelled using shared-variable based communication. Meanwhile, we have also explored the link between the operational semantics and algebraic semantics, where our approach was started from algebraic laws via head normal form. This paper considers the animation of the link between operational semantics and algebraic semantics for PTSC. Our approach is by using Prolog as the development language. Firstly we explore the animation of the operational semantics for PTSC. The link of the two semantics is proceeded via the concept of head normal form. Secondly the generation of head normal form is explored, especially the animation of parallel expansion laws. Finally we consider the animation of deriving operational semantics by a provided derivation strategy via head normal form. The results animated from the first and the third exploration indicate that our operational semantics is sound and complete with respect to head normal form (or algebraic laws in general).

Refinement algebra provides axioms for the stepwise removal of abstraction, in the form of demonic nondeterminism, in a first-order system that supports reasoning about loops. It has been extended by Solin and Meinecke to computations involving implicit probabilistic choices: demonic nondeterminism then satisfies weaker properties. In this paper their axiom system is extended to capture explicit probabilistic choices. The first form is an unquantified probabilistic choice; the second is a partial quantified probabilistic choice (from which the usual binary probabilistic choice can be recovered). The new refinement algebra is sound with respect to 1-bounded expectation transformers, the premier model of probabilistic computations, but also with respect to a new model introduced here to capture more directly partial quantified computations. In this setting a `normal form' result of Kozen is proved, replacing multiple loops with a single loop that does the same job; and the extent to which the two forms of loop have the same expected number of steps to termination is considered. Being entirely first-order, the new refinement algebra is targeted to automation.

This paper proposes a , the "ambit' of an action, that allows the degree of distribution of an action in a multiagent system to be quantified without regard to its functionality. It demonstrates the use of that notion in the design, analysis and implementation of dynamically-reconfigurable multi-agent systems. It distinguishes between the extensional (or system) view and intensional (or agent-based) view of such a system and shows how, using the notion of ambit, the step-wise derivation paradigm of formal methods can be used to derive the latter from the former. In closing it addresses the manner in which these ideas inform studies in the ethics of systems of artificial agents.

An intermediate-level specification formalism (i.e., specification language supported by laws and a semantic model), Logs, is presented for PRAM and BSP styles of parallel programming. It extends pre-post sequential semantics to reveal states at points of global synchronization. The result is an integration of the pre-post and reactive-process styles of specification. The language consists of only six commands from which other useful commands can be derived. Parallel composition is simply logical conjunction and hence compositional. A simple predicative semantics and a complete set of algebraic laws are presented. Novel ingredients include the separation, in our reactive context, of the processes for nontermination and for abortion which coincide in standard programming models; the use of partitions, combining the terminating behavior of one program with the nonterminating behavior of another; and a fixpoint operator, the partitioned fixpoint. Our semantics benefits from the recent "healthiness function" approach for predicative semantics. Use of Logs, along with the laws for reasoning about it, is demonstrated on two problems: matrix multiplication (a terminating numerical computation) and the dining philosophers (a reactive computation). The style of reasoning is so close to programming practice that direct transformation from Logs specifications to real PRAM and BSP programs becomes possible.

In this paper a programming language, qGCL, is presented for the expression of quantum algorithms. It contains the features required to program a 'universal' quantum computer (including initialisation and observation), has a formal semantics and body of laws, and provides a refinement calculus supporting the verification and derivation of programs against their specifications. A representative selection of quantum algorithms are expressed in the language and one of them is derived from its specification.

Abstract Jones and Plotkin give a general construction for forming a probabilistic powerdomain over any directed-complete partial order [Jon90, JoP89]. We apply their technique to the failures/divergences semantic model for Communicating Sequential Processes [Hoa85]. The resulting probabilistic model supports a new binary operator, probabilistic choice, and retains all operators of CSP including its two existing forms of choice. An advantage of using the general construction is that it is easy to see which CSP identities remain true in the probabilistic model. A surprising consequence however is that probabilistic choice distributes through all other operators; such algebraic mobility means that the syntactic position of the choice operator gives little information about when the choice actually must occur. That in turn leads to some interesting interaction between probability and nondeterminism. A simple communications protocol is used to illustrate the probabilistic algebra, and several suggestions are made for accommodating and controlling nondeterminism when probability is present.

Abstract In specifying an operation it is often advantageous to describe it with abstract inputs and outputs whose concrete representation is described separately. For example, it is often convenient to describe as a set, input which in practice occurs as a sequence. The primary advantage of this approach is that one can initially concentrate on specifying an operation without the representations of its interface (that is, its inputs and outputs) obscuring the more important concerns of its abstract functional properties. Interface representations can be tackled independently, after the abstract functionality has been decided. Such separation of an operation into an abstract core and its interface with its environment makes the task of specification simpler, aids clarity of the result, and encourages reuse of both the abstract operation and its interface descriptions.

It is known that functional refinement does not preserve the security properties of a system. The authors propose a trace-based method for specifying the security properties of a system and a method which ensures that this security is preserved under refinement. They include an example to illustrate the use of the definitions and make use of non-interference (as defined in their notation).>

Abstract A scheme is presented which transforms systolic programs with a two-dimensional structure to one dimension. The elementary steps of the transformation are justified by theorems in the theory of communicating sequential processes and the scheme is demonstrated with an example in occam: matrix composition/decomposition.