Sciweavers

JSA
2008

Formal verification of ASMs using MDGs

13 years 9 months ago
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic repion of transition systems with support of abstract sorts and functions. We implemented a transformation tool that automatically generates MDG models from ASM specifications. Then formal verification techniques provided by the MDG tool, such as model checking or equivalence checking, can be applied on the generated models. We illustrate this work with the case study of an ATM switch controller, in which behavior and structure were specified in ASM and, using our ASM-MDG facility, are successfully verified with the MDG tool.
Amjad Gawanmeh, Sofiène Tahar, Kirsten Wint
Added 27 Dec 2010
Updated 27 Dec 2010
Type Journal
Year 2008
Where JSA
Authors Amjad Gawanmeh, Sofiène Tahar, Kirsten Winter
Comments (0)