Specifying distributed CICS in Z: Accessing local and remote resources

The CICS/ESA Intercommunication Guide is a source of information about distributed CICS systems. Among other things, it describes how an application program running on one system can issue a command that will be shipped to a remote system. A resource manager located at the remote system will execute the command and ship back a response.This paper presents a formal specification of the above interaction between application programs and resource managers. Some familiarity with the Z specification language is assumed. The structure of the specification illustrates how it is possible to address separately, and later combine, different aspects of a complex system, including its distributed nature.IBM is a trademark of the International Business Machines Corporation.     

Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time

We prove that weak bisimilarity is decidable in polynomial time between finite-state systems and several classes of infinite-state systems: context-free processes and normed basic parallel processes (normed BPP). To the best of our knowledge, these are the first polynomial algorithms for weak bisimilarity problems involving infinite-state systems.     

What is a free name in a process algebra?

There are two popular approaches to specifying the semantics of process algebras: labelled transition semantics and reaction semantics. While the notion of free name is rather unproblematic for labelled transition semantics this is not so for reaction semantics in the presence of a structural congruence for unfolding recursive declarations.We show that the standard definition of free name is not preserved under the structural congruence. We then develop a fixed point approach to the set of free names and show that it is invariant under the structural congruence.     

Interfaces for Refining Recursion and Procedures

This paper presents novel definitions of interfaced recursion blocks, interfaced procedures, and interfaced recursive procedures for the Refinement Calculus. These definitions allow step-wise refinement rules to be formally stated and proved for these constructs. An interface is associated with a (recursive) call by preceding the body of the implementation by an assertion statement which says that the interface refines to the implementation. An interface will typically be a specification statement, but in principle can be any command. The theory and rules presented in this paper have been mechanised in the theorem prover Isabelle/ZF. Received August 1999 / Accepted in revised form November 2000     

Progress assumption in concurrent systems

A denotational semantics and a sound and complete inequational proof systems for processes with varying degrees of liveness is presented. New insights onquiescence are given concerning the Jonsson characterisation of input/output system. A theory oftransational behaviour of the typecarry out until the end is developed as an application of this concept of process with liveness requirements. The proposed model fully reflects the parallel composition oftransactional requirements, giving the expected composite requirements.     

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.     

Unifying Concurrent and Relational Refinement

Refinement in a concurrent context, as typified by a process algebra, takes a number of different forms depending on what is considered observable, where observations record, for example, which events a system is prepared to accept or refuse. Examples of concurrent refinement relations include trace refinement, failures-divergences refinement and bisimulation.Refinement in a state-based language such as Z, on the other hand, is defined using a relational model in terms of input/output behaviour of abstract programs. These refinements are verified by using two simulation rules which help make the verification tractable.The purpose of this paper is to unify these two standpoints, and we do so by generalising the standard relational model to include additional observable aspects. The central result of the paper is then to develop simulation rules to verify relations such as failures-divergences refinement in a relational setting, and show how these might be applied in a specification language such as Z.     

Z39.50协议的原理及其在分布式检索中的应用

主要围绕如何实现分布式环境中的异种数据源的检索，介绍了Z39．50协议的基本工作原理，以及其在分布式环境中的简单应用。     

Using the Alloy Analyzer to Verify Data Refinement in Z

In the development of critical systems, standards dictate that it is necessary to first design, construct and formally analyse abstract models of the system. Developers must then verify that the final implementation is consistent with these more abstract specifications.Z is an example of a state-based specification language. It has been shown to be effective in a variety of cases—indeed it was developed as part of a joint collaboration between Oxford University's PRG and IBM Hursley for the specification of the CICS system. However, Z's main weakness is that it does not have the necessary tool support: whilst there are associated type checkers, there is no tool for automatically verifying refinement in Z.The contribution of this paper is to show how data refinement in Z can be automatically verified using the Alloy Analyzer. The soundness and joint completeness of the simulation rules for Z have already been established: here we translate them to Alloy. We then show how data types expressed in Z can also be translated to Alloy, before presenting the assertions necessary for the Alloy Analyzer to identify the retrieve relation and hence verify refinement. We present a simple example in which the Alloy Analyzer successfully identifies the retrieve relation between two data types thereby verifying simulation and hence refinement. We conclude the paper with a discussion of the suitability of the Alloy Analyzer for such a task.     

Composing and Refining Dense Temporal Logic Specifications

A dense temporal logic development method for the specification, refinement, composition and verification of reactive systems is introduced. A reactive system is specified by a pair consisting of a machine and a condition that indicate the valid computations of this machine. Compositionality is achieved by indicating whether each step is an environment step, a system step, or a communication step. Refinement can be expressed straightforwardly in the logic because the stutter problem is elegantly solved by using the dense structure of the logic. Compositionality enables us to break refinement between complex systems into refinement between small and simple systems. The latter can then be verified by existing proof rules for refinement which are reformulated in our formalism. Received January 1997 / Accepted in revised form April 2000     

Specifying distributed multi-agent systems in chemical reaction metaphor

