<  Back to the Polytechnique Montréal portal

On the verification of a WiMax design using symbolic simulation

Salim Ismail Al-Akhras, Sofiène Tahar, Gabriela Nicolescu, Michel Langevin and Pierre Paulin

Paper (2012)

Open Acess document in PolyPublie and at official publisher
Open Access to the full text of this document
Published Version
Terms of Use: Creative Commons Attribution
Download (262kB)
Show abstract
Hide abstract


In top-down multilevel design methodologies, design descriptions at higher levels of abstraction are incrementally refined to the final realizations. Simulation based techniques have traditionally been used to verify that such model refinements do not change the design functionality. Unfortunately, with computer simulations it is not possible to completely check that a design transformation is correct in a reasonable amount of time, as the number of test patterns required to do so increase exponentially with the number of system state variables. In this paper, we propose a methodology for the verification of conformance of models generated at higher levels of abstraction in the design process to the design specifications. We model the system behavior using sequence of recurrence equations. We then use symbolic simulation together with equivalence checking and property checking techniques for design verification. Using our proposed method, we have verified the equivalence of three WiMax system models at different levels of design abstraction, and the correctness of various system properties on those models. Our symbolic modeling and verification experiments show that the proposed verification methodology provides performance advantage over its numerical counterpart.

Subjects: 2700 Information technology > 2706 Software engineering
Department: Department of Computer Engineering and Software Engineering
PolyPublie URL: https://publications.polymtl.ca/10595/
Conference Title: 4th International Symposium on Symbolic Computation in Software Science
Conference Location: Gammarth, Tunisia
Conference Date(s): 2012-12-15 - 2012-12-17
Journal Title: Electronic Proceedings in Theoretical Computer Science (vol. 122)
DOI: 10.4204/eptcs.122.3
Official URL: https://doi.org/10.4204/eptcs.122.3
Date Deposited: 02 Oct 2023 15:41
Last Modified: 10 Apr 2024 00:14
Cite in APA 7: Al-Akhras, S. I., Tahar, S., Nicolescu, G., Langevin, M., & Paulin, P. (2012, December). On the verification of a WiMax design using symbolic simulation [Paper]. 4th International Symposium on Symbolic Computation in Software Science, Gammarth, Tunisia. Published in Electronic Proceedings in Theoretical Computer Science, 122. https://doi.org/10.4204/eptcs.122.3


Total downloads

Downloads per month in the last year

Origin of downloads


Repository Staff Only

View Item View Item