An Efficient Solution for Model Checking Abstract State Machine Using Bogor

TL;DR

This paper presents an efficient method for verifying Abstract State Machine models specified in AsmetaL by automatically encoding them into Bogor's input language, facilitating formal verification of distributed system architectures.

Contribution

It introduces an automated encoding process from AsmetaL to BIR, enabling effective model checking of ASM models with Bogor.

Findings

Automated encoding from AsmetaL to BIR is feasible.

Verification of ASM models using Bogor is improved.

The approach supports modeling publish subscribe architectures.

Abstract

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.