Login | Register

A practical model checking approach using FormalCheck


A practical model checking approach using FormalCheck

Barakatain, Leila (2000) A practical model checking approach using FormalCheck. Masters thesis, Concordia University.

[thumbnail of MQ54316.pdf]
Text (application/pdf)


Verification of industrial designs is becoming more challenging as technology advances and demand for higher performance increases. One of the most suitable debugging aids is automatic formal verification, which tests behaviors under all possible executions of a system. However, automatic formal verification is limited by the state explosion problem. This thesis presents a practical verification approach using FormalCheck, which helps reducing the state space explosion problem when verifying the high level descriptions of practical systems. This approach relies on the design's built-in hierarchy as the mechanism to conquer its complexity during verification. Then an assume guarantee paradigm is used to verify functional units built on top of instantiated and previously verified modules. We applied this approach to an industrial design (Transmit Master/Receive Slave (TMRS) Telecom System Block) as a case study. The TMRS was thoroughly verified and in consistencies in the design with respect to its specification were uncovered through model checking. The main contributions of this thesis are, (1) the application of a variety of model checking techniques to a real size design and (2) proposing a number of improvements to the design flow which can accelerate the whole verification process.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Barakatain, Leila
Pagination:107 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Thesis Supervisor(s):Tahar, Sofiene
Identification Number:TK 7874 B36 2000
ID Code:1111
Deposited By: Concordia University Library
Deposited On:27 Aug 2009 17:16
Last Modified:13 Jul 2020 19:48
Related URLs:
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