分离内核形式化规约与验证综述
软件工程
2016-07-12 v3
摘要
分离内核是安全与安保关键系统的基础软件，它为其承载的应用程序提供空间和时间上的分离，以及分区之间受控的信息流。分离内核在关键领域的应用要求通过形式化验证来保证内核的正确性。据我们所知，目前没有关于该主题的综述论文。本文概述了分离内核的形式化规约与验证。我们首先介绍背景，包括分离内核的概念以及不同内核之间的比较。然后，我们调研了自 2000 年以来该主题的研究现状。最后，我们通过详细的比较与讨论对研究工作进行了总结。
引用
@article{arxiv.1508.07066,
title = {A survey on formal specification and verification of separation kernels},
author = {Yongwang Zhao},
journal= {arXiv preprint arXiv:1508.07066},
year = {2016}
}