A survey on formal specification and verification of separation kernels

被引：8
作者：
Zhao, Yongwang [1 ]
Yang, Zhibin [1 ,2 ,3 ]
Ma, Dianfu [1 ]
机构：
[1] Beihang Univ, Sch Comp Sci & Engn, State Key Lab Software Dev Environm NLSDE, Beijing 100191, Peoples R China
[2] Nanjing Univ Aeronaut & Astronaut, Coll Comp Sci & Technol, Nanjing 210016, Jiangsu, Peoples R China
[3] Collaborat Innovat Ctr Novel Software Technol & I, Nanjing 210016, Jiangsu, Peoples R China
来源：
FRONTIERS OF COMPUTER SCIENCE | 2017年 / 11卷 / 04期
基金：
中国国家自然科学基金;
关键词：
real-time operating systems; separation kernel; survey; formal specification; formal verification; SECURITY; SOFTWARE; DECOMPOSITION;
D O I：
10.1007/s11704-016-4226-2
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Separation kernels are fundamental software of safety and security-critical systems, which provide their hosted applications with spatial and temporal separation as well as controlled information flows among partitions. The application of separation kernels in critical domain demands the correctness of the kernel by formal verification. To the best of our knowledge, there is no survey paper on this topic. This paper presents an overview of formal specification and verification of separation kernels. We first present the background including the concept of separation kernel and the comparisons among different kernels. Then, we survey the state of the art on this topic since 2000. Finally, we summarize research work by detailed comparison and discussion.
引用
收藏
页码：585 / 607
页数：23
相关论文
共 97 条
  • [11] [Anonymous], 2014, Lecture Notes in Computer Science
  • [12] [Anonymous], 2013, TECHNICAL REPORT
  • [13] [Anonymous], 2009, P 11 REAL TIM LIN WO
  • [14] [Anonymous], 1981, ACM OPERATING SYSTEM, DOI DOI 10.1145/1067627.806586
  • [15] [Anonymous], CROSSTALK J DEFENCE
  • [16] ARINC, 2003, 653 ARINC
  • [17] Modelling, Verification and Synthesis of Two-Tier Hierarchical Fixed-Priority Preemptive Scheduling
    Asberg, Mikael
    Pettersson, Paul
    Nolte, Thomas
    [J]. PROCEEDINGS OF THE 23RD EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS (ECRTS 2011), 2011, : 172 - 181
  • [18] Barthe Gilles, 2011, FM 2011: Formal Methods. Proceedings 17th International Symposium on Formal Methods, P231, DOI 10.1007/978-3-642-21437-0_19
  • [19] Baumann C, 2010, P EMB WORLD C
  • [20] Baumann C, 2009, P EMB WORLD C
12345678910