Light-Weight API-Call Safety Checking for Automotive Control Software Using Constraint Patterns
Dongwoo Kim, Yunja Choi · 2016
We present a background constraint checker that helps to detect constraint violations regarding API call sequences in automotive software development. Our tool traces API call sequences in a program and warns programmers if they violate pre-defined constraint patterns identified from international standard for automotive operating systems. The background constraint checker implements constraint patterns as C library functions and uses the model checker CBMC as its underlying checking engine. The tool is developed in JAVA and is validated through a series of experiments.