@inproceedings{e80d06c999cd4001b2c8862310272cfc,
title = "Model-based API-call constraint checking for automotive control software",
abstract = "Operating systems for embedded software publish a set of API functions together with a set of API-call constraints that have to be followed by application software running on the OS. If the embedded software is controlling safety-critical systems, a violation of those constraints may be a source of massive property damage or human injury. As a light-weight support for pre-checking such constraints during the development of embedded software, this work presents an API-call constraint checker for automotive control software. The checker converts application source code into formal models and checks violations of a set of pre-defined constraint patterns from OSEK/VDX international standard using model checker NuSMV. It is capable of checking local constraints within a task as well as global constraints involving task scheduling without suffering from false/missed alarms, by using formal models of the underlying operating system. We demonstrate the efficiency and effectiveness of the checker through comparative experiments with our previous checker which did not use the formal OS model.",
keywords = "API, API-call constraint, Automotive Software, Constraint Pattern, Global Constraint, Model checking, OSEK/VDX",
author = "Dongwoo Kim and Yoohee Chung and Yunja Choi",
note = "Publisher Copyright: {\textcopyright} 2016 IEEE.; 23rd Asia-Pacific Software Engineering Conference, APSEC 2016 ; Conference date: 06-12-2016 Through 09-12-2016",
year = "2016",
month = jul,
day = "2",
doi = "10.1109/APSEC.2016.039",
language = "English",
series = "Proceedings - Asia-Pacific Software Engineering Conference, APSEC",
publisher = "IEEE Computer Society",
pages = "217--224",
editor = "Alex Potanin and Murphy, \{Gail C.\} and Steve Reeves and Jens Dietrich",
booktitle = "Proceedings - 23rd Asia-Pacific Software Engineering Conference, APSEC 2016",
address = "United States",
}