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