Formal verification of embedded system designs at multiple levels of abstraction

Embedded electronics today are becoming increasingly complex, which makes their design and analysis more and more difficult. An important approach to overcome the increasing complexity is to divide the system design procedure into different but interrelated stages, and represent system designs with description at different levels of abstraction. Design and analysis tools at each stages can then be more effectively applied onto the designs at particular level of abstraction. In this paper, we focus on the formal verification of embedded system designs at multiple levels of abstraction, enabled by the Metropolis design environment. Based on Metropolis framework and the model checker SPIN, a translation mechanism from Metropolis design to Promela description is presented and an automatic translator is developed accordingly. We discuss the challenges and solutions in semantically translating from an object-based system design language to a procedural verification language. To demonstrate the correctness and effectiveness of our approach for formal verification, we verify properties of typical producer-consumer systems.