Login | Register

A Design for verification approach using an embedding of PSL in AsmL

Title:

A Design for verification approach using an embedding of PSL in AsmL

Gawanmeh, Amjad, Tahar, Sofiène, Moinudeen, Haja and Habibi, Ali (2007) A Design for verification approach using an embedding of PSL in AsmL. Journal of Circuits, Systems and Computers, 16 (06). pp. 859-881. ISSN 0218-1266

[thumbnail of JCSC2008.pdf]
Preview
Text (application/pdf)
JCSC2008.pdf - Accepted Version
259kB

Official URL: http://dx.doi.org/10.1142/S0218126607004052

Abstract

In this paper, we propose to integrate an embedding of Property Specification Language (PSL) in Abstract State Machines Language (AsmL) with a top–down design for verification approach in order to enable the model checking of large systems at the early stages of the design process. We provide a complete embedding of PSL in the ASM language AsmL, which allows us to integrate PSL properties as a part of the design. For verification, we propose a technique based on the AsmL tool that translates the code containing both the design and the properties into a finite state machine (FSM) representation. We use the generated FSM to run model checking on an external tool, here SMV. Our approach takes advantage of the AsmL language capabilities to model designs at the system level as well as from the power of the AsmL tool in generating both C# code and FSMs from AsmL models. We applied our approach on the PCI-X bus standard, which AsmL model was constructed from the informal standard specifications and a subsequent UML model. Experimental results on the PCI-X bus case study showed a superiority of our approach to conventional verification.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Article
Refereed:Yes
Authors:Gawanmeh, Amjad and Tahar, Sofiène and Moinudeen, Haja and Habibi, Ali
Journal or Publication:Journal of Circuits, Systems and Computers
Date:2007
Digital Object Identifier (DOI):10.1142/S0218126607004052
Keywords:PSL; abstract state machines; AsmL; model checking; PCI-X bus
ID Code:977372
Deposited By: Danielle Dennie
Deposited On:14 Jun 2013 14:49
Last Modified:18 Jan 2018 17:44

References:

E. Börger and R. Stärk, Abstract State Machines: A Method for High-Level System Design and Analysis (Springer-Verlag, 2003).

K. Claessen and J. Martensson, Formal Methods in Computer-Aided Design, LNCS 3312 (Springer-Verlag, 2004) pp. 337–351.

K. H. Chang, A PCI-X verification environment using C and Verilog, VLSI Design/CAD Symp. (2003).

M. Chong, A PCI express to PCI-X bridge optimized for performance and area, Master's thesis, Department of Electrical Engineering and Computer Science, Massachussets Institute of Technology (2004).

M. Dwyer, Tool-supported program abstraction for finite-state verification, Int. Conf. Software Engineering (2001) pp. 177–187.

A. Gawanmeh, A. Habibi and S. Tahar, Languages for Formal Specification and Verification, Forum on Specification and Design Languages (2004).

A. Gawanmeh, A. Habibi and S. Tahar, Embedding and verification of PSL using ASM, IEEE Int. Workshop on System-on-Chip (2006) pp. 125–130.

A. Gawanmeh, S. Tahar and K. Winter, J. Syst. Architecture 54, 15 (2008), DOI: 10.1016/j.sysarc.2007.03.007

W. Grieskamp, Software Eng. Notes 27, 112 (2002), DOI: 10.1145/566171.566190

D. Grobe and R. Drechsler, Checkers for SystemC designs, 2nd ACM and IEEE Int. Conf. Formal Methods and Models for Codesign (2004) pp. 171–178.

M. Gordon, J. Hurd and K. Slind, Correct Hardware Design and Verification Methods, LNCS 2860 (Springer-Verlag, 2003) pp. 200–215.

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

M. Gordon, Formal Aspects Comput. 15, 406 (2003), DOI: 10.1007/s00165-003-0014-5

Y. Gurevich, Specification and Validation Methods (Oxford University Press, 1995).

Y. Gurevich, B. Rossman and W. Schulte, Semantic essence of AsmL, Technical Report, Microsoft Research, MSR-TR-2004-27, March 2004.

A. Habibi, A framework for system level verification: The SystemC case, PhD thesis, Concordia University, Montreal, Canada (2005).

A. Habibi and S. Tahar, Electron. Notes Theor. Comput. Sci. 131, 39 (2005), DOI: 10.1016/j.entcs.2005.01.021

J. Huggins, Abstract state machines website, http://www.eecs.umich.edu/gasm (2008).

M. L. McMillan, Symbolic Model Checking (Kluwer Academic Publishers, 1993).

H. Moinudeen, A. Habibi and S. Tahar, Design for verification of the PCI-X bus, IEEE Int. Conf. Formal Methods in Computer-Aided Design (IEEE Computer Society Press, 2006) pp. 187–188.

K. Oumalou, A. Habibi and S. Tahar, Design for verification of a PCI bus in SystemC, Symp. System-on-Chip (IEEE Computer Society Press, 2004) pp. 201–204.

PCI Special Interest Group, www.pcisig.com (2005).
Accellera Property Specification Language Reference Manual, Version 1.01, http://www.accellera.org (2008).

K. Shimizu, D. Dill and A. Hu, Formal Methods in Computer-Aided Design, LNCS 1954 (Springer-Verlag, 2000) pp. 335–353.
SystemVerilog, http://www.systemverilog.org (2008).

C. Wallace, Specification and Validation Methods (Oxford University Press, 1995) pp. 131–164.

R. Wang and Z. Wen, A verification environment for PCI-X BFMs in VERA, Technical report, Synopsys Inc. (2002).

K. Winter, Model checking abstract state machines, PhD thesis, Technical University of Berlin, Germany (2001).

C. C. Yu, System level assertion-based verification environment for PCI/PCI-X and PCI-express, VLSI Design/CAD Symp. (2004).
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