Paper Info
Title
Modelling and Proof of a Tree-Structured File System in Event-B and Rodin
Abstract
Event-B is a formalism used for specifying and reasoning about complex discrete systems. The Rodin platform is a new tool for specification, refinement and proof in Event-B. In this paper, we present a verified model of a tree-structured file system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities affecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a file system, we begin with an abstract model of a file system and subsequently refine it by adding more details through refinement steps. We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.
Year
DOI
Venue
2008
10.1007/978-3-540-88194-0_5
ICFEM
Keywords
Field
DocType
refinement step,accurate model,file system,proof obligation,complex discrete system,similar proof obligation,abstract model,rodin platform,tree-structured file system,basic functionalities,refinement,tree structure,proof,discrete system
File system,Computer science,Theoretical computer science,Invariant (mathematics),Tree structure,Formalism (philosophy)
Conference
Volume
ISSN
Citations 
5256
0302-9743
15
PageRank 
References 
Authors
0.83
9
3
Name
Order
Citations
PageRank
Kriangsak Damchoom1281.58
Michael Butler21768104.74
Jean-raymond Abrial31275167.86