Abstract
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 are used primarily for modeling hardware systems. The notions of ASM and MDG are 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Balakrishnan A Hierarchical Approach to the Formal Verification of Embedded Systems Using MDGs. Master’s Thesis, Concordia University, Department of Electrical and Computer Engineering, November 1999. 283
D. Beauquier and A. Slissenko. The Railroad Crossing Problem: Towards Semantics of Timed Algorithms and their Model-Checking in High-Level Languages. In M. Bidoit and M. Dauchet (eds.), Proceedings of TAPSOFT’97, LNCS 1214, Springer-Verlag, 1997. 279
E. Cerny, F. Corella, M. Langevin, X. Song, S. Tahar, Z. Zhou. Automated Verification with Abstract State Machines Using Multiway Decision Graphs. In T. Kropf (ed.), Formal Hardware Verification: Methods and Systems in Comparison, LNCS 1287, State-of-the-Art Survey, Springer-Verlag, 1997, pp. 79–113. 278, 282, 283
F. Corella, Z. Zhou, X. Song, M. Langevin and E. Cerny. Multiway Decision Graphs for Automated Hardware Verification. Formal Methods in System Design, Vol. 10, February 1997, pp. 7–46. 280, 282
G. Del Castillo. The ASM Workbench: A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models. Ph.D. Thesis, Heinz Nixdorf Institute, Paderborn, Germany, 2000. 279, 280
G. Del Castillo and K. Winter. Model Checking Support for the ASM High-level Specification Language. In S. Graf and M. Schwartzbach (eds.), Tools and Algorithms for the Construction and Analysis of Systems. LNCS 1785, Springer-Verlag, pp. 331–346, 2000. 279, 280
Y. Feng, E. Cerny. Term Ordering Problem on MDG. In Proc. ACM 12th Great Lakes Symposium on VLSI, New York City, New York, USA, April 2002, pp. 160–165. 283
J. K. Huggins. Abstract State Machines home page. EECS Department, University of Michigan. http://www.eecs.umich.edu/gasm/. 278, 279
S. Katz and O. Grumberg. A Framework for Translating Models and Specification. In K. Sere and M. Butler (eds.), Integrated Formal Methods. LNCS 2335, Springer-Verlag, 2002. 279
S. Kort, S. Tahar, and P. Curzon. Hierarchical Verification Using an MDG-HOL Hybrid Tool. In: T. Margaria and T. Melham (eds.), Correct Hardware Design and Verification Methods, LNCS 2144, Springer Verlag, 2001, pp. 244–258. 279
T. Kropf. Introduction to Formal Hardware Verification, Springer-Verlag, 1999. 278, 280
Y. Mokhtari, M. Shirazipour, and S. Tahar. A Case Study on Model Checking and Refinement of Abstract State Machines. Proc. Eight International Conference on Computer Aided Systems Theory, Las Palmas de Gran Canaria, Canary Islands, Spain, February 2001, pp. 239–242.
C. Plonka. Model checking for the design with abstract state machines. Master’s thesis, University of Ulm, Department of Applied Information Processing, 2000. 279
M. Spielmann. Automatic verification of abstract state machines. In N. Halbwachs and D. Peled (eds.), Computer Aided Verification, LNCS 1633, pages 431–442. Springer-Verlag, 1999. 279
N. Shankar. Symbolic Analysis of Transition Systems. In Y. Gurevich, P. Kutter, M. Odersky, and L. Thiele (eds.), Abstract State Machines, Theory and Applica-tions, ASM 2000, LNCS 1912, pp. 287–302, Springer-Verlag, 2000. 279
S. Tahar, X. Song, E. Cerny, Z. Zhou, M. Langevin and O. Ait-Mohamed. Modeling and Verification of the Fairisle ATM Switch Fabric using MDGs. IEEE Transactions on CAD of Integrated Circuits and Systems, Vol. 18 No. 7, July 1999, pp. 956–972. 283
K. Winter. Model Checking Abstract State Machines, Ph.D. thesis, Technical University of Berlin 2001. 279, 280, 283
Y. Xu, E. Cerny, X. Song, F. Corella, O. Mohamed. Model Checking for First-Order Temporal Logic using Multiway Decision Graphs. In Computer Aided Verification, LNCS 1427, Springer Verlag, 1998, pp. 219–231. 282
Z. Zhou, X. Song, S. Tahar, E. Cerny, F. Corella, M. Langevin. Formal Verification of the Island Tunnel Controller using Multiway Decision Graphs. In Formal Methods in Computer-Aided Design, LNCS 1166, Springer Verlag, 1996, pp. 233–246. 283, 287
Z. Zhou and N. Boulerice. MDG Tools (v1.0) User’s Manual. Dept. of Information and Operation Research, University of Montreal, Canada, 1996. 279, 282
M. H. Zobair. Modeling and Formal Verification of a Telecom System Block using MDGs. M. A.Sc. Thesis, Concordia University, Department of Electrical and Computer Engineering, Montreal, Canada, April 2001. 283
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gawanmeh, A., Tahar, S., Winter, K. (2003). Interfacing ASM with the MDG Tool. In: Börger, E., Gargantini, A., Riccobene, E. (eds) Abstract State Machines 2003. ASM 2003. Lecture Notes in Computer Science, vol 2589. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36498-6_16
Download citation
DOI: https://doi.org/10.1007/3-540-36498-6_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00624-4
Online ISBN: 978-3-540-36498-6
eBook Packages: Springer Book Archive