A two-step approach for pattern-based API-call constraint checking

As automated tool support for pre-checking constraint violations in the development process, this study presents a two-step approach for checking API-call constraints by using predefined patterns specifically designed for automotive operating systems. A lightweight checking method is designed for quick-and-easy checking of local API-call constraints, which utilizes constraint patterns and the C code model checker CBMC. The global constraint checking method is a heavyweight method, as it requires behavior models of the underlying operating system constructs as well as constraint patterns, but it produces more accurate verification results; it uses the symbolic model checker NuSMV as the backend verification engine. This two-step approach is effective in identifying constraint violations and efficient in reducing false alarms from infeasible execution paths.