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.
Description
An Efficient Solution for Model Checking Abstract State Machine Using
Bogor
%0 Generic
%1 doostali2014efficient
%A Doostali, Saeed
%D 2014
%K myown
%R 10.1016/j.jvlc.2012.05.002
%T An Efficient Solution for Model Checking Abstract State Machine Using
Bogor
%U http://arxiv.org/abs/1404.2155
%X 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.
@misc{doostali2014efficient,
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.},
added-at = {2014-04-28T10:31:58.000+0200},
author = {Doostali, Saeed},
biburl = {https://www.bibsonomy.org/bibtex/29e9f1759f8842daccaf7f492ec14c1ec/doostali},
description = {An Efficient Solution for Model Checking Abstract State Machine Using
Bogor},
doi = {10.1016/j.jvlc.2012.05.002},
interhash = {ff9b555faf74aef958e0c6a032b3de19},
intrahash = {9e9f1759f8842daccaf7f492ec14c1ec},
keywords = {myown},
note = {cite arxiv:1404.2155Comment: 57 pages, 25 figures, 4 tables, Technical Report},
timestamp = {2014-04-28T10:31:58.000+0200},
title = {An Efficient Solution for Model Checking Abstract State Machine Using
Bogor},
url = {http://arxiv.org/abs/1404.2155},
year = 2014
}