Name
Abstract | ||
|---|---|---|
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
<inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$\mathbb {K}$</tex-math></inline-formula>
. The formal kernel is
<italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">unified</italic>
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. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1109/tr.2018.2863744 | IEEE Transactions on Reliability |
Keywords | Field | DocType |
Standards,Kernel,Automobiles,Task analysis,Computer bugs,Testing | Operational semantics,Software engineering,Software bug,OSEK,Deadlock,Correctness,Test case,Workflow,Reliability engineering,Mathematics,Executable | Journal |
Volume | Issue | ISSN |
68 | 3 | 0018-9529 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Xiaoran Zhu | 1 | 17 | 3.22 |
| Min Zhang | 2 | 7 | 4.23 |
| Jian Guo | 3 | 2 | 2.06 |
| Xin Li | 4 | 1 | 1.71 |
| Huibiao Zhu | 5 | 583 | 86.68 |
| Jifeng He | 6 | 1 | 1.70 |