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: tahar@ece.concordia.ca