Refinement of fair action systems

An action system is a framework for describing parallel or distributed systems, for which the refinement calculus offers a formalisation of the stepwise development method. Fairness is an important notion in modelling parallel or distributed systems, and this paper investigates a calculus for refinement of fair action systems. Simulations, which are proof techniques for refinement, are extended to verify fair action systems. Our work differs from others' in that the additional condition concerning fairness is expressed through termination of related iteration statements. For this purpose, existing proof rules for termination are extended. In the tradition of the refinement calculus, our approach to fairness is based on techniques developed mainly for sequential programming. Received: 16 March 1995 / 16 April 1997     

ZRC – A Refinement Calculus for Z

The fact that Z is a specification language only, with no associated program development method, is a widely recognised problem. As an answer to that, we present ZRC, a refinement calculus based on Morgan's work that incorporates the Z notation and follows its style and conventions. This work builds upon existing refinement techniques for Z, but distinguishes itself mainly in that ZRC is completely formalised. In this paper, we explain how programs can be derived from Z specifications using ZRC. We present ZRC-L, the language of our calculus, and its conversion laws, which are concerned with the transformation of Z schemas into programs of this language. Moreover, we present the weakest precondition semantics of ZRC-L, which is the basis for the derivation of the laws of ZRC. More than a refinement calculus, ZRC is a theory of refinement for Z. Received July 1997 / Accepted in revised form October 1998     

Refinement concepts formalised in higher order logic

A theory of commands with weakest precondition semantics is formalised using the HOL proof assistant system. The concept of refinement between commands is formalised, a number of refinement rules are proved and it is shown how the formalisation can be used for proving refinements of actual program texts correct.     

A formal model of fair exchange protocols

1 Background Electronic commerce over open networks has been growing rapidly over the last dec- ade. Usually commercial transactions involve parties who mutually distrust each other, so protecting one legitimate party from another is as important as protecting legitimate parties from intruders. Therefore the fairness property of an exchange protocol is vital. Generally, a typical fair exchange protocol has a main protocol and several sub-protocols. It has a much bigger size than the classical…     

Data refinement of mixed specifications

Using predicate transformers as a basis, we give semantics and refinement rules for mixed specifications that allow UNITY style specifications to be written as a combination of abstract program and temporal properties. From the point of view of the programmer, mixed specifications may be considered a generalization of the UNITY specification notation to allow safety properties to be specified by abstract programs in addition to temporal properties. Alternatively, mixed specifications may be viewed as a generalization of the UNITY programming notation to allow arbitrary safety and progress properties in a generalized ‘always section’. The UNITY substitution axiom is handled in a novel way by replacing it with a refinement rule. The predicate transformers foundation allows known techniques for algorithmic and data-refinement for weakest precondition based programming to be applied to both safety and progress properties. In this paper, we define the predicate transformer based specifications, specialize the refinement techniques to them, demonstrate soundness, and illustrate the approach with a substantial example. Received: 1 April 1996 / 6 March 1997     

On the existence of delay-insensitive fair arbiters: Trace theory and its limitations

This paper considers the existence and formal specification of delay-insensitive fair arbiters. We show that the exact notion of fairness used is of critical importance because certain common notions are not delay-insensitive when used across independent interfaces. We further show that for the relevant notions of fairness, the existing trace theory of finite traces lacks the expressive power to specify a delay-insensitive fair arbiter (i.e. the specification of such a fair arbiter is also satisfied by an unfair arbiter). Based on this we extend trace theory to include infinite traces, and show by example the importance of including liveness in such a theory. The extended theory is sufficiently expressive to distinguish fair arbiters from unfair ones, and we use it to exhibit a delay-insensitive fair arbiter, thus establishing their existence. In addition our extended theory generalizes the existing trace theory by introducing a composition operator (C) that at once generalizes the existing operators and obviates the composability restrictions used by previous authors. Finally our extended theory introduces wire modules as an abstraction to capture the important role that transmission media properties play in circuit behavior. David L. Black is a graduate student and Ph.D. candidate in the Department of Computer Science, Carnegie-Mellon University, Pittsburgh, PA. His research interests include trace theory, temporal logic, and the specification, design and verification of asynchronous circuits. Mr. Black received the B.A. and M.A. degrees in Mathematics along with the B.S.E. (Computer Science and Engineering) degree in 1983 from the University of Pennsylvania, Philadelphia, PA. He also received the M.S. degree in computer science from Carnegie-Mellon University in 1985. Partial support of his graduate studies at Carnegie-Mellon has been provided by a R.K. Mellon fellowship. Mr. Black is also a member of Phi Beta Kappa, Tau Beta Pi, Eta Kappa Nu and Pi Mu Epsilon.     

