Recent advances in theory and tool support have inspired industrial and academic researchers to join up in an international Grand Challenge (GC) in Verified Software, and have created a sense of urgency in making its objectives a reality. The main motto of the GC is that
The first VSR pilot project experiment took place during 2006. This involved the successful mechanisation of the verification of a commercially sanitised version of the first project to meet the high-assurance standard, ITSEC Level 6: the Mondex smart-card banking application. The original formal specification and design are publicly available, and the mechanisation was accomplished by seven groups using different theories and tools. Their work is being recorded in a special issue of the Formal Aspects of Computing Journal. Further information on VSR can be found here.
In the first conference on Verified Software: Theories, Tools, and Experiments, held in Zurich in 2005, Joshi and Holzmann suggested a new pilot project for the grand challenge: the specification and verification of the POSIX file-store interface of Unix. It involves a small subset of POSIX (which is detailed below) suitable for flash-memory hardware with strict fault-tolerant requirements to be used by forthcoming NASA's Jet Propulsion Laboratory missions. Obviously, we do not stop there: following the GC's motto, we see this as an important research opportunity far beyond JPL's original pilot project.
The challenge proposed for participants at the ABZ 2008 Conference is for them to make a significant contribution to the file-store pilot project. Is the mechanical verification of a practical system within the state of the art? Can high levels of automation be achieved? Can useful guarantees be given about the dependability of the system across different hardware platforms? How do different theories, tools, and technique compare?
A series of informal development workshops will be organised leading up to the ABZ 2008 Conference for those who are going to work on the problem. This is inspired by what we did on the Mondex project, where the workshops gave useful deadlines for people to make progress and to interact. It will also give an opportunity for groups to parcel out the work, so that we might proceed collaboratively rather than competitively. It may even be the case that groups might be able to agree on a common notation to work in.
Work has started on this project, following an architecture set out by Intel (see documentation here). This architecture explains how to separate and then orthogonally combine the following aspects of file systems:
The functional requirements specification for POSIX file systems are hosted by the Open Group (see the catalogue of documentation), and was agreed as a standard for Unix implementations in 2003. Before this, an early attempt at producing this requirements document used the Z Notation to straighten out unresolved ambiguities (see the resulting Z document). The Open Group requirements document was originally inspired by available Unix file systems formal specifications, such as Morgan and Sufrin's paper on the Unix filing system.
The VSR group at the University of York is working on the functional specification, following an initial subset of the POSIX API discussed with JPL. This minimal POSIX interface focuses on the basic functionality of files and directories, where we want to support at least the following API:
We also agreed with JPL to opt for a very conservative guarantee about concurrent behaviour: that the result of executing concurrent operations is equivalent to executing them in some serial order. This guarantee entails a performance cost, which is being traded for simplicity. But this may be too strict a requirement for a general embedded file-system, so this issue remains open in the context of the grand challenge, and so presents yet another research opportunity to those who want to get involved.
The results obtained between May 2006 and May 2007 are:
HashMap.Although a general Intel architecture integrating the file system functionality with varied hardware is possible, we again turn our attention to one particular target: NAND flash-memory. This type of hardware has been standardised quite recently by ONFI. In collaboration between Trinity College Dublin and the University of York, we have started formalising ONFI's standard.
Due to the nature of the environment this small functional subset would run in, two important robustness requirements for fault-tolerance were later agreed with JPL:
It is expected that each group working on the problem will submit a paper to ABZ 2008 in the normal way. They will also be asked to deposit their work in the Verified Software Repository, and to submit a longer, more technical paper to a special issue of a leading journal.
There are a series of other pilot projects beside POSIX. We list further information about them in the list below.
Dr. Leo Freitas or
Prof. Jim Woodcock
Department of Computer Science,
University of York, YO10 5DD, UK