The long-standing relationship between Oxford University’s Programming Research Group and IBM’s CICS software has entered a new phase which may some day lead to communicating concurrent versions of CICS in the commercial market. The relationship, inspired by one of IBM’s leading software gurus Harlan Mills in charge of Federal Systems Division programming, began five years ago. Mills saw potential for big savings for IBM when enhancing large existing pieces of system software such as CICS, if it had resort to a formal definition of that system. Oxford’s team was given the contract to do just that in 1982, and proceeded to use the Z definition language, a non-computer language that is really a system of mathematical notation with which to define software function. IBM’s internal education has seen to it that all system software developers are versed in formal methods, and with the recently-completed Z definition of the core of CICS, subsequent changes to CICS should be a lot cheaper for IBM to write, and a lot less painless for the user to install. By extending the formal Z specification, and adhering to it when developers code a new version, IBM can make sure that it does not disturb existing fuctions and instead adds only new ones. Now the Oxford team is working on an extension to Z so that it can benefit from the branch of mathematics developed by Professor Tony Hoare at Oxford, called Communicating Sequential Processes upon which the Occam programming language for the Inmos Transputer is based. When complete in two years or so this will give IBM the basic tool for building versions of CICS (if it chooses to) which run concurrently and communicate with each other, or which can place different parts of single transactions across a number of different processors. Although IBM would be the first to point out that this is purely theoretical research, the Oxford group, working IBM’s Hursley Laboratories in Hampshire will be building a case study to demonstrate how Z can be used to define an effective concurrent system. And IBM would only need a Z definition of any other piece of its strategic software to carry across the same advantage to these other products.