Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6875173 | Science of Computer Programming | 2018 | 23 Pages |
Abstract
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.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Dongwoo Kim, Yunja Choi,