POSIX file store in Z/Eves: An experiment in the verified software repository
Saved in:
| 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 |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 36337160 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: POSIX file store in Z/Eves: An experiment in the verified software repository – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Freitas%2C+Leo%22">Freitas, Leo</searchLink><i> leo@cs.york.ac.uk</i><br /><searchLink fieldCode="AR" term="%22Woodcock%2C+Jim%22">Woodcock, Jim</searchLink><relatesTo>1</relatesTo><i> jim@cs.york.ac.uk</i><br /><searchLink fieldCode="AR" term="%22Fu%2C+Zheng%22">Fu, Zheng</searchLink><i> zhengfu@itee.uq.edu.au</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Science+of+Computer+Programming%22">Science of Computer Programming</searchLink>. Feb2009, Vol. 74 Issue 4, p238-257. 20p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22POSIX+%28Computer+software+standard%29%22">POSIX (Computer software standard)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+operating+system+standards%22">Computer operating system standards</searchLink><br /><searchLink fieldCode="DE" term="%22Random+access+memory%22">Random access memory</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+storage+devices%22">Computer storage devices</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: 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] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>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.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=36337160 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1016/j.scico.2008.08.001 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 20 StartPage: 238 Subjects: – SubjectFull: POSIX (Computer software standard) Type: general – SubjectFull: Computer operating system standards Type: general – SubjectFull: Random access memory Type: general – SubjectFull: Computer storage devices Type: general Titles: – TitleFull: POSIX file store in Z/Eves: An experiment in the verified software repository Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Freitas, Leo – PersonEntity: Name: NameFull: Woodcock, Jim – PersonEntity: Name: NameFull: Fu, Zheng IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 02 Text: Feb2009 Type: published Y: 2009 Identifiers: – Type: issn-print Value: 01676423 Numbering: – Type: volume Value: 74 – Type: issue Value: 4 Titles: – TitleFull: Science of Computer Programming Type: main |
| ResultId | 1 |
