Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition systems with support of abstract sorts and functions. We implemented a transformation tool that automatically generates MDG models from ASM specifications. Then formal verification techniques provided by the MDG tool, such as model checking or equivalence checking, can be applied on the generated models. We illustrate this work with the case study of an ATM switch controller, in which behavior and structure were specified in ASM and, using our ASM-MDG facility, are successfully verified with the MDG tool.