Interfacing ASM with the MDG tool
Amjad Gawanmeh, Sofiène Tahar, Kirsten Winter · 2003
In this paper we describe an approach to interface Abstract State Machines (ASM) with Multiway Decision Graphs (MDG) to enable tool support for the formal veri cation of ASM descriptions. ASM is a speci cation method for software and hardware providing a powerful means of modeling various kinds of systems. MDGs are decision diagrams based on abstract representation of data and are used primarily for modeling hardware systems. The notions of ASM and MDG are hence closely related to each other, making it appealing to link these two concepts. The proposed interface between ASM and MDG uses two steps: rst, the ASM model is transformed into a at, simple transition system as an intermediate model. Second, this intermediate model is transformed into the syntax of the input language of the MDG tool, MDG-HDL. We have successfully applied this transformation scheme on a case study, the Island Tunnel Controller, where we automatically generated the corresponding MDG-HDL models from ASM speci cations.