微信服务号

微信订阅号

2025-4-13- 3
Home > Archive>Volume 31, Issue 8, 2020 >2375-2387. DOI:10.13328/j.cnki.jos.005961
PDF HTML XML Export Cite reminder
Operating System Task Management Requirements Layer Modeling and Verification Based on Coq
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61632005, 61502031); Open project of State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (SYSKF1804)

  • Article
    • | |
  • Metrics
    • |
  • Reference [27]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    In order to ensure the reliability of task management design in the operating system on the satellite, the theorem proving tool Coq is used to requirements layer modeling and formal verification of the operating system task management module. From the user point of view for the basic mechanism of on-board operating system task management, this study proposes verification method based on task state list collection. The mechanism process is formalized and implemented in Coq. Six properties are consistent with the task management of the real-world operating system for the established requirements layer model. This article gives a verification process of one of the properties in Coq. The result shows that the model satisfies the properties of the article.

    Reference
    [1] Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engerlhardt K, Kolanski R, Norrish M, Sewell T. seL4:Formal verification of an OS kernel. In:Proc. of the ACM SIGOPS 22nd Symp. on Operating Systems Principles. 2009. 207-220.
    [2] Gu RH, Koenig J, Ramananandro T, Shao Z, Wu XN, Weng SC, Zhang HZ, Guo Y. Deep specifications and certified abstraction layers. In:Proc. of the 42nd ACM Symp. on Principles of Programming Languages (POPL 2015). 2015. 595-608.
    [3] Gu RH, Shao Z, Chen H, Wu XN, Kim J, Sjoberg V, Costanzo D. CertiKOS:An extensible architecture for building certified concurrent OS kernels. In:Proc. of the 12th USENIX Symp. on Operating Systems Design and Implementation (OSDI 2016). 2016. 653-669.
    [4] Feng XF, Shao Z, Guo Y, Dong Y. Combining domain-specific and foundational logics to verify complete software systems. In:Proc. of the VSTTE 2008. 2008. 54-69.
    [5] Liang HJ, Feng XF, Fu M. A rely-guarantee-based simulation for verifying concurrent program transformations. In:Proc. of the 39th ACM Symp. on Principles of Programming Languages (POPL 2012). 2012. 455-468.
    [6] Xu FW, Fu M, Feng XF, Zhang XR, Zhang H, Li ZH. A practical verification framework for preemptive OS kernel. In:Proc. of the Int'l Conf. on Computer Aided Verification. Springer-Verlag, 2016. 57-59.
    [7] Barras B, Boutin S, Cornes C, Courant J, Coscoy Y, Delahaye D, de Rauglaudre D, Filliâtre JC, Giménez E, Herbelin H, Huet G, Laulhère H, Loiseleur P, Muñoz C, Murthy C, Parent C, Paulin C, Saïbi A, Werner B. The Coq Proof Assistant Reference Manual-Version V6.3. 1999.
    [8] Chen H, Wu XN, Shao Z, Lockerman J, Gu RH. Toward compositional verification of interruptible OS kernels and device drivers. In:Proc. of the 37th ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). 2016. 431-447.
    [9] Guo Y, Feng XF, Shao Z, Shi P. Modular verification of concurrent thread management. In:Proc. of the 10th Asian Symp. on Programming Languages and Systems (APLAS). 2012. 315-331.
    [10] Feng XF, Shao Z, Dong Y, Guo Y. Certifying low-level programs with hardware interrupts and preemptive threads. Journal of Automated Reasoning, 2009,42(2-4):301-347.
    [11] Ma D, Fu M, Qiao L, Feng XY. Formal specification and verification of complex kernel data structures. Journal of Chinese Computer Systems, 2019,40(2):359-366(in Chinese with English abstract).
    [12] Andronick J, Lewis C, Matichuk D, Morgan C, Rizkallah C. Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency. Berlin:Springer-Verlag, 2016. 52-68.
    [13] Cao QX, Beringer L, Gruetter S, Dodds J, Appel AW. VST-Floyd:A separation logic tool to verify correctness of C programs. Journal of Automated Reasoning, 2018,61(1-4):1-56.
    [14] Zou M, Ding HR, Du D, Fu M, Gu RH, Chen HB. Using concurrent relational logic with helper for verifying the AtomFS file system. In:Zou M, Ding HR, Du D, Fu M, Gu RH, Chen HB, et al., eds. Proc. of the 27th ACM Symp. on Operating System Principles. Deerhurst Resort, 2019.
    [15] Wang HB, Guo Y, Chen YY. Verification multithreaded Code with dynamic thread creation and termination. Journal of Chinese Computer Systems, 2010,31(8):1637-1642(in Chinese with English abstract).
    [16] Ma JB, Fu M, Feng XY. Formal verification of the message queue communication mechanism in μC/OS-II. Journal of Chinese Computer Systems, 2016,37(6):1179-1184(in Chinese with English abstract).
    [17] Gu HB, Fu M, Qiao L, Feng XY. Formalization and verification of several global properties of SpaceOS. Journal of Chinese Computer Systems, 2019,40(1):141-148(in Chinese with English abstract).
    [18] Simon W, Gerwin K, Thomas S, June A, David C, Michael N. Mind the gap:A verification framework for low-level C. In:Berghofer S, Nipkow T, Urban C, Wenzel M, eds. Proc. of the 22nd TPHOLs. LNCS 5674, Springer-Verlag, 2009. 500-515.
    [19] Qiao L, Yang MF, Tan YL, Pu GG, Yang H. Formal verification of memory management system in spacecraft using Event-B. Ruan Jian Xue Bao/Journal of Software, 2017,28(5):1204-1220(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5218.htm[doi:10.13328/j.cnki.jos.005218]
    [20] Tan YL, Yang H, Qiao L. Formal modeling and verification of task-management requirement for SpaceOS2 on Event-B. Aerospace Control and Application, 2014,40(4):57-62(in Chinese with English abstract).[doi:10.3969/j.issn.1674-1579.2014.04.011]
    附中文参考文献:
    [11] 马顶,付明,乔磊,冯新宇.复杂内核数据结构的形式化描述和验证.小型微型计算机系统,2019,40(2):359-366.
    [15] 王海波,郭宇,陈意云,验证带有线程的动态创建和退出的多线程程序.小型微型计算机系统,2010,31(8):1637-1642.
    [16] 马杰波,付明,冯新宇.μC/OS-II中消息队列通信机制的形式化验证.小型微型计算机系统,2016,37(6):1179-1184.
    [17] 顾海博,付明,乔磊,冯新宇.SpaceOS中若干全局性质的形式化描述和验证.小型微型计算机系统,2019,40(1):141-148.
    [19] 乔磊,杨孟飞,谭彦亮,蒲戈光,杨桦.基于Event-B的航天器内存管理系统形式化验证.软件学报,2017,28(5):1204-1220. http://www.jos.org.cn/1000-9825/5218.htm[doi:10.13328/j.cnki.jos.005218]
    [20] 谭彦亮,杨桦,乔磊.基于Event-B的SpaceOS2操作系统任务管理需求形式化建模与验证.空间控制技术与应用,2014,40(4):57-62.[doi:10.3969/j.issn.1674-1579.2014.04.011]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

姜菁菁,乔磊,杨孟飞,杨桦,刘波.基于Coq的操作系统任务管理需求层建模及验证.软件学报,2020,31(8):2375-2387

Copy
Share
Article Metrics
  • Abstract:2951
  • PDF: 6604
  • HTML: 3775
  • Cited by: 0
History
  • Received:August 31,2019
  • Revised:November 02,2019
  • Online: April 20,2020
  • Published: August 06,2020
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2034785Visitors
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