|
| EPSRC Reference: |
EP/D070880/1 |
| Title: |
A Unified Approach to Compositional Software Modelling, Analysis and Verification |
| Principal Investigator: |
Dr DR Ghica |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Birmingham |
| Scheme: |
Advanced Fellowship |
| Starts: |
01 July 2006 |
Ends: |
30 June 2011 |
Value (£): |
386,160
|
| EPSRC Research Topic Classifications: |
| Modelling and Simulation of IT Systems |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
Software modelling, analysis and verification
comprises many sophisticated but often disparate techniques such as
model checking, static analysis or testing. Although taken
individually such techniques are effective in targeting particular
problems, a combined approach is always recommended. However, in the
absence of a unified framework, integration can be awkward and may
fail to achieve true synergy. Using Game Semantics as a common
theoretical foundation we can provide such a unified framework for
software modelling, analysis and verification. The modularity of
extant techniques is often limited, which restrains their
scalability. Game Semantics is intrinsically compositional and recent
research has already shown how it can be used to model subprograms in
modular fashion, especially the subtle interplay between procedures
and state that cannot be represented using extant techniques. However,
compositional modelling is only the first step towards compositional
verification. We plan to further develop means for compositional
reasoning, that is methods of specifying properties of execution
environments and of verifying that subprograms plug together without
violating their mutual assumptions. This can be achieved using either
program logics or type systems. Building on existing research, we aim
to push compositional methods beyond correctness verification, into
more intensional analyses such as estimating time of execution, memory
requirements or resource usage. We also aim to expand beyond static
verification, by examining compositional approaches to
testing. Throughout the programme, foundational and applied research
will naturally intertwine and play off each other.
|
| Final Report Summary |
|
No final report summary is available for this grant.
|
| Further Information: |
|
| Organisation Website: |
http://www.bham.ac.uk |
|
|