Analysis of a File System Using the Verifying C Compiler
| Název práce v češtině: | Analýza souborového systému pomocí Verifying C Compiler |
|---|---|
| Název v anglickém jazyce: | Analysis of a File System Using the Verifying C Compiler |
| Klíčová slova: | Formal Verification, File System, VCC |
| Klíčová slova anglicky: | Formal Verification, File System, VCC |
| Akademický rok vypsání: | 2012/2013 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | doc. RNDr. Jan Kofroň, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 08.11.2012 |
| Datum zadání: | 08.11.2012 |
| Datum potvrzení stud. oddělením: | 27.11.2012 |
| Datum a čas obhajoby: | 03.02.2015 09:00 |
| Datum odevzdání elektronické podoby: | 06.12.2014 |
| Datum odevzdání tištěné podoby: | 05.12.2014 |
| Datum proběhlé obhajoby: | 03.02.2015 |
| Oponenti: | RNDr. David Bednárek, Ph.D. |
| Zásady pro vypracování |
| 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. |
| Seznam odborné literatury |
| [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 |