| EPSRC Reference: |
EP/K022741/1 |
| Title: |
Future filesystems: mechanized specification, validation, implementation and verification of filesystems |
| Principal Investigator: |
Ridge, Dr T |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Leicester |
| Scheme: |
First Grant - Revised 2009 |
| Starts: |
01 May 2013 |
Ends: |
30 April 2015 |
Value (£): |
91,730
|
| EPSRC Research Topic Classifications: |
| Computer Sys. & Architecture |
Fundamentals of Computing |
|
| EPSRC Industrial Sector Classifications: |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
16 Jan 2013
|
EPSRC ICT Responsive Mode - Jan 2013
|
Announced
|
|
|
Summary on Grant Application Form |
Filesystems are extremely important. Users depend on filesystems to store their files whenever they hit "save". Businesses rely on databases to store their data safely, and these databases in turn rely on the filesystem.
Modern filesystems are designed to satisfy many complicated requirements. As a result, implementations are beset with problems. The implementation code is extremely complex, and almost inevitably contains bugs. These bugs can and do lead to data corruption and loss. Development time is very lengthy. Testing is also very lengthy and costly, and does not guarantee to eliminate all bugs. It is often unclear to application developers what guarantees a filesystem provides, so that it becomes extremely difficult to write correct applications for a given filesystem, let alone applications that are portable across different filesystems.
Even NASA was adversely affected by poor filesystem design. On January 21 2004, mission control lost contact with the Mars Exploration Rover (MER) Spirit. Fortunately Spirit had been equipped with a "crippled mode capability" to cope with unforeseen errors, and together with extensive efforts by the operations team, Spirit was returned to operational status 16 days later on February 6. The official report states: "the root cause of the anomaly was a design error in the software module that provides file system services". Without crippled mode capability, "the MER mission may well have been lost". The cost of the mission was estimated at over US$ 800 million.
What can be done to tackle these problems? For many decades, computer scientists have been developing techniques for producing dependable systems. One approach that is receiving much current interest is verification and correctness i.e. mathematical proof that software is correct according to its specification. The widespread need in the digital economy for reliable and dependable systems means that research in this area is increasingly important.
In 2003, Tony Hoare proposed a verification grand challenge for the following 15 years: a verified compiler. Following the NASA MER anomaly, two NASA research scientists, Rajeev Joshi and Gerard Holzmann, proposed a more tractable challenge: to build a verifiable filesystem. We will take up this challenge, and specify and build a verified filesystem.
This work is foundational in nature, but tackles the complexities of real-world systems. We will use very sophisticated and high-level logical techniques combined with state-of-the-art software development techniques to address the full complexity of real-world systems. The verified filesystem has the potential to impact both technologically highly sophisticated organizations such as NASA and internet giants such as Google, Amazon and Facebook, whilst also delivering benefits to end users. A verified filesystem can have a significant impact on many areas of the digital economy. For example, an ultra-reliable filesystem is a key part of the quest for ultra-reliable computing infrastructure, which in turn contributes to the goal of delivering information technology as a utility. Finally, in addition to real-world impact, this research will provide a solid mathematical foundation for further research and verification of critical applications that make use of filesystem functionality, such as databases and persistent message queues.
|
|
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.le.ac.uk |