Formal Verification for Embedded System Designs

Embedded electronics today are becoming increasingly complex, which makes their design and analysis more and more difficult. 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 the Metropolis framework and the model checker SPIN, a translation mechanism from a Metropolis design to a 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 for both system level representations and refined representations, where the representations may contain system functions or abstract architectures.