Login | Register

Formal verification of ASMs using MDGs

Title:

Formal verification of ASMs using MDGs

Gawanmeh, A., Tahar, Sofiène and Winter, K. (2008) Formal verification of ASMs using MDGs. Journal of Systems Architecture, 54 (1-2). pp. 15-34. ISSN 13837621

[thumbnail of JSA-2008.pdf]
Preview
Text (application/pdf)
JSA-2008.pdf - Accepted Version
267kB

Official URL: http://dx.doi.org/10.1016/j.sysarc.2007.03.007

Abstract

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 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 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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Gawanmeh, A. and Tahar, Sofiène and Winter, K.
Journal or Publication:Journal of Systems Architecture
Date:2008
Digital Object Identifier (DOI):10.1016/j.sysarc.2007.03.007
Keywords:Formal verification; Abstract state machines; Multiway decision graphs; Model checking
ID Code:977371
Deposited By: Danielle Dennie
Deposited On:14 Jun 2013 14:41
Last Modified:18 Jan 2018 17:44

References:

[1]
Accellera Organization, Accellera Property Specification Language Reference Manual, version 1.1, 2007. Available from: www.accellera.org.

[2]
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.

[3]
D. Beauquier, A. Slissenko
The railroad crossing problem: towards semantics of timed algorithms and their model-checking in high-level languages
Theory and Practice of Software Development, LNCS, vol. 1214, Springer, Berlin (1997), pp. 202–212

[4]
E. Börger, R. Stark
Abstract State Machines: A Method for High-Level System Design and Analysis Springer, Berlin (2003)

[5]
E. Börger, J. Huggins, Abstract state machines 1988–1998: commented ASM bibliography, in: Formal Specification Column, EATCS Bulletin 64, February, 1998, pp. 105–127.

[6]
R.E. Bryant
Graph-based algorithms for Boolean function manipulation
IEEE Transactions on Computers, C-35 (8) (1986), pp. 677–691

[7]
E. Cerny, F. Corella, M. Langevin, X. Song, S. Tahar, Z. Zhou Automated verification with abstract state machines using multiway decision graphs Formal Hardware Verification: Methods and Systems in Comparison, LNCS, vol. 1287, State-of-the-Art Survey, Springer, Berlin (1997), pp. 79–113

[8]
F. Corella, Z. Zhou, X. Song, M. Langevin, E. Cerny
Multiway decision graphs for automated hardware verification
Formal Methods in System Design, 10 (1997), pp. 7–46

[9]
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.

[10]
K. Fisler, S. Johnson Integrating design and verification environments through a logicsupporting hardware diagrams
Proc. IFIP Conference on Hardware Description Languages, IEEE Computer Society Press (1995), pp. 669–674

[11]
A. Gargantini, E. Riccobene, Encoding abstract state machines in PVS, Abstract state machines, TIK-Report 87, Swiss Federal Institute of Technology (ETH) Zurich, March, 2000, pp. 152–173.

[12]
A. Gawanmeh, S. Tahar, K. Winter Interfacing ASMs with the MDG tool Abstract State Machines – Advances in Theory and Applications, LNCS, vol. 2589, Springer, Berlin (2003), pp. 278–292

[13]
A. Gawanmeh, S. Tahar, K. Winter Formal verification of ASM designs using the MDG tool IEEE International Conference on Software Engineering and Formal MethodsIEEE Computer Society Press (2003), pp. 210–219

[14]
M. Gordon, T. Melham Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic Cambridge University Press, Cambridge, UK (1993)

[15]
Y. Gurevich Evolving Algebras 1993: Lipari Guide. In Specification and Validation Methods Oxford University Press (1995)

[16]
J.K. Huggins, Abstract state machines home page, EECS Department, University of Michigan. Available from: http://www.eecs.umich.edu/gasm/.

[17]
S. Katz, O. Grumberg A framework for translating models and specification Integrated Formal Methods, LNCS, vol. 2335, Springer, Berlin (2002), pp. 145–164

[18]
C. Kern, M. Greenstreet Formal verification in hardware design: a survey ACM Transactions on Design Automation of Electronic Systems, 4 (1999), pp. 123–193

[19]
S. Kort, S. Tahar, P. Curzon Hierarchical formal verification using a hybrid tool International Journal on Software Tools for Technology Transfer, vol. 4Springer, Berlin (2002) pp. 1–10

[20]
I. Leslie, D. McAuley Fairisle: an ATM network for the local area ACM Communication Review, 19 (4) (1991), pp. 327–336

[21]
J. Lu, On the formal verification of ATM switches, MaSc. Thesis, Concordia University, Canada, 1999.

[22]
J. Lu, S. Tahar, D. Voicu, X. Song Model checking of a real ATM switch Proc. IEEE International Conference on Computer DesignIEEE Computer Society Press (1998), pp. 195–198

[23]
M.L. McMillan Symbolic Model Checking Kluwer (1993)

[24]
AsmL for Microsoft .NET (version 2.1.5.7), Microsoft, 2003. Available from: http://www.research.microsoft.com/foundations/asml.

[25]
S. Owre, J.M. Rushby, N. Shankar PVS: a prototype verification system Automated Deduction, LNCS, vol. 607, Springer, Berlin (1992), pp. 748–752

[26]
G. Schellhorn, Verification of abstract state machines, Ph.D. Thesis, University of Ulm, Germany, 1999.

[27]
N. Shankar Symbolic analysis of transition systems
Abstract State Machines, Theory and Applications, LNCS, vol. 1912, Springer, Berlin (2000), pp. 287–302

[28]
M. Spielmann Automatic verification of abstract state machines Computer Aided Verification, LNC, vol. 1633, Springer, Berlin (1999), pp. 431–442

[29]
S. Tahar, X. Song, E. Cerny, Z. Zhou, M. Langevin, O. Ait-Mohamed, Modeling and verification of the Fairisle ATM switch fabric using MDGs, in: IEEE Transactions on CAD of Integrated Circuits and Systems, vol. 18, No. 7, July 1999, pp. 956–972.

[30]
K. Winter, Model checking abstract state machines, Ph.D. Thesis, Technical University of Berlin, Germany, 2001.

[31]
Y. Xu, E. Cerny, X. Song, F. Corella, O. Mohamed Model checking for first-order temporal logic using multiway decision graphs Computer Aided Verification, LNCS, vol. 1427, Springer, Berlin (1998), pp. 219–231

[32]
Z. Zhou, N. Boulerice, MDG Tools (v1.0) User’s Manual, University of Montreal, Dept. of Information and Operation Research, 1996.

[33]
Z. Zhou, Multiway decision graphs and their applications in automatic verification of RTL designs, Ph.D. Thesis, University of Montreal, Dept. of Information and Operational Research, 1997.

[34]
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, 2001.

[35]
Z. Zhou, X. Song, S. Tahar, E. Cerny, F. Corella, M. Langevin Formal verification of the island tunnel controller using multiway decision graphs Formal Methods in Computer-Aided Design, LNCS, vol. 1166, Springer, Berlin (1996), pp. 233–246
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top