Automatic Analysis and Abstraction for Model Checking HW/SW Co-Designs modeled in SystemC

摘要

Embedded systems usually consist of deeply integrated hardware and software components. As a consequence, modular verification is not easily possible. One important step towards modular verification of integrated HW/SW systems is to automatically compute abstractions of components that influence the overall system behavior but are not relevant for a given property. In this paper, we present an automatic abstraction technique for HW/SW co-designs modeled in Sys-temC. The key idea is to use a variant of classical abstract interpretation that is tailored for the specific semantics of SystemC. Our main contributions are the following: First, we present an analysis that determines data-dependencies between variables and equivalent data values with respect to conditional branches while taking the timing behavior and scheduling policies of SystemC into consideration. Second, we use the results for slicing and variable abstraction to significantly reduce the semantic state space of a given SystemC design and again produce a valid abstract design. Our abstraction technique makes it possible to automatically verify properties for comparatively large designs with the UPPAAL model checker, which cannot be handled without our approach. We demonstrate this with two case studies from the SystemC reference implementation.