Research on method of formal design and verification of memory management based on microkernel architecture

被引：0

作者：

Qian Z.-J. ^{[1
,2
]}

Liu Y.-J. ^{[2
]}

Yao Y.-F. ^{[2
]}

Tang L. ^{[2
]}

Huang H. ^{[1
]}

Song F.-M. ^{[1
]}

机构：

[1] Department of Computer Science and Technology, Nanjing University, Nanjing, 210023, Jiangsu

[2] School of Computer Science and Engineering, Changshu Institute of Technology, Suzhou, 215500, Jiangsu

来源：

Tien Tzu Hsueh Pao/Acta Electronica Sinica | 2017年 / 45卷 / 01期

关键词：

Formal design; Formal verification; Memory management; Operating system; Theorem proving;

D O I：

10.3969/j.issn.0372-2112.2017.01.035

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

The correctness of design and implementation of operating systems is difficult to be described with the traditional quantitative methods, because of the enormous size and complexity. This paper illustrates our method of formal design and verification of microkernel operating system. We construct the system model with the non-deterministic automaton in the assembly level, and use the Hoare triples to describe the previous and post conditions of the interface functions, as the definitions of function correctness. We take the module of memory management in the self-implemented VSOS (Verified Secure Operating System) as an example, to illustrate our formal method. Meanwhile, we formally describe the constructed memory management model and operation semantics of system behaviors in the Isabelle/HOL theorem prover, and verify the correctness of design and implementation of the memory management. The result shows that the method proposed is feasible and efficient. © 2017, Chinese Institute of Electronics. All right reserved.

引用

页码：251 / 256

页数：5

共 11 条

[1]

Alkassar E., Hillebrand M.A., Leinenbach D., Et al., The Verisoft approach to systems verification, Proceedings of the 2nd Working Conference on Verified Software: Theories, Tools, and Experiments, pp. 209-224, (2008)

[2]

Leinenbach D., Petrova E., Pervasive compiler verification-from verified programs to verified systems, Proceedings of the 3rd International Workshop on Systems Software Verification, pp. 23-40, (2008)

[3]

Shao Z., Certified software, Communications of the ACM, 53, 12, pp. 56-66, (2010)

[4]

Stampoulis A., VeriML: A Dependently-Typed, User-Extensible, and Language-Centric Approach to Proof Assistant, (2012)

[5]

Liang H., Feng X., Shao Z., Compositional verification of termination-preserving refinement of concurrent programs, Proceedings of the 23rd EACSL Annual Conference on Computer Science Logic and 29th Annual IEEE Symposium on Logic in Computer Science (CSL-LICS'14), pp. 65:1-65:10, (2014)

[6]

Carbonneaux Q., Hoffmann J., Ramananandro T., Shao Z., End-to-end verification of stack-space bounds for C programs, Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 270-281, (2014)

[7]

Klein G., Andronick J., Elphinstone K., Murray T., Sewell T., Kolanski R., Heiser G., Comprehensive formal verification of an OS microkernel, ACM Transactions on Computer Systems, 32, 1, pp. 1-70, (2014)

[8]

Nipkow T., Paulson L.C., Wenzel M.T., Isabelle/HOL: A Proof Assistant for Higher-Order Logic, (2002)

[9]

Qian Z.-J., Liu W., Huang H., OSOSM: operating system object semantics model and formal verification, Journal of Computer Research and Development, 49, 12, pp. 2702-2712, (2012)

[10]

Sipser M., Introduction to the Theory of Computation, (2012)

← 1 2 →