Formal Verification of Memory Management System in Spacecraft Using Event-B
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61502031, 61632005)

  • Article
  • | |
  • Metrics
  • |
  • Reference [30]
  • |
  • Related
  • |
  • Cited by [1]
  • | |
  • Comments
    Abstract:

    In the safety-critical system of spacecraft, memory management system is the essential part of operating system kernels to provide allocation and cleanup mechanism at the lowest level and is obviously critical to the reliability and safety of spacecraft computer systems. The memory management system should satisfy strict constraints such as real-time response, space usage limit, allocation efficiency and many boundary conditions. It has to use very complex data structures and algorithm to manage the whole memory space. In order to make the complex memory management system of spacecraft highly reliable, the formal verification of the system also becomes much more complicated as it embodies formal verification of complex data structures such as two level segregated double linked list with two level bitmaps, specification of operations, modeling on behavior, assertion definition of inner function, loop invariant definition and real-time verification. This paper provides an in-depth analysis on these problems and characteristics of spacecraft memory management system to find certain general method and theory based on hierarchical iteration for verifying a concrete operating system used on spacecraft. The results of this study offer potential benefits in improving the reliability of the spacecrafts of China.

    Reference
    [1] Jackson D. A direct path to dependable software. Communications of the ACM, 2009,52(4):78-88. [doi: 10.1145/1498765.14987 87]
    [2] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1983,26(1):53-56. [doi: 10.1145/35798 0.358001]
    [3] Lamport L. Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering, 1977,2(3):125-143. [doi: 10. 1109/TSE.1977.229904]
    [4] Reeves G, Neilson T. The mars rover spirit FLASH anomaly. In: Proc. of the Aerospace Conf. IEEE, 2005. [doi: 10.1109/AERO.20 05.1559723]
    [5] Krebbers R, Leroy X, Wiedijk F. Formal C semantics: CompCert and the C standard. In: Proc. of the 5th Conf. on Interactive Theorem Proving (ITP 2014). Vienna: Springer-Verlag, 2014. 543-548. [doi: 10.1007/978-3-319-08970-6_36]
    [6] Baumann C, Bormer T. Verifying the PikeOS microkernel: First results in the Verisoft XT Avionics project. In: Proc. of the Doctoral Symp. on Systems Software Verification (SSV 2009). 2009. 20-22.
    [7] Yu DC, Hamid NA, Shao Z. Building Certified Libraries for PCC: Dynamic Storage Allocation. Berlin, Heidelberg: Springer- Verlag, 2003. [doi: 10.1007/3-540-36575-3_25]
    [8] Saltzer JH, Kaashoek MF. Principle of Computer System Design, An Introduction. Morgan Kaufmann Publishers, 2009.
    [9] Wilcox M. I'll do it later: Softirqs, tasklets, bottom halves, task queues, work queues and timers. linux.conf.au, 2003.
    [10] Corbet J, Rubini A, Kroah-Hartman G. Linux Device Drivers. 3rd ed., Oreilly and Associates Inc., 2005.
    [11] McKusick MK, Neville-Neil GV. The Design and Implementation of the FreeBSD Operating System. Pearson Education, 2004.
    [12] Walker BJ, Kemmerer RA, Popek GJ. Specification and verification of the UCLA Unix security kernel. Communications of the ACM, 1980,23(2):118-131. [doi: 10.1145/358818.358825]
    [13] Mel G. Understanding the Linux Virtual Memory Manager. Upper Saddle River: Prentice Hall, 2004.
    [14] Marco Cesati DP. Understanding the Linux Kernel. 3rd ed., O'Reilly Media, Inc., 2005.
    [15] Love R. Linux Kernel Development. 3rd ed., Novel Press, 2005.
    [16] Fankhauser G, Conrad C, Zitzler E, Plattner B. Topsy-A teachable operating system [Ph.D. Thesis]. ETH Zürich: Computer Engineering and Networks Laboratory, 2000.
    [17] Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4: Formal verification of an OS kernel. In: Proc. of ACM SIGOPS the 22nd Symp. on Operating Systems Principles. ACM, 2009. 207-220. [doi: 10.1145/1629575.1629596]
    [18] Klein G. Operating system verification-An overview. Sadhana, 2009,34(1):27–69. [doi: 10.1007/s12046-009-0002-4]
    [19] Klein G, Tuch H. Towards verified virtual memory in L4. In: Proc. of the TPHOLS EMERGING TRENDS 2004. Park City, 2004.
    [20] Qiao L, Yang MF, Gu B. An embedded operating system design for the Lunar exploration rover. In: Proc. of the 5th IEEE Conf. on SSIRI. 2011. 160-165. [doi: 10.1109/SSIRI-C.2011.39]
    [21] Masmano M, Ripoll A, Crespo A, Real J. TLSF: A new dynamic memory allocator for real-time systems. In: Proc. of the ECRTS. 2004. 79-88. [doi: 10.1109/EMRTS.2004.1311009]
    [22] Masmano M, Ripoll I, Balbastre P, Crespo A. A constant-time dynamic storage allocator for real-time systems. Real-Time Systems, 2008,40(2):149-179. [doi: 10.1007/s11241-008-9052-7]
    [23] Marinak KG, Bradley J, Feehan J, Medeiros H, Patel N. Amiga operating system: A brief discussion about history and specifications. 2014. http://www.amiga.com
    [24] Crespo A, Ripoll I, Masmano M, Arberet P, Metge JJ. XtratuM: An open source Hypervisors for TSP embedded systems in aerospace. 2014. http://www.xtratum.org
    [25] Open Robot Control Software. 2013. http://www.orocos.org
    [26] Abrial JR, Leino R. Mini-Course around Event-B and Rodin: hypervisor. 2011. http://research.microsoft.com/apps/video/default. aspx?id=151665
    [27] Abrial JR. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
    [28] Hu YC. Research on dynamic memory management of embedded real-time system ARTs-OS [MS. Thesis]. Wuhan: Huazhong University of Science and Technology, 2010 (in Chinese with English abstract).
    附中文参考文献:
    [28] 胡雨翠.嵌入式实时系统ARTs-OS的动态内存管理研究[硕士学位论文].武汉:华中科技大学,2010.
    Related
    Comments
    Comments
    分享到微博
    Submit
Get Citation

乔磊,杨孟飞,谭彦亮,蒲戈光,杨桦.基于Event-B的航天器内存管理系统形式化验证.软件学报,2017,28(5):1204-1220

Copy
Share
Article Metrics
  • Abstract:4315
  • PDF: 6878
  • HTML: 3260
  • Cited by: 0
History
  • Received:August 30,2016
  • Revised:September 25,2016
  • Online: January 22,2017
You are the first2033294Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063