Formal verification of ASM designs using the MDG tool

Gawanmeh, A., Tahar, S. and Winter, K. (2003). Formal verification of ASM designs using the MDG tool. In: A. Cerone and P. Lindsay, Proceedings of the First International Conference on Software Engineering and Formal Methods 2003. The First International Conference on Software Engineering and Formal Methods 2003, Brisbane, Australia, (210-219). 22-27 September 2003. doi:10.1109/SEFM.2003.1236223


Author Gawanmeh, A.
Tahar, S.
Winter, K.
Title of paper Formal verification of ASM designs using the MDG tool
Conference name The First International Conference on Software Engineering and Formal Methods 2003
Conference location Brisbane, Australia
Conference dates 22-27 September 2003
Proceedings title Proceedings of the First International Conference on Software Engineering and Formal Methods 2003
Journal name First International Conference On Software Engineering and Formal Methods, Proceedings
Place of Publication Los Alamitos, CA, U.S.A.
Publisher IEEE Computer Society
Publication Year 2003
Sub-type Fully published paper
DOI 10.1109/SEFM.2003.1236223
ISBN 0-7695-1949-0
ISSN 1551-0255
Editor A. Cerone
P. Lindsay
Start page 210
End page 219
Total pages 10
Collection year 2003
Language eng
Abstract/Summary 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.
Subjects E1
280000 Information, Computing and Communication Sciences
780000 - Non-Oriented Research
Keyword Data structures
Decision diagrams
Decision tables
Q-Index Code E1

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 0 times in Thomson Reuters Web of Science Article
Scopus Citation Count Cited 3 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Fri, 24 Aug 2007, 02:03:21 EST