Advancing Formal Verification

Background

Formal verification is an approach to the development of error-free, dependable hardware and software systems. It is motivated by the high cost of correcting errors in digital designs and computer programs during the later stages of their development cycle (e.g. the Pentium Bug or the Ariane 5 rocket disaster). This cost has been increasing with the ever greater complexity we see in hardware and software systems, and an ever greater integration of both. What is needed are precise yet understandable ways of specifying an abstract model of a system and what would constitute its correct behaviour, and exhaustive methods for determining that the system model behaves correctly for all input patterns, resulting in a dependable system. Formal verification is one approach to the development of such systems. Because of this, it is one of the seven proposals for Grand Challenges in Computer Science that will help to focus UK computing research upon long-term scientific objectives over the coming two decades.

The Logic and Computation Research Group at the Department of Computer Science has an international reputation for its work in this field. In the context of the Liverpool Verification Laboratory the group has started to apply its theoretical and practical work and has contacts with ARM (UK/USA), Motorola Research Labs (UK), and NASA Ames Research Center (USA) concerning the exploitation of its work.

A particular focus of the research within the group is on formal verification by temporal resolution. The results of that research have been published in international journals of high standing and have been applied to real-world problems in the Liverpool Verification Laboratory using the system TRP++.

The project will investigate a number of open research questions in this context. First, there is a range of important real-world problems, for example, feature interaction problems in telecommunications software or access control security protocols for computer systems, to which our current methods do not apply. Second, practical computational aspects of temporal resolution and of its implementation in TRP++ are largely uninvestigated. These questions should be the focus of the proposed research programme.

The Reseach Programme

1. to extend our theoretical work in directions which would allow us to deal with verification problems we are currently not able to solve;
2. to investigate practical aspect of temporal resolution;
3. to implement the results of (1) and (2);
4. to evaluate the theoretical results and their implementation on real-world problems.

Workpackage 1. Theoretical aspects of temporal resolution (Month 1 to 12)

This workpackage will include the consideration of extensions of our work on the monodic fragment of first-order temporal logic to non-monodic fragments and fragments with equality. These logics would considerably extend the range of verification problems we can formalise and possibly solve. Particular attention will be paid to the determination of feature interaction problems and the verification of access control protocols.

Workpackage 2. Practical aspects of temporal resolution (Month 13 to 24)

This workpackage will look at refinements of temporal resolution which would positively influence its performance. Of particular interest could be a combination with semantic resolution. The workpackage will also look at implementation issues, e.g. the choice of suitable data structures and algorithms.

Workpackage 3. Implementation (Month 10 to 26)

In this workpackage the results of the first two workpackages will be implemented and integrated into \texttt{TRP++}.

Workpackage 4. Evaluation and Application (Month 27 to 32)

This workpackage will apply the improved system to a number of real-world verification problems arising in the context of the Liverpool Verification Laboratory related to those problems guiding our work in workpackage 1, which will allow us to evaluate the extend to which the system has improved. Work during this phase should allow the research student to gain industry experience.

The last four months of the project (month 33 to 36) will be spent on writing up the PhD thesis. The research student will produce a series of publications and reports during the project that form the basis of the thesis.

Initial project specific training will be provided by the supervisors of the project. The student will also take part in the Departmental Postgraduate Training Programme, for example, the departmental postgraduate workshop, and the University Postgraduate Research Development Programme.

Additional Information

For additional information concerning the studentship associated with this project please consult the advert. For enquiries concerning this research project and the associated studentship please contact Ullrich Hustadt (e-mail: U.Hustadt@csc.liv.ac.uk).

The project and studentship will start at the beginning of September 2006.

Created and maintained by Ullrich Hustadt, U.Hustadt@csc.liv.ac.uk. Last modified: Fri Apr 7 14:56:08 BST 2006