| EPSRC Reference: |
GR/K40420/01 |
| Title: |
AUTOMATIC CHECKING OF MESSAGE-PASSING PROGRAMS |
| Principal Investigator: |
Nicole, Dr DA |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Electronics and Computer Science |
| Organisation: |
University of Southampton |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 August 1995 |
Ends: |
30 April 1998 |
Value (£): |
82,368
|
| EPSRC Research Topic Classifications: |
|
| EPSRC Industrial Sector Classifications: |
| Creative Industries |
Information Technologies |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Over the last ten years, major advances have been achieved in the development of symbolic model checking. This is a technique for the testing of a nondeterministic system by the (symbolic) exhaustive enumeration of all possible branches. Direct model checkers can now handle systems of up to 10^5 states, while checkers based on Binary Decision Diagrams, such as SMV developed at Carnegie Mellon University in Pittsburgh, can manage systems of up to 10^10 states. So far, these techniques have been applied principally to hardware design and to protocol checking, for example for multiprocessor cache architectures. The principal novel aspect of this proposal is the application of model checking to parallel program development, in order to catch possible deadlock, livelock and other problems during the program design cycle. Considerable sophistication will also be required in the choice of data-dependent state to be ignored-resulting in increased nondeterminism, and in the ordering of BDD states. Message passing FORTRAN is the principal target of our work, but occam has been chosen for a preliminary implementation as it serve as a briding language between application programming, protocol design and hardware specification. We have direct applications for the occam system in each of these domains.
|
|
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.soton.ac.uk |