On the expressive power of CSP refinement

We show that wide-ranging classes of predicates on the failures-divergences model for CSP can be represented by refinement checks in a general form. These are predicates of a process P expressible as F(P)⊏G(P), where F and G are CSP contexts and ⊏ is refinement. We use ideas similar to full abstraction, but achieve a stronger property than that. Our main result is that topologically-closed predicates are precisely those representable when F and G are both uniformly continuous. We show that sub-classes of predicates such as refinement-closed and distributive ones are represented by special forms of this check.Received November 2003Revised July 2004Accepted December 2004 by M. Leuschel and D. J. Cooke     

Structural Refinement of Systems Specified in Object-Z and CSP

This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.     

A Refinement Strategy for Circus

We present a refinement strategy for Circus, which is the combination of Z, CSP, and the refinement calculus in the setting of Hoare and Hes unifying theories of programming. The strategy unifies the theories of refinement for processes and their constituent actions, and provides a coherent technique for the stepwise refinement of concurrent and distributed programs involving rich data structures. This kind of development is carried out using Circuss refinement calculus, and we describe some of its laws for the simultaneous refinement of state and control behaviour, including the splitting of a process into parallel subcomponents. We illustrate the strategy and the laws using a case study that shows the complete development of a small distributed program.     

A tactic language for refinement of state-rich concurrent specifications

Circus is a refinement language in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but since refinements may be long and repetitive, the practical application of this technique can be hard. Useful strategies have been identified, described, and used, and by documenting them as tactics, they can be expressed and repeatedly applied as single transformation rules. Here, we present ArcAngelC, a language for defining such tactics; we present the language, its semantics, and its application in the formalisation of an existing strategy for verification of Ada implementations of control systems specified by Simulink diagrams. We also discuss its mechanisation in a theorem prover, ProofPower-Z.     

Weak Probabilistic Anonymity

Anonymity means that the identity of the user performing a certain action is maintained secret. The protocols for ensuring anonymity often use random mechanisms which can be described probabilistically. In this paper we propose a notion of weak probabilistic anonymity, where weak refers to the fact that some amount of probabilistic information may be revealed by the protocol. This information can be used by an observer to infer the likeliness that the action has been performed by a certain user. The aim of this work is to study the degree of anonymity that the protocol can still ensure, despite the leakage of information.We illustrate our ideas by using the example of the dining cryptographers with biased coins. We consider both the cases of nondeterministic and probabilistic users. Correspondingly, we propose two notions of weak anonymity and we investigate their respective dependencies on the biased factor of the coins.     

加密服务程序CSP的建立方法

本文通过对CSP结构的剖析,详细说明了在WINDOWS操作系统下建立特定的CSP所需要的步骤和开发方法,对CSP开发者有很好的帮助.     

Formal development of industrial-scale systems in <Emphasis Type="BoldItalic">Circus</Emphasis>

Circus is a new notation that may be used to specify both data and behavioural aspects of a system, and has an associated refinement calculus. In this work, we present rules to translate Circus programs to Java programs that use JCSP, a library that implements Communicating Sequential Processes constructs. These rules can be used as a complement to the Circus algebraic refinement technique, or as a guideline for implementation. They are a link between the results on refinement in the context of Circus and a practical programming language in current use. The rules can also be used as the basis for a tool that mechanises the translation. Although a few case studies are already available in the literature, the industrial fire control system, whose refinement and implementation is discussed in this paper, is, as far as we know, the largest case study on the Circus refinement strategy.     

An upper （lower） bound for Max （Min） CSP

The random constraint satisfaction problem(CSP)instances generated by Model RB have been widely used in the field of CSP and have some nice features.In this paper,we consider two optimization versions of CSP,i.e.,the maximum constraint satisfaction problem(Max-CSP)and the minimum satisfaction problem(Min-CSP)of Model RB.The problem of the Max-CSP is how to find an assignment to all the variables such that the maximum number of constraints are satisfied and the problem of Min-CSP is how to find an assignment to all the variables such that the minimum number of constraints are satisfied.We use the first moment method to prove that when r2α(1/p-1)(or p2α/(2α+r)),an upper bound of Max-CSP can be derived.Similarly,we can prove that when r2α(1/p-1)(or p2α/(2α+r)),a lower bound of Min-CSP can be derived.     

