ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System
ORIENTAIS: Formal Verified OSEK/VDX Real-Time Operating System
复制标题
DOI：
10.1109/iceccs.2012.27
复制
发表时间：
2012-07
期刊：
影响因子：
--
通讯作者：
Jianqi Shi;J. He;Huibiao Zhu;Huixing Fang;Yanhong Huang;Xiaoxian Zhang
中科院分区：
文献类型：
--
作者：
Jianqi Shi;J. He;Huibiao Zhu;Huixing Fang;Yanhong Huang;Xiaoxian Zhang
在本文中，我们报告了正式的机器验证的操作系统 - Orientais。 Orientais是用于汽车应用程序的OSEK/VDX标准操作系统。 Orientais中包含约8000行C和60行组件。该操作系统对于嵌入式系统至关重要，尤其是在某些时间敏感和准确的控制应用程序中，就像汽车应用一样。我们证明，Orientais应用程序编程界面的实现严格遵循OSEK/VDX规范，我们从自然语言表达的OSEK/VDX规范中形式化。同时，我们用CSP对高级相互作用行为进行建模，并像无僵局一样验证属性。为了确保涉及中断程序的内存访问和有限响应时间的安全性，二进制代码级验证是基于xbil开发的，这是我们提出的一种二进制中间语言。我们介绍了一系列验证东方的技术和方法。我们的方法是对Orientais进行验证的有效工作，并在其帮助下检测到了几个错误。现在，Orientais已获得Osek认证小组的认证，并在中国安装了超过138万辆汽车。
In this paper, we report on the formal, machine-verified operating system - ORIENTAIS. ORIENTAIS is an OSEK/VDX standard based real-time operating system for automotive applications. About 8000 lines of C and 60 lines of assembler are comprised in the ORIENTAIS. The operating system is of vital importance to embedded systems, especially for some time sensitive and accurate controlling applications just like automotive applications. We prove that the implementation of ORIENTAIS application programming interfaces strictly follow the OSEK/VDX specification which we formalized from natural language expressed OSEK/VDX specification. Meanwhile, we model the high level interaction behaviors with CSP and verify the properties just like deadlock-free. To guarantee the safety of memory access and bounded response time with interrupt program involved, binary code level verification is developed based on xBIL which is a binary intermediate language we proposed. We introduce a series of techniques and approaches for verifying the ORIENTAIS. Our approach is an efficient work for the verification of ORIENTAIS, with whose help several bugs are detected. Now, ORIENTAIS has been certificated by OSEK certification group and installed on more than 1.38 million cars in China.