High-assurance timing analysis for a high-assurance real-time operating system
High-assurance timing analysis for a high-assurance real-time operating system
复制标题
高保证实时操作系统的高保证时序分析
DOI：
10.1007/s11241-017-9286-3
复制
发表时间：
2017
影响因子：
1.3
通讯作者：
Gernot Heiser
中科院分区：
文献类型：
--
作者：
Thomas Sewell;Felix Kam;Gernot Heiser
为了保证实时代码的可靠性，需要对可执行二进制代码进行最坏情况执行时间（WCET）分析。获得紧密的WCET边界需要确定环路边界和消除不可行路径。然而，二进制代码缺乏确定这些边界所需的信息。这些信息通常是通过人工干预提供的，或者由专门修改过的编译器保存在二进制文件中。我们提出了一种替代方法，使用现有的翻译验证框架，以实现高保证，自动确定循环边界和不可行的路径。我们展示了这种方法自动确定seL4微内核中的所有循环边界和许多（可能是全部）不可行的路径，以及在我们的C解析器的语言子集中的标准WCET基准测试。我们还设计并验证了对seL4实现的改进，它允许在混合临界设置中向用户提供内核API的关键部分。
Worst-case execution time (WCET) analysis of real-time code needs to be performed on the executable binary code for soundness. Obtaining tight WCET bounds requires determination of loop bounds and elimination of infeasible paths. The binary code, however, lacks information necessary to determine these bounds. This information is usually provided through manual intervention, or preserved in the binary by a specially modified compiler. We propose an alternative approach, using an existing translation-validation framework, to enable high-assurance, automatic determination of loop bounds and infeasible paths. We show that this approach automatically determines all loop bounds and many (possibly all) infeasible paths in the seL4 microkernel, as well as in standard WCET benchmarks which are in the language subset of our C parser. We also design and validate an improvement to the seL4 implementation, which permits a key part of the kernel’s API to be available to users in a mixed-criticality setting.
DOI：
10.1145/2737924.2738006
发表时间：
2015-06
期刊：
Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Peter Gammie;Antony Hosking;Kai Engelhardt
通讯作者：
Peter Gammie;Antony Hosking;Kai Engelhardt
影响因子：
22.7
作者：
Gu, Ronghui;Shao, Zhong;Costanzo, David
通讯作者：
Costanzo, David