August 1986 to October 1988
GEC and Plessey Telecommunications Limited
Key team member responsible for specifying and designing a new storage management process for the System X operating system. Specification was in VDM (with rely and guarantee conditions to handle concurrency), and the implementation was in (BT) Coral and POPUS2 assembler.
The techniques were successfully applied to deliver a high reliability product. Central to this was the utilization of my mathematical skills in proving coexistence arguments for this concurrent operating system process.
Reference: Using VDM with Rely and Guarantee-Conditions - Experiences from a Real Project by J.Woodcock and B.Dickinson. VDM Europe (1988).