Comparison of Path Exploration and Model Checking Techniques for Checking Automotive API Call Safety


KIPS Transactions on Software and Data Engineering, Vol. 5, No. 12, pp. 615-622, Dec. 2016
10.3745/KTSDE.2016.5.12.615,   PDF Download:
Keywords: Automotive Software, API, Constraint Pattern, Static Analysis, Model Checking
Abstract

Automotive control software can be a source of critical safety issues when developers do not comply system constraints. However, a violation is difficult to identify in complicated source code if not supported by an automated verification tool. This paper introduces two possible approaches that check whether an automotive control software complies API call constraints to compare their performance and effectiveness. One method statically analyzes the source code and explores all possible execution paths, and the other utilizes a model checker to monitor constraint violations for a given set of constraint automata. We have implemented both approaches and performed a series of experiments showing that the approach with model-checking finds constraint violations more accurately and scales better.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from September 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
D. Kim and Y. Choi, "Comparison of Path Exploration and Model Checking Techniques for Checking Automotive API Call Safety," KIPS Transactions on Software and Data Engineering, vol. 5, no. 12, pp. 615-622, 2016. DOI: 10.3745/KTSDE.2016.5.12.615.

[ACM Style]
Dongwoo Kim and Yunja Choi. 2016. Comparison of Path Exploration and Model Checking Techniques for Checking Automotive API Call Safety. KIPS Transactions on Software and Data Engineering, 5, 12, (2016), 615-622. DOI: 10.3745/KTSDE.2016.5.12.615.