Interfacing ASM with the MDG tool

Gawanmeh, Amjad, Tahar, Sofiène and Winter, Kirsten (2003). Interfacing ASM with the MDG tool. In: E. Borger, A. Gargantini and E. Riccobene, Lecture Notes in Computer Science: Abstract State Machines 2003. Abstract State Machines 2003 Advances in Theory and Practice 10th International Workshop, ASM 2003, Taormina, Italy, (278-292). 3-7 March, 2003. doi:10.1007/3-540-36498-6

Author Gawanmeh, Amjad
Tahar, Sofiène
Winter, Kirsten
Title of paper Interfacing ASM with the MDG tool
Conference name Abstract State Machines 2003 Advances in Theory and Practice 10th International Workshop, ASM 2003
Conference location Taormina, Italy
Conference dates 3-7 March, 2003
Proceedings title Lecture Notes in Computer Science: Abstract State Machines 2003   Check publisher's open access policy
Journal name Abstract State Machines 2003: Advances in Theory and Practic, Proceedings   Check publisher's open access policy
Place of Publication Berlin
Publisher Springer-Verlag
Publication Year 2003
Sub-type Fully published paper
DOI 10.1007/3-540-36498-6
Open Access Status
ISBN 3540-00624-9
ISSN 0302-9743
Editor E. Borger
A. Gargantini
E. Riccobene
Volume 2589
Start page 278
End page 292
Total pages 15
Collection year 2003
Language eng
Abstract/Summary In this paper we describe an approach to interface Abstract State Machines (ASM) with Multiway Decision Graphs (MDG) to enable tool support for the formal verification of ASM descriptions. ASM is a specification method for software and hardware providing a powerful means of modeling various kinds of systems. MDGs are decision diagrams based on abstract representation of data and axe used primarily for modeling hardware systems. The notions of ASM and MDG axe hence closely related to each other, making it appealing to link these two concepts. The proposed interface between ASM and MDG uses two steps: first, the ASM model is transformed into a flat, simple transition system as an intermediate model. Second, this intermediate model is transformed into the syntax of the input language of the MDG tool, MDG-HDL. We have successfully applied this transformation scheme on a case study, the Island Tunnel Controller, where we automatically generated the corresponding MDG-HDL models from ASM specifications.
Subjects E1
280000 Information, Computing and Communication Sciences
780000 - Non-Oriented Research
08 Information and Computing Sciences
Keyword Computer Science, Theory & Methods
Multiway Decision Graphs
Formal Verification
Model Checking
Q-Index Code E1

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