Technical Report

Model Checking and Refinement of ASM Models Using SMV

M. Shirazipour, Y. Mokhtari, and S. Tahar


Gurevich's Abstract State Machines (ASMs) are computational models of systems specified in a high level language (ASM-SL). In this paper, we investigate the pros and cons of the automatic verification of ASM models using the ASM-Workbench and its extension ASM-SMV, which supports computer aided verification by model checking. The results obtained are based on the validation and verification of a design block of a communication chip. We conclude this work by some suggestions on the automated process of verifying ASM models.

Download postscript file (PS File
Send comments and suggestions to: