  Nowadays, publish subscribe and event based architecture are frequently used
for developing loosely coupled distributed systems. Hence, it is desirable to
find a proper solution to specify different systems through these
architectures. Abstract state machine (ASM) is a useful means to visually and
formally model publish subscribe and event based architectures. However,
modeling per se is not enough since the designers want to be able to verify the
designed models. As the model checking is a proper approach to verify software
and hardware systems. In this paper, we present an approach to verify ASM
models specified in terms of AsmetaL language using Bogor. In our approach, the
AsmetaL specification is automatically encoded to BIR, the input language of
the Bogor.
