Bibliographic Details
| Title: |
POSIX file store in Z/Eves: An experiment in the verified software repository |
| Authors: |
Freitas, Leo leo@cs.york.ac.uk, Woodcock, Jim1 jim@cs.york.ac.uk, Fu, Zheng zhengfu@itee.uq.edu.au |
| Source: |
Science of Computer Programming. Feb2009, Vol. 74 Issue 4, p238-257. 20p. |
| Subjects: |
POSIX (Computer software standard), Computer operating system standards, Random access memory, Computer storage devices |
| Abstract: |
Abstract: We present results from the second pilot project in the international Verification Grand Challenge: a formally verified specification of a POSIX-compliant file store using the Z/Eves theorem prover. The project’s overall objective is to build a verified file store for space-flight missions. Our specification of the file store is based on Morgan and Sufrin’s specification of the UNIX filing system; the proof and its mechanisation in Z/Eves are novel. We show how our work contributes towards building a verified software repository: a set of general theories, proof techniques, and experiments reusable across different domains. [Copyright &y& Elsevier] |
|
Copyright of Science of Computer Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
