Formal co-verification of local interconnect network master node

In this paper, we describe a case-study of formal co-verification of a Local Interconnect Network (LIN) master node which is implemented as an embedded system. We use the framework described in [1] to formally co-verify the LIN master node. However, as the proof problem of verifying global behaviors of the LIN master node is complex and exceeds the capacity of a state-of-the-art formal property checker, we apply an abstract technique to reduce the size of the LIN master node implementation. In our abstraction technique, only LIN protocol-related behaviors are kept in the new, simplified LIN master node. After abstraction, we can successfully verify several global properties against the LIN master node.