As modern embedded systems become more integrated and complex, it is crucial to be able to represent systems at multiple levels of abstraction, so that the design space can be effectively explored by successive re.nements and abstractions. In this paper, we present a formal verification methodology and case studies for property verification of designs represented at different abstraction levels. Utilizing Metropolis meta-model (MMM), Y-chart Application Programmer?s Interface (YAPI), an automatic translator, and the model checker SPIN, we verify properties for both system level representations and refined representations.