Thesis Topic Details

Topic ID:
3515
Title:
Implementing Verified File Systems in a Domain Specific Language
Supervisor:
Toby Murray
Research Area:
Operating Systems, Programming Languages, Formal Methods
Associated Staff
Assessor:
Gernot Heiser
Topic Details
Status:
Active
Type:
R & D
Programs:
CS CE SE
Group Suitable:
No
Industrial:
No
Pre-requisites:
Operating Systems
Description:
NICTA is currently producing the world's first formally verified file system, as part of its Trustworthy Filesystems research project. That research project aims to radically reduce the cost of producing formally verified systems code by writing it in a domain specific language (DSL), from which both a C implementation and associated correctness proofs are generated. This development methodology is being trialled on a high-performance flash file system design, called BilbyFs.

This thesis project aims to explore the generality of the DSL being used for BilbyFs, by using it to produce verified implementations of other file systems. You will write versions of well-known file systems in the DSL, from which both their C code implementations as well as Isabelle proofs of correctness can be generated by the DSL compiler. In doing so, you would be producing perhaps the first verified C code implementations of these file systems.

Further details about the Trustworthy Systems project can be found at:
http://www.ssrg.nicta.com.au/projects/TS/filesystems.pml
Comments:
--
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.