Modeling and Proof of a File System Based on Micro-Kernel

Hong Ying Tang; Zhen Jiang  Qian; Hao Huang

doi:10.4028/www.scientific.net/AMR.765-767.837

Paper Titles

An Algorithm of Global Path Planning Applied for Rapid Prototyping
p.817

A Blind Watermarking Algorithm for 2D CAD Drawings Based on SVD
p.821

Reversible Watermarking Algorithm in DFT Domain for 2D CAD Engineering Graphics
p.826

The Application of Open Scene Graph Technology in Visualization of Aircraft Route Planning
p.833

Modeling and Proof of a File System Based on Micro-Kernel
p.837

The Platform Designing of Resources Construction Based on Virtual Synergistic Technology
p.841

A Research of 3D Industrial Land Information Management System Based on Stamp Platform – A Case Study of Jintan County
p.845

Cloud Computing Environment Data Mining Storage Management Design
p.850

A Project-Based Approach to Teaching Programmable Logic Controller Course
p.854

HomeAdvanced Materials ResearchAdvanced Materials Research Vols. 765-767Modeling and Proof of a File System Based on...

Modeling and Proof of a File System Based on Micro-Kernel

Abstract:

As the manager of the data stored in the disk, the security of the file system is an important aspect of the operating system. Given the high logicalness and unambiguousness of the formal methods, also the module independence of the micro-kernel, this paper abstracts a formal model from the file system implementation based on micro-kernel, and then gives the axiomatic semantics of the initialization; finally, gives the correctness assertions of file system initialization, then verify the correctness of the formal model of file system aided with Isabelle/HOL.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Advanced Materials Research (Volumes 765-767)

Pages:

837-840

DOI:

https://doi.org/10.4028/www.scientific.net/AMR.765-767.837

Citation:

Cite this paper

Online since:

September 2013

Authors:

Hong Ying Tang, Zhen Jiang Qian, Hao Huang

Keywords:

Correctness, File System, Formal Method, Formal Verification, Isabelle/HOL

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] C.C. Morgan, B.A. Sufrin. Specification of the Unix filing system [J]. IEEE Trans. Software Engng, March 1984, SE-10(2): 128-142.

DOI: 10.1109/tse.1984.5010215

Google Scholar

[2] Wenzel,M. Some aspect of Unix file-system security[J]. Isabelle/Isar proof document. T.U. Mun-chen, (2001).

Google Scholar

[3] Damchoom,K., Butler,M., Abrial J.R. Modelling and Proof of a Tree-structured File System in Event-B and Rodin[C]. ICFEM, 2008, 25-44.

DOI: 10.1007/978-3-540-88194-0_5

Google Scholar

[4] Wim H. Hesselink M.I. Lali. Formalizing a hierar-chical file system[J]. Electron. Notes Theor. Co-mput. Sci., December 2009, 259: 67-85.

Google Scholar

[5] Galloway,A., Luttgen,G., Muhlberg,J. et al. Model-Checking the Linux Virtual File System[C]. VMCAI. 2009, 74-88.

Google Scholar

[6] Tobias NIPKOW, Lawrence C. PAULSON, Markus WENZEL . A Proof Assistant for Higher-Order Logic[M], Berlin: Springer-Verlag, 2012: 1-223.

Google Scholar

[7] Chaochen Zhou. Introduction of formal semantics[M]. Hunan science and technology Press, 1985. In Chinese.

Google Scholar

[8] Gerwin KLEIN, Kevin ELPHINSTONE, Gernot Heiser. SeL4: Formal Verification of an OS kernel[J]. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles, 2009. 10.

DOI: 10.1145/1629575.1629596

Google Scholar