This paper presents an application of Chemical Reaction Metaphor (CRM) in distributed multi-agent systems (MAS). The suitability of using CRM to model multi-agent systems is justified by CRM's capacity in specifying dynamic features of multi-agent systems. A case study in an agent-based e-learning system (course material updating) demonstrates how the CRM based language, Gamma, can be used to specify the architectures of multi-agent systems. The effectiveness of specifying multi-agent systems in CRM from the view point of software engineering is further justified by introducing a transformational method for implementing the specified multi-agent systems. A computation model with a tree-structured architecture is proposed to base the design of the specified multi-agent system during the implementation phase. A module language based on the computation model is introduced as an intermediate language to facilitate the translation of the specification of multi-agent systems. The multicast networking technology pragmatizes the implementation of communications and synchronization among distributed agents. The paper also discusses the feasibility of implementing an automatic translation from the Gamma specification to a program in the module language. This work is supported by University of Houston-Downtown Organized Research Committee.     

A note on atomicity: Boosting Test&Set to solve consensus

This short note shows how a simple extension of object types with consensus number 2 boosts them to an infinite consensus number. This extension is a simple embedding of a shared memory write within the base operation defining the corresponding type with consensus number 2. The style of this note is voluntarily informal.     

Spatial-behavioral types for concurrency and resource control in distributed systems

We develop a notion of spatial-behavioral typing suitable to discipline concurrent interactions and resource usage in distributed object systems. Our type structure reflects a resource sensitive model, where a parallel composition type operator expresses resource independence, a sequential composition type operator expresses resource synchronization, and a type modality expresses resource ownership. We model the intended computational systems using a concurrent object calculus. Soundness of our type system is established using a logical relations technique, building on a interpretation of types as properties expressible in a spatial logic.     

A framework for specifying and verifying the behaviour of open systems

Coding no longer represents the main issue in developing software applications. It is the design and verification of complex software systems that require to be addressed at the architectural level, following methodologies which permit us to clearly identify and design the components of a system, to understand precisely their interactions, and to formally verify the properties of the systems. Moreover, this process is made even more complicated by the advent of the “network-centric” model of computation, where open systems dynamically interact with each other in a highly volatile environment. Many of the techniques traditionally used for closed systems are inadequate in this context.We illustrate how the problem of modeling and verifying behavioural properties of open system is addressed by different research fields and how their results may contribute to a common solution. Building on this, we propose a methodology for modeling and verifying behavioural aspects of open systems. We introduce the IP-calculus, derived from the π-calculas process algebra so as to describe behavioural features of open systems. We define a notion of partial correctness, acceptability, in order to deal with the intrinsic indeterminacy of open systems, and we provide an algorithmic procedure for its effective verification.     

基于Z39．50协议的分布式检索在复合型图书馆系统中的应用

通过分析复合型数字图书馆系统信息检索的特性,以及对基于移动主体分布式信息检索技术与Z39．50标准协议的研究,并利用基于移动主体分布式信息检索的灵活性和高效性与Z39．50协议强壮的广播检索能力,设计实现了应用于复合型数字图书馆系统的基于移动主体的分布式检索子系统Web-OPAC,并在ADLibSys项目中得以应用,使跨库检索的准确率和速度得到很大的提高。     

Operations Research Techniques in Manufacturing Planning and Control Systems

This paper investigates the possible uses for operations research (OR) models and techniques in manufacturing planning and control (MPC) systems. We discuss various MPC problems where OR can be applied and the potential inclusion of such models in computer-aided MPC systems. It is found that even though the use of OR techniques in current standard MPC packages is rather restricted, there is a potential for utilizing more OR techniques in computer-aided MPC systems, at least in theory. In practice, OR-related techniques are more often developed as stand-alone systems for decision support as a complement to the MPC system. In this paper, specific OR techniques are discussed for specific MPC problems in terms of applicability and the appropriate type of software solution; none at all, stand-alone system or integrated part of the MPC system.     

The Least Conjunctive Refinement and Promotion in the Refinement Calculus

A syntactic calculation of Morgan's least conjunctive refinement operator for predicate transformers is developed. The operator is used to develop a general approach to lifting relational operators to predicate transformer operators. Predicate transformer versions of the relational conjunction and disjunction operators are considered in detail. The Z-based technique of program promotion is considered in a refinement calculus setting. A standard Z promotion example is recast in the refinement calculus. Received August 1997 / Accepted in revised form January 1999     

Real-time BASIC

A standard for BASIC is nearing completion. An integral part of that standard is a module of the language addressing the needs of real-time applications. This paper describes the features of real-time BASIC, highlighting the concurrency aspects, the mechanisms provided for inter-process communication and synchronization, and for communication with the hardware system. An example showing how the language may be used to control the environment and pump water from a mine shaft is included. The use of the language with a distributed control system is also discussed.     

Complete and ready simulation semantics are not finitely based over BCCSP, even with a singleton alphabet

This note shows that the complete and the ready simulation preorders do not have a finite inequational basis over the language BCCSP when the set of actions is a singleton. Moreover, the equivalences induced by those preorders do not have a finite (in)equational axiomatization either. These results are in contrast with a claim of finite axiomatizability for those semantics in the literature, which was based on the erroneous assumption that they coincide with complete trace semantics in the presence of a singleton set of actions.