ASM (Abstract State Machines) is a formal specification method for
software and hardware systems that has become successful for specifying
and verifying complex systems. An ASM model describes the state space of
the system by means of universes or functions, and the state transitions
by means of transition rules. ASM is used as a modeling language in a variety
of domains as it has been used both in academic and industry contexts.
The wide group of ASM users shows that there is interest in the language
and, consequently, there is an interest in tool support. ASM model transition
systems in a simple and uniform fashion and give these transition systems
an operational semantics. Many verification tools that are available are
based on transition systems. A transformation from ASM into these tools'
languages can be done without losing properties of the original model.