Sequential to parallel buffer refinement

This paper is intended to solve a particular problem related to the refinement of a shared sequential buffer into a parallel collection of buffers arising from a study on the IBM CICS project. Using the notion of cooperating refinement we show that the two systems are equivalent from the users' points of view (except with respect to efficiency). This is achieved by constructing an interleaving for each possible sequence of commands which access the buffer. The induction used in the proof is non-standard, and makes the problem harder than it would at first seem. Further we show that the interleaving cannot be done on the fly, showing that in some other sense, the parallel collection is indeed superior, as intuition suggests.This author was supported by the Esprit REX project     

一种从Object—Z到CSP规格说明的转化方法

面向对象形式规格说明语言Object-Z与进程代数CSP相结合是当今的一个热点,它既可以表示复杂的模块化数据与算法,又可以表示系统的行为,但求精与验证对它们结合后的规格说明需要分别进行处理。本文提出了一个方法,把Object-Z规格说明转化为CSP规格说明,可以方便地处理结合后的规格说明,因此求精与推理对结合后的规格说明可以按CSP规则与方法一致来进行处理。此外,转化后的Object-Z规格说明可以按照CSP方法进行模型检查。     

基于USB KEY的CSP实现

CSP是目前应用最广泛的PKI密码接口。CSP终端用户通过Windows提供的CryptoAPI公共接口访问密码函数,而不需要去关心密码运算的具体实现。USB KEY具有使用方便、安全性高、运算能力强等特点,是实现PKI密码运算的理想设备。用户可以通过调用动态库来使用USBKEY的加密运算功能,从而实现CSP所需要的PKI密码函数。本文从CSP的技术原理出发,结合USB KEY的功能特点,深入讨论了如何使用USB KEY实现CSP的功能。     

A LISP implementation of the model for ‘communicating sequential processes’

To explain his abstract model of Communicating Sequential Processes, Hoare includes an implementation of the concepts being expounded as a set of LISP functions. However, the final sections are only described sketchily. This paper completes the missing details, and briefly discusses experience with the system. The usefulness of the implementation is enhanced by the addition of features to ensure that incomplete program fragments can be executed, and that no restrictions are placed on the way operators may be combined.     

Unifying classes and processes

Previously, we presented Circus, an integration of Z, CSP, and Morgan’s refinement calculus, with a semantics based on the unifying theories of programming. Circus provides a basis for development of state-rich concurrent systems; it has a formal semantics, a refinement theory, and a development strategy. The design of Circus is our solution to combining data and behavioural specifications. Here, we further explore this issue in the context of object-oriented features. Concretely, we present an object-oriented extension of Circus called OhCircus. We present its syntax, describe its semantics, explain the formalisation of method calls, and discuss our approach to refinement.     

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.     

基于离散模式的XML数据查询的CSP实现

XML成为WWW上采用的信息交换，表示和存储手段之一，文中给出了基于OEM数据模型的XML数据离散模式概念和基于模式匹配的数据查询概念，重点研究了通过将模式匹配转换到约束满足问题（CSP）来具体求解匹配实例的方法，此方法使WWW上基于内容的查询转变为更为精确的基于结构的查询，理论上证明了这种模式匹配到CSP转换的可行性。     

CSP喷号机数据生成和传输系统

以河北钢铁集团连铸连轧生产线喷号机数据生成和传输系统为例,对喷号机数据生成和传输系统进行分析,详细介绍该系统的工作原理和运行情况。     

工作流建模语言XPDL到CSP进程的转化研究

针对工作流定义标准语言XPDL缺乏形式化语义,提出了将XPDL描述转化为通信顺序进程(CSP)的方法,从而可以利用进程代数CSP理论以加强对工作流模型的语义描述分析检测。通过实例分析具体说明转化方法的有效性。