Paper Info
Title
Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B
Abstract
Event-B is a formal method used for specifying and reasoning about systems. Rodin is a toolset for developing system models in Event-B. Our experiment which is outlined in this paper is aimed at applying Event-B and Rodin to a flash-based filestore. Refinement is a useful mechanism that allows developers to sharpen models step by step. Two uses of refinement, feature augmentation and structural refinement, were employed in our development. Event decomposition and machine decomposition are structural refinement techniques on which we focus in this work. We present an outline of a verified refinement chain for the flash filestore. We also outline evidence of the applicability of the method and tool together with some guidelines.
Year
DOI
Venue
2009
10.1007/978-3-642-10452-7_10
SBMF
Keywords
Field
DocType
reflnement,feature augmentation,flle system,proof,event-b,flash filestore,rodin,structural refinement technique,formal method,structural refinement,event decomposition,models step,flash-based filestore,machine decomposition,∞ash memory,refinement chain,system modeling
File system,Flash memory,Computer science,Real-time computing,Theoretical computer science,Formal methods
Conference
Volume
ISSN
Citations 
5902
0302-9743
13
PageRank 
References 
Authors
0.75
14
2
Name
Order
Citations
PageRank
Kriangsak Damchoom1281.58
Michael Butler21768104.74