Title :
POSIX file store in Z/Eves: an experiment in the verified software repository
Author :
Freitas, Leo ; Fu, Zheng ; Woocock, J.
Author_Institution :
Univ. of York, York
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 & 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 and experiments reusable across different domains.
Keywords :
Unix; file organisation; formal specification; theorem proving; POSIX-compliant file store; UNIX filing system; Z/Eves theorem prover; file store specification; space-flight mission; verified file store; verified software repository; Application software; Banking; Computer industry; Computer science; Concrete; Fault tolerance; File systems; Hardware; Programming; Software tools;
Conference_Titel :
Engineering Complex Computer Systems, 2007. 12th IEEE International Conference on
Conference_Location :
Auckland
Print_ISBN :
0-7695-2895-3
DOI :
10.1109/ICECCS.2007.36
