| EPSRC Reference: |
EP/C510615/1 |
| Title: |
Splitting atoms safely (in software design) |
| Principal Investigator: |
Jones, Professor CB |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computing Sciences |
| Organisation: |
Newcastle University |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 July 2005 |
Ends: |
30 November 2008 |
Value (£): |
241,118
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
W e hope to offer new ways of (formally) designing large concurrent and/or distributed computations. The development of concurrent programmes is hard because interference between processes complicates reasoning. Previous research has provideda successful way of specifying and reasoning about interference using rely and guarantee-conditions but these give rise to complex proof obligations whoseuse 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 development and then to have formal rules for splitting the atoms (i.e letting the steps of the sub-operations overlap in time). The need 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 (including the case of rely/guarantee-conditions for concurrency) and data reificationto 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.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.ncl.ac.uk |