| EPSRC Reference: |
GR/M07779/01 |
| Title: |
DIET: DEVELOPING IMPLEMENTATION AND EXTENDING THEORY: A SYMBOLIC APPROACH TO REASONING ABOUT LOTOS |
| Principal Investigator: |
Shankland, Professor CE |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computing Science and Mathematics |
| Organisation: |
University of Stirling |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 January 1999 |
Ends: |
30 April 2002 |
Value (£): |
52,856
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
Computer failures can be spectacular, and occasionally fatal, therefore we must find ways of making these systems more reliable. Formal methods can contribute to achieving this, but the chosen formalism must reflect the real world system accurately, otherwise any results proved about he mathematical model may not apply to the real system. Also, since only small studies can be analysed by hand, good tool support is required. Lastly, in order to assist and guide software engineers applying formal methods it is important to have a selection of case studies on which to draw.The proposed programme will address these points by extending the support available for a particular formal method (LOTOS) and its extension (E-LOTUS). In particular, we will: Develop an implementation of a model checker for symbolic temporal logic and Full (symbolic) LOTOS. This will be based upon existing model checkers for concrete LOTOS. Carry out several case studies to demonstrated the effectiveness of the theory and the implemented tool, and to provide guidance for practitioners wishing to adopt this approach. Extend the theory and implementation to include features of the modal mu-calculus, and those introduced in E-LOTUS (particularly timed operators).
|
|
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.stir.ac.uk |