Members

• Fang Wang
• Sofiène Tahar
• Eduard Cerny

Description

In this project, we propose a new MDG based first-order model checking approach using w-automata as the unified models for both the property and the system design. In this approach the verification task is reduced to a language emptiness checking (LEC) problem, where the system design is described as an abstract state machine (ASM) encoded by MDGs, and the specification to be verified is represented by a new specification language, called Lmdg*, derived from the many sorted first-order logic and removing the limitations imposed by the previous MDG model checking tool. We have implemented a dedicated tool, called MDG-LEC, on top of the MDG package, which accepts models in MDG-HDL hardware description language. To evaluate the performance of our approach, we used MDG-LEC to conduct a few case studies and present several experimental results. We also compared its efficiency with the existing MDG regular model checking application, as well as to popular ROBDD-based automata model checking tools such as VIS and FormalCheck. Our MDG-LEC is found to be more performing than the above tools.

Publications

1. F. Wang, S. Tahar, and O. Ait Mohamed: First-order LTL Model Checking using MDGs; In: F. Wang (Ed.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 3299, Springer Verlag, 2004, pp. 441-455. [Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA'04), Taipei, Taiwan, November 2004]
2. F. Wang, S. Tahar, and O. Ait Mohamed: Automaton based Model Checking Using Multiway Decision Graphs; Proc. 2004 Micronet Annual Workshop, Alymer, Canada, April 2004, pp. 133-134.
3. F. Wang, A. Habibi, and S. Tahar: Translating LTL Specification to MDG-HDL; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'03), Montreal, Quebec, Canada, May 2003.Vol. 2, pp. 1369-1373.
4. F. Wang and S. Tahar: Language Emptiness Checking using MDGs; Proc. ACM 13th Great Lakes Symposium on VLSI (GLS-VLSI'03), Washington D.C., USA, April 2003, ACM Publications
5. F. Wang and S. Tahar: Towards Language Emptiness Model Checking for MDGs; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'02), Winnipeg, Manitoba, Canada, May 2002, Vol. 2, pp. 590-595.