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

An operating system publishes a set of application programming interface (API) functions along with a set of API-call constraints with which programs running on the operating system must comply. Any violation of these constraints may become a source of massive property damage or even human injury when such a program is used for safety-critical systems. A rigorous and targeted verification method is needed to identify such violations, which are frequently subtle and difficult to identify using conventional verification methods. 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.