A Logic for Schema-Based Program Development

We show how a theory of specification refinement and program development can be constructed as a conservative extension of our existing logic for Z. The resulting system can be set up as a development method for a Z-like specification language, or as a generalisation of a refinement calculus (with a novel semantics). In addition to the technical development we illustrate how the theory can be used in practice.     

The μ-calculus as an assertion-language for fairness arguments

Various principles of proof have been proposed to reason about fairness. This paper addresses—for the first time—the question in what formalism such fairness arguments can be couched. To wit: we prove that Park's monotone first-order μ-calculus, augmented with constants for all recursive ordinals can serve as an assertion-language for proving fair termination of do-loops. In particular, the weakest precondition for fair termination of a loop w.r.t. some postcondition is definable in it. The relevance of this result to proving eventualities in the temporal logic formalism of Manna and Pnuelis (in “Foundations of Computer Science IV, Part 2,” Math. Centre Tracts, Vol. 159, Math. Centrum, Amsterdam, 1983) is discussed.     

Action systems,unbounded nondeterminism,and infinite traces

Morgan [Mor90a] has described a correspondence between Back's action systems [BKS83] and the conventionalfailures-divergences model of Hoare'scommunicating sequential processes (CSP) formalism [Hoa85]. However, the CSP failures-divergences model does not treat unbounded nondeterminism, although unbounded nondeterminism arises quite naturally in action systems; to that extent, the correspondence between the two approaches is inadequate.Fortunately there is an extendedinfinite traces model of CSP [RoB89] which treats unbounded nondeterminism. We extend the CSP-action system correspondence, using that model instead, to take the unbounded nondeterminism of action systems properly into account.In passing, we develop a definition of the weakest precondition under which an infinite heterogeneous trace of actions is enabled.Funded by Broadcom Éireann Research Ltd, Dublin.     

Calculating sharp adaptation rules

Adaptation rules adapt the pre-post specification of a procedure to contexts where it is called. Such rules are important for practical reasons and necessary for completeness for languages with recursive procedures. A sharp rule is one that gives the weakest precondition with respect to a given postcondition. A number of rules have been proposed, most unsound or incomplete or non-sharp. Using refinement algebra, we clarify and extend the applicability of previously proposed sharp rules for total correctness and show how further rules may be found.     

Event refinement in state-based concurrent systems

Operations on action systems may be defined corresponding to CSP hiding and renaming. These are of particular use in describing the refinement between action systems in which the granularity of actions is altered. We derive a simplified expression for hiding sets of actions and present sufficient conditions for forwards simulation in which the concrete system uses hiding and renaming. Both of these reduce the complexity of proofs of refinement. We present a case study in specification and refinement using action systems which makes use of the operations and refinement rules previously defined.A trademark of the IBM Corporation.     

Towards action refinement for true concurrent real time

Action refinement is an essential operation in the design of concurrent systems, real-time or not. In this paper we develop a theory of action refinement in a real-time non-interleaving causality based setting, a timed extension of bundle event structures that allows for urgent interactions to model timeout. The syntactic action refinement operation is presented in a timed process algebra as incorporated in the internationally standardised specification language LOTOS. We show that the behaviour of the refined system can be inferred compositionally from the behaviour of the original system and from the behaviour of the processes substituted for actions with explicitly represented start points, that the timed versions of a linear-time equivalence, termed pomset trace equivalence, and a branching-time equivalence, termed history preserving bisimulation equivalence, are both congruences under the refinement, and that the syntactic and semantic action refinements developed coincide under these equivalence relations with respect to a metric denotational semantics. Therefore, our refinement operations behave well. They meet the commonly expected properties.Received: 9 January 2003     

The weakest specifunction

The weakest specifunction has been introduced to generalise the notions of weakest prespecification and weakest parallel environment. It calculates the weakest specification function whose value refines the target specification when applied to a given component; thus it forms the basis for compositional refinement, an essential ingredient in program derivation. But unlike those previous calculi it is able to deal with several unknown components simultaneously and hence has wider applicability. In this paper we extend the general theory of the weakest specifunction, identifying those spaces in which it behaves miraculously. The par-seq specifunction places an established component in parallel with a required component and the result in sequence with another required component to meet a given specification. We extend the study of the par-seq specifunction in the context of log s, an intermediate-level language for reactive computing in an abstraction of the PRAM and BSP models of computation, and provide a single complete law for its use in program derivation. The resulting calculus is applied to the derivation of a distributed algorithm for dynamic load balancing.     

An optimal self-stabilizing strarvation-free alternator

