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
相关论文
共 50 条
  • [21] Formal Specification and Verification of Mobile Agent Systems
    Kahloul, L.
    Grira, M.
    INTERNATIONAL JOURNAL OF COMPUTERS COMMUNICATIONS & CONTROL, 2014, 9 (03) : 292 - 304
  • [22] Tools for formal specification, verification, and validation of requirements
    Heitmeyer, C
    Kirby, J
    Labaw, B
    COMPASS '97 - ARE WE MAKING PROGRESS TOWARDS COMPUTER ASSURANCE?, 1997, : 35 - 47
  • [23] Formal Specification and Verification of Ubiquitous and Pervasive Systems
    Coronato, Antonio
    De Pietro, Giuseppe
    ACM TRANSACTIONS ON AUTONOMOUS AND ADAPTIVE SYSTEMS, 2011, 6 (01)
  • [24] Formal Specification and Verification of Dynamic Parametrized Architectures
    Cimatti, Alessandro
    Stojic, Ivan
    Tonetta, Stefano
    FORMAL METHODS, 2018, 10951 : 625 - 644
  • [25] FORMAL SPECIFICATION AND VERIFICATION OF ISDN SERVICES IN LOTOS
    YAMANO, K
    JOKANOVIC, D
    ANDO, T
    OHTA, M
    TAKAHASHI, K
    IEICE TRANSACTIONS ON COMMUNICATIONS, 1992, E75B (08) : 715 - 722
  • [26] Formal Specification Technique in Smart Contract Verification
    Lee, Seung-Min
    Park, Soojin
    Park, Young B.
    2019 INTERNATIONAL CONFERENCE ON PLATFORM TECHNOLOGY AND SERVICE (PLATCON), 2019, : 7 - 10
  • [27] Formal specification and verification of ARM6
    Fox, A
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2003, 2758 : 25 - 40
  • [28] VESAR - A PRAGMATIC APPROACH TO FORMAL SPECIFICATION AND VERIFICATION
    ALGAYRES, B
    COELHO, V
    DOLDI, L
    GARAVEL, H
    LEJEUNE, Y
    RODRIGUEZ, C
    COMPUTER NETWORKS AND ISDN SYSTEMS, 1993, 25 (07): : 779 - 790
  • [29] Formal Specification and Verification of Transmission Control Protocol
    Jarrar, Abdessamad
    Bellasri, Otman
    Chougdali, Sallami
    Balouki, Youssef
    ICCWCS'17: PROCEEDINGS OF THE 2ND INTERNATIONAL CONFERENCE ON COMPUTING AND WIRELESS COMMUNICATION SYSTEMS, 2017,
  • [30] Formal Specification and Automatic Verification of Conditional Commitments
    El Kholy, Warda
    El Menshawy, Mohamed
    Bentahar, Jamal
    Qu, Hongyang
    Dssouli, Rachida
    IEEE INTELLIGENT SYSTEMS, 2015, 30 (02) : 36 - 44
12345