loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First International Conference on Software Engineering and Formal Methods (SEFM'03)
Formal Verification of ASM Designs Using the MDG Tool
Brisbane, Australia
September 22-September 27
ISBN: 0-7695-1949-0
Amjad Gawanmeh, Concordia University
Sofiène Tahar, Concordia University
Kirsten Winter, University of Queensland
In this paper, we present a formal hardware verification framework linking ASM with MDG. ASM (Abstract State Machine) is a state based language for describing transition systems. MDG (Multiway Decision Graphs) provides symbolic representation 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 support this work with a case study of an Island Tunnel Controller, which behavior and structure were specified in ASM then using our ASM-MDG tool successfully verified within the MDG tool.
Citation:
Amjad Gawanmeh, Sofiène Tahar, Kirsten Winter, "Formal Verification of ASM Designs Using the MDG Tool," sefm, pp.210, First International Conference on Software Engineering and Formal Methods (SEFM'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.