Translation-based co-verification

We propose a translation-based approach to hardware and software co-verification of embedded systems using model checking. Software and hardware designs of an embedded system are translated into the input formal language of a state-of-the-art model checker to enable co-verification. The formal model of the whole system is constructed through integrating the translations of hardware and software designs via a bridge module. The bridge module preserves the semantics of hardware and software. Co-verification complexity is reduced through (1) leveraging reduction algorithms of the target model checkers, (2) applying reduction algorithms in translation via model transformations, and (3) conducting compositional reasoning across the interfaces of the bridge module. Our approach has been implemented to support co-verification of software designs specified in executable UML and hardware designs specified in Verilog. We have successfully applied this approach to co-verification of networked sensors, an emerging type of embedded systems. The case study has shown that our approach is practical - applicable to embedded systems of real-world scale, and effective - leading to order-of-magnitude reduction on co-verification complexities.