System refinements from a strong to a weaker model are highly desirable because they allow designers to reason effectively in the strong model. Semantics and fairness refinements are often implemented by alternators preserving the property of stabilization. The existing alternators [Gouda and Haddix, Proceedings of the Third Workshop on Self-Stabilizing Systems (published in association with ICDCS99) The 19th IEEE International conference on Distributed Computing System), IEEE Computer Society Silver Spring, MD, 1999, pp. 48-53; Nesterenko and Arora, Disc99 Distributed Computing 13th International symposium springer, Berlin, 1999, pp. 254-268] provide semantics refinement but fail to implement starvation-freedom. Starvation-freedom requires that no two neighboring processes are scheduled simultaneously; along any interleaved execution, each action is executed infinitely often; no action is infinitely often enabled but never executed; and the number of enabled actions scheduled by the alternator is maximal. In this paper, we first establish the relationships between various mutual exclusion assumptions and the starvation-free alternators (SFAs) under various execution models.Then, as a remedy for the deficiencies of the existing alternators, we propose a fairness refinement for self-stabilizing distributed systems based on a state-space optimal self-stabilizing a (SFA) for arbitrary topologies and verify its correctness.     

Z规格说明的前置条件的简化

在软件方法学中，形式方法越来越受到人们的重视，并已被应用于软件开发．Z是一种基于数学表示的软件规格说明方法．前置条件的简化是Z规格说明方法中一种标准的检查，本文讨论了Z规格说明中关于操作的前置条件及其计算．提出了简化过程的终止条件，给出了一个用于简化前置条件的算法，该算法可自动产生简化过程的证据．     

一种REM算法辅助的分层组播流量控制方案

基于分层组播中公平速率分配算法实施过程中存在的问题以及分层组播协议策略中同步点的优化问题,提出了将主动队列管理算法REM作为对端系统的辅助加入到分层组播流量控制中,将分层组播同步点策略、满足Max-Min公平性要求的速率分配算法以及基于REM的显式拥塞指示技术有机地结合起来,设计了一种基于速率的、由接收者和发送者混合驱动的分层组播流量控制方案。仿真实验结果表明该方案使得分层多速率组播在保证会话内、会话间公平性的前提下,提高了流量控制机制的高效性和对网络状态适应的灵敏性。     

Atomic actions, and their refinements to isolated protocols

Inspired by the properties of the refinement development of the Mondex Electronic Purse, we view an isolated atomic action as a family of transitions with a common before-state, and different after-states corresponding to different possible outcomes when the action is attempted. We view a protocol for an atomic action as a computation DAG, each path of which achieves in several steps one of the outcomes of the atomic action. We show that in this picture, the protocol can be viewed as a relational refinement of the atomic action in a number of ways. Firstly, it yields a ‘big diagram’ simulation à la ASM. Secondly, it yields a ‘small diagram’ simulation, in which the atomic action is synchronised with an individual step along each path through the protocol, and all the other steps of the path simulate skip. We show that provided each path through the protocol contains one step synchronised with the atomic action, the choice of synchronisation point can be made freely. We describe the relationship between such synchronisations and forward and backward simulations. We relate this theory to serialisations of system runs containing multiple interleaved transactions, showing how the clean picture of the refinement of an isolated atomic action to an isolated protocol becomes obscured by the details of the interleaving. In effect, the fact that protocols are typically executed by a number of co-operating agents, not all of which embark on executing the protocol at the same moment, results in ‘ragged starts’ and ‘ragged ends’ to protocol instantiations, leading to potential overlaps between unrelated protocol instances that the theory must handle. We show how existing Mondex refinements embody the ideas developed, and describe a mechanical verification of the results presented.     

Measurement of refinement and correctness

The purpose of this paper is to introduce a measurement approach of refinement and correctness of probabilistic programs. That is, we define the refinement degree and the correctness degree by the weakest precondition transformers. This kind of measurement indicates the degree that a program is refined by another and the degree that a program is correct with respect to a pair of precondition and postcondition. Some properties of this measurement, for example continuity, are discussed.     

Probabilistic guarded commands mechanized in HOL

The probabilistic guarded-command language (pGCL) contains both demonic and probabilistic non-determinism, which makes it suitable for reasoning about distributed random algorithms. Proofs are based on weakest precondition semantics, using an underlying logic of real- (rather than Boolean-)valued functions.We present a mechanization of the quantitative logic for pGCL using the HOL theorem prover, including a proof that all pGCL commands satisfy the new condition sublinearity, the quantitative generalization of conjunctivity for standard GCL.The mechanized theory also supports the creation of an automatic proof tool which takes as input an annotated pGCL program and its partial correctness specification, and derives from that a sufficient set of verification conditions. This is employed to verify the partial correctness of the probabilistic voting stage in Rabin's mutual-exclusion algorithm.