Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Multi-threading and message communication in Qu-Prolog

This paper presents the multi-threading and internet message communication capabilities of Qu-Prolog. Message addresses are symbolic and the communications package provides high-level support that completely hides details of IP addresses and port numbers as well as the underlying TCP/IP transport layer. The combination of the multi-threads and the high level inter-thread message communications provide simple, powerful support for implementing internet distributed intelligent applications.

Parametric signal regeneration

We present an ultra-high bandwidth all-optical digital signal regeneration device concept utilising non-degenerate parametric interaction in a one-dimensional waveguide. Performance is analysed in terms of re-amplification, re-timing, and re-shaping (including centre frequency correction) of time domain multiplexed signals. Bandwidths of 10-100 THz are achievable. (C) 2001 Published by Elsevier Science B.V.

Thue's theorem and the diophantine equation x2 - Dy2 = ±N

A constructive version of a theorem of Thue is used to provide representations of certain integers as x(2) - Dy-2, where D = 2, 3, 5, 6, 7.

Steiner trades that give rise to completely decomposable latin interchanges

In this paper we focus on the representation of Steiner trades of volume less than or equal to nine and identify those for which the associated partial latin square can be decomposed into six disjoint latin interchanges.

On the Hamilton-Waterloo problem

The Hamilton-Waterloo problem asks for a 2-factorisation of K-v in which r of the 2-factors consist of cycles of lengths a(1), a(2),..., a(1) and the remaining s 2-factors consist of cycles of lengths b(1), b(2),..., b(u) (where necessarily Sigma(i)(=1)(t) a(i) = Sigma(j)(=1)(u) b(j) = v). In thus paper we consider the Hamilton-Waterloo problem in the case a(i) = m, 1 less than or equal to i less than or equal to t and b(j) = n, 1 less than or equal to j less than or equal to u. We obtain some general constructions, and apply these to obtain results for (m, n) is an element of {(4, 6)1(4, 8), (4, 16), (8, 16), (3, 5), (3, 15), (5, 15)}.

The three-way intersection problem for latin squares

The set of integers k for which there exist three latin squares of order n having precisely k cells identical, with their remaining n(2) - k cells different in all three latin squares, denoted by I-3[n], is determined here for all orders n. In particular, it is shown that I-3[n] = {0,...,n(2) - 15} {n(2) - 12,n(2) - 9,n(2)} for n greater than or equal to 8. (C) 2002 Elsevier Science B.V. All rights reserved.

The metamorphosis of lambda-fold K-3,K-3-designs into lambda-fold 6-cycle systems

In this paper necessary and sufficient conditions are given for the metamorphosis of a lambda-fold K-3,K-3-design of order n into a lambda-fold 6-cycle system of order n, by retaining one 6-cycle subgraph from each copy of K-3,K-3, and then rearranging the set of all the remaining edges, three from each K-3,K-3, into further 6-cycles so that the result is a lambda-fold 6-cycle system.