التفاصيل البيبلوغرافية
| العنوان: |
POSIX file store in Z/Eves: An experiment in the verified software repository |
| المؤلفون: |
J. Woocock, Leo Freitas, Zheng Fu |
| المصدر: |
ICECCS |
| بيانات النشر: |
Elsevier BV, 2009. |
| سنة النشر: |
2009 |
| مصطلحات موضوعية: |
POSIX, Computer science, Application software, computer.software_genre, Set (abstract data type), Design rule for Camera File system, Formal specification, Versioning file system, Theorem proving, Unix, Grand challenge, Programming language, Computer file, File descriptor, Working directory, Verification, Fault tolerance, computer.file_format, Everything is a file, Unix file types, Virtual file system, Flash memory, File systems, Automated theorem proving, Operating system, Software repository, computer, Software |
| الوصف: |
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. |
| تدمد: |
0167-6423 |
| DOI: |
10.1016/j.scico.2008.08.001 |
| URL الوصول: |
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::74ee160a8698457a1a26abe0e33286fc |
| Rights: |
OPEN |
| رقم الانضمام: |
edsair.doi.dedup.....74ee160a8698457a1a26abe0e33286fc |
| قاعدة البيانات: |
OpenAIRE |