Toward a Unified Executable Formal Automobile OS Kernel and Its Applications
Toward a Unified Executable Formal Automobile OS Kernel and Its Applications
复制标题
统一可执行的正式汽车操作系统内核及其应用
DOI：
10.1109/tr.2018.2863744
复制
发表时间：
2019-09
影响因子：
5.9
通讯作者：
He Jifeng
中科院分区：
文献类型：
--
作者：
Zhu Xiaoran;Zhang Min;Guo Jian;Li Xin;Zhu Huibiao;He Jifeng
在汽车工业中，在一定的标准下开发汽车实时操作系统是一种常用的方法。例如，OSEK/VDX是一个全球采用的开放标准。传统的工作流程是首先理解标准，设计和开发一个系统，然后测试它是否符合标准，最后部署。传统的工作流程存在几个问题，例如，标准中的模糊性可能导致实际系统的不正确设计和实现;实际系统与标准的一致性难以检查;并且实现后的错误修复成本高昂。为了弥补这种情况，本文提出了一个统一的可执行的形式化汽车内核在OSEK/VDX标准下定义的系统服务的操作语义的标准使用重写的可执行语义框架称为$\mathbb {K}$。形式化内核是统一的，它有多种用途：1）OSEK/VDX标准的形式化建模有助于检测标准中的歧义; 2）可执行内核本质上是标准的形式化模型，可用于验证汽车应用程序的正确性;以及3）经验证的应用程序可以用作测试用例，以检查真实世界的汽车操作系统与OSEK/VDX标准的一致性。使用正式的内核，我们确定在OSEK/VDX标准和一个潜在的死锁漏洞在工业汽车应用程序中的几个歧义。
In automobile industry, it is a common approach to develop automobile real-time operating systems under some standards. For instance, OSEK/VDX is a world-wide adopted open standard. Traditional workflow is to first understand the standard, design and develop a system, then test its conformance to the standard, and finally deploy. There are several issues with the traditional workflow, e.g., ambiguities in standards may lead to incorrect design and implementation of real-world systems; the conformance of real-world systems to standards is difficult to check; and bug fixing after implementation is costly. To remedy the situation, in this paper, we present a unified executable formal automobile kernel under OSEK/VDX standard by defining the operational semantics of the system services in the standard using a rewrite-based executable semantic framework called $\mathbb {K}$. The formal kernel is unified in that it serves multiple purposes such as: 1) formal modeling of the OSEK/VDX standard helps detect ambiguities in the standard; 2) the executable kernel is essentially a formal model of the standard, which can be used to verify the correctness of automobile applications; and 3) verified applications can be used as test cases to check the conformance of a real-world automobile operating system against the OSEK/VDX standard. Using the formal kernel, we identify several ambiguities in the OSEK/VDX standard and a potential deadlock vulnerability in an industrial automobile application.
登录
查看更多内容
DOI：
10.1007/978-3-319-19249-9_4
发表时间：
2015-06
期刊：
--
影响因子：
--
作者：
Musab A. Alturki;Omar Alzuhaibi
通讯作者：
Musab A. Alturki;Omar Alzuhaibi
DOI：
--
发表时间：
2017-08
期刊：
--
影响因子：
--
作者：
Everett Hildenbrandt;M. Saxena;Xiaoran Zhu;Nishant Rodrigues;Philip Daian;Dwight Guth;Grigore Roşu
通讯作者：
Everett Hildenbrandt;M. Saxena;Xiaoran Zhu;Nishant Rodrigues;Philip Daian;Dwight Guth;Grigore Roşu
影响因子：
7.4
作者：
Yunja Choi
通讯作者：
Yunja Choi
DOI：
10.1007/978-3-642-32943-2_15
发表时间：
2012-09
期刊：
--
影响因子：
--
作者：
K. Yatake;Toshiaki Aoki
通讯作者：
K. Yatake;Toshiaki Aoki
DOI：
10.1109/icst.2012.105
发表时间：
2012-04
期刊：
2012 IEEE Fifth International Conference on Software Testing, Verification and Validation
影响因子：
--
作者：
Ling Fang;Takashi Kitamura;Thi Bich Ngoc Do;H. Ohsaki
通讯作者：
Ling Fang;Takashi Kitamura;Thi Bich Ngoc Do;H. Ohsaki