Name
Abstract | ||
|---|---|---|
File systems are too important, and current ones are too buggy, to remain unverified. Yet the most successful verification methods for functional correctness remain too expensive for current file system implementations-we need verified correctness but at reasonable cost. This paper presents our vision and ongoing work to achieve this goal for a new high-performance flash file system, called BilbyFs. BilbyFs is carefully designed to be highly modular, so it can be verified against a high-level functional specification one component at a time. This modular implementation is captured in a set of domain specific languages from which we produce the design-level specification, as well as its optimised C implementation. Importantly, we also automatically generate the proof linking these two artefacts. The combination of these features dramatically reduces verification effort. Verified file systems are now within reach for the first time. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2626401.2626414 | Operating Systems Review |
Keywords | Field | DocType |
successful verification method,design-level specification,functional correctness,high-level functional specification,current file system implementation,verified file system,new high-performance flash file,modular implementation,verification effort,optimised c implementation | Domain-specific language,File system,Flash file system,Programming language,Computer science,Correctness,Implementation,Real-time computing,Modular design,Functional specification,Operating system | Journal |
Volume | Issue | Citations |
48 | 1 | 10 |
PageRank | References | Authors |
0.54 | 17 | 8 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gabriele Keller | 1 | 657 | 36.02 |
| Toby Murray | 2 | 242 | 17.03 |
| Sidney Amani | 3 | 67 | 5.00 |
| Liam O'Connor | 4 | 44 | 5.02 |
| Zilin Chen | 5 | 23 | 2.53 |
| Leonid Ryzhyk | 6 | 212 | 16.05 |
| Gerwin Klein | 7 | 1450 | 87.47 |
| Gernot Heiser | 8 | 2525 | 137.42 |