@inproceedings{80f0b13cbe204c85bf146ca24c8ffd30,
title = "Modeling OSEK/VDX OS Requirements in C",
abstract = "This paper presents an approach to use C language to model underlying operating systems widely used in the domain of automotive control software. The greatest benefit of using C, a programming language, which is used widely in this domain, is the elimination of the heterogeneity between OS model and control software. This enables us to formally verify control software while keeping its own characteristics such as function calls, the use of external libraries, and dynamic memory allocation. We took a two-step approach to maintain the level of abstraction; we first define formal CSP models of OS components based on the OSEK/VDX international standard and then define an OS model in C by using the CSP models as references. We derived 20 functional API assertions, 6 invariant properties, 4 temporal properties and 4 code-safety properties from the OSEK/VDX international standard, and validated the model with the C code model checker CBMC. We used our OS C model to verify applications for Erika OS and could find out severe property violations.",
keywords = "CBMC, Formal Modeling, OSEK/VDX OS, Verification & Validation",
author = "Yoohee Chung and Dongwoo Kim and Yunja Choi",
note = "Publisher Copyright: {\textcopyright} 2017 IEEE.; 24th Asia-Pacific Software Engineering Conference, APSEC 2017 ; Conference date: 04-12-2017 Through 08-12-2017",
year = "2017",
month = jul,
day = "2",
doi = "10.1109/APSEC.2017.46",
language = "English",
series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",
publisher = "IEEE Computer Society",
pages = "398--407",
editor = "Jian Lv and He Zhang and Mike Hinchey and Xiao Liu",
booktitle = "Proceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017",
address = "United States",
}