Splitting Atoms - Splitting Atoms Safely (in Software Design)

Project Dates: From July 2005 to November 2008

Project Leader: Prof. Cliff Jones

Staff: Dr. Joey Coleman

Sponsors: EPSRC

 

We hope to offer new ways of (formally) designing large concurrent and/or distributed computations. The development of concurrent programs is hard because interference between processes complicates reasoning. Previous research has provided one successful way of specifying and reasoning about interference using rely and guarantee conditions but these give rise to complex proof obligations whose use should be minimised. The major aim of this proposal is to formulate a development method which might be called refining atomicity. Given a specification of a task, it can be decomposed into sub-tasks. The idea is to use the abstraction of assuming that sub-tasks are executed atomically in early steps of design and then to have formal rules for "splitting the atoms" (i.e. letting the steps of the sub-operations overlap in time). One push for a formal treatment of this idea is indicated by its widespread informal use. Refining atomicity could take its place alongside other formal development methods like operation decomposition and data reification to which the PI has already made major contributions. A formal compositional method for refining atomicity would be of widespread use; a list of related theoretical and practical goals will also be considered.