ASM2Bogor: An approach for verification of models specified through Asmeta language

Nowadays, publish–subscribe (pub-sub) and event-based architectures 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 pub–sub 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 Asmeta language using Bogor—a well known model checker. In our approach, the AsmetaL specification is automatically encoded to BIR, the input language of the Bogor. Our experimental results show that in the most cases our approach generates more efficient results in comparison with the existing approach.

► ASM is a powerful language for modeling different software architectures.
► Modeling per se is not enough since developers want to be able to analyze their designed models.
► ASM2Bogor is a framework to verify ASM-based models using model checking.
► The presented approach covers most of the constructs in the AsmetaL.