Breadcrumb

 
 

A practical model checking approach using FormalCheck

Title:

A practical model checking approach using FormalCheck

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

[img]
Preview
PDF
3810Kb

Abstract

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 > Faculty 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:Theses (M.A.Sc.)
Program:Electrical and Computer Engineering
Date:2000
Thesis Supervisor(s):Tahar, Sofiene
ID Code:1111
Deposited By:Concordia University Libraries
Deposited On:27 Aug 2009 13:16
Last Modified:08 Dec 2010 10:18
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

Document Downloads

More statistics for this item...

Concordia University - Footer