Analysis of a File System Using the Verifying C Compiler
| Thesis title in Czech: | Analýza souborového systému pomocí Verifying C Compiler |
|---|---|
| Thesis title in English: | Analysis of a File System Using the Verifying C Compiler |
| Key words: | Formal Verification, File System, VCC |
| English key words: | Formal Verification, File System, VCC |
| Academic year of topic announcement: | 2012/2013 |
| Thesis type: | diploma thesis |
| Thesis language: | angličtina |
| Department: | Department of Distributed and Dependable Systems (32-KDSS) |
| Supervisor: | doc. RNDr. Jan Kofroň, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 08.11.2012 |
| Date of assignment: | 08.11.2012 |
| Confirmed by Study dept. on: | 27.11.2012 |
| Date and time of defence: | 03.02.2015 09:00 |
| Date of electronic submission: | 06.12.2014 |
| Date of submission of printed version: | 05.12.2014 |
| Date of proceeded defence: | 03.02.2015 |
| Opponents: | RNDr. David Bednárek, Ph.D. |
| Guidelines |
| Verifier for Concurrent C (VCC) [1,2] is a tool that accepts an annotated C code and automatically verifies its correctness with respect to the given annotations. As proposed in [3], an interesting challenge for such a tool is specification and verification of a (simple) file system.
The goal of this thesis is to: - Study the VCC tool - Choose an existing real file system (tmpfs [4] or FatFS [5]) - Make an attempt to specify it using the VCC annotations - Analyze it using the VCC tool - Document the experiment in the text of the thesis This is a research work, in which a failure of the experiment is a perfectly acceptable result, provided that the reasons of the failure are well-documented and justified. |
| References |
| [1] Microsoft, VCC: A Verifier for Concurrent C, http://research.microsoft.com/en-us/projects/vcc/
[2] E. Cohen, M. Moskal, W. Schulte, and S. Tobies, A Practical Verification Methodology for Concurrent Programs, Technical Report no. MSR-TR-2009-15, February 2009 [3] R. Joshi and G. J. Holzmann, A mini challenge: build a verifiable filesystem. Form. Asp. Comput. 19, 2 (Jun. 2007), 269-272. [4] Linux kernel, tmpfs, http://www.kernel.org/doc/Documentation/filesystems/tmpfs.txt [5] FatFs - Generic FAT File System Module, http://elm-chan.org/fsw/ff/00index_e.html |