Members

• Amjad Gawanmeh
• Sofiène Tahar
• Kirsten Winter

Description

Digital systems are becoming very large and complex making the process of finding bugs and design validation in early stages of the design cycle a must. As a contribution towards catching this goal, we propose in this thesis 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 mainly used for modeling hardware systems. Both ASM and MDG are based on a subset of many-sorted first order logic, making it appealing to link these two concepts. The proposed interface 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 consider both structural and behavioral models of hardware. We have applied this transformation schema on some examples and case studies where our tool generates the corresponding MDG-HDL models automatically

Publications

1. A. Gawanmeh, S. Tahar, and K. Winter: Formal Verification of ASM Designs using the MDG Tool; Proc. IEEE International Conference on Software Engineering and Formal Methods (SEFM'03), Brisbane, Australia, September 2003, pp. 210-219, IEEE Computer Society Press.
2. A. Gawanmeh, S. Tahar and K. Winter: Interfacing ASMs with the MDG Tool; In: E. Boerger, A. Gargantini, E. Riccobene (Eds.) Abstract State Machines - Advances in Theory and Applications, Lecture Notes in Computer Science 2589, Springer Verlag, 2003, pp. 278-292. Proc. International Conference on Abstract State Machines (ASM'03), Taormina, Italy, March 2003.
3. Amjad Gawanmeh: Interfacing Abstract State Machines with Multiway Decision Graphs, Concordia University, MASc thesis, Department of Electrical and Computer Engineering, April 2003.
4. A. Gawanmeh, S. Tahar and Kirsten Winter: Formal Verification of ASM Designs using the MDG Tool; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 2003. [28 pages]
5. A. Gawanmeh, S. Tahar, and K. Winter; A Tool for Verifying ASM Models Using Multiway Decision Graphs; Proc. 2003 Micronet Annual Workshop, Toronto, Canada, September 2003, pp 127-128.