Case Studies of Model Checking for Embedded System Designs

As modern embedded systems become more integrated and complex, it is crucial to be able to represent systems ple levels of abstraction, so that the design space can be effectively explored by successive refinements and ions. In this paper, we present a formal verification methodology and case studies for property verification of 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.

• Type: Conference
• Year: 2003
• Where: ACSD
• Authors: Xi Chen, Harry Hsieh, Felice Balarin, Yosinori Watanabe
• Keywords: ACSD 2003, Formal Verification Methodology, Hardware, Modern Embedded Systems, Systems Ple Levels