Paper Info
Title
A Compact Encoding of Sequential ASMs in Event-B.
Abstract
We present a translation of sequential ASMs to Event-B specifications. The translation also addresses the partial update problem, and allows a variable to be updated (consistently) in parallel. On the theoretical side, the translation highlights the intricacies of ASM rule execution in terms of Event-B semantics. On the practical side, we show on a series of examples that the Event-B encoding remains compact and is amenable to proof within Rodin as well as animation and model checking using ProB.
Year
DOI
Venue
2016
10.1007/978-3-319-33600-8_7
ABZ
Keywords
DocType
Volume
ASM,B-method,Model checking,Constraint-solving,Tools
Conference
9675
ISSN
Citations 
PageRank 
0302-9743
4
0.48
References 
Authors
10
2
Name
Order
Citations
PageRank
Michael Leuschel12156135.89
Egon Börger21596202.86