Login | Register

Abstract property verifier based on multiway decision graphs


Abstract property verifier based on multiway decision graphs

Hussain, Kamran (2007) Abstract property verifier based on multiway decision graphs. Masters thesis, Concordia University.

[thumbnail of MR40883.pdf]
Text (application/pdf)
MR40883.pdf - Accepted Version


Symbolic model-checking tools encounter state-explosion problem when verifying designs with large data paths. Multiway Decision Graph (MDG) model-checker uses abstract data representation and applies abstract operations to address the state explosion problem. The MDG verification tool, also known as Abstract Verifier, takes as input the specification (written as properties) and the description of the design, and then proves or disproves if the design satisfies these properties. The original specification language of the Abstract Verifier was called L mdg that provides temporal operators and abstract data types to formalize properties. Meanwhile, the Property Specification Language (PSL) has changed the verification world by introducing very rich temporal operators but without abstract data types. In this thesis, we propose a new specification language called Abstract Property Language (APL), for the MDG model-checker. This language replaces the L mdg specification language by introducing new operators borrowed from PSL to improve its expressiveness. We provide the formal definition of this language in BackusNaur form (BNF) and provide its formal semantics based on the computational model of the Abstract Verifier. APL is associated with a front-end translator that accepts APL specifications and builds verification-ready models to be handled directly inside the MDG model-checker. Finally, we have validated our APL language and the translator tool on the verification of several test benches including Look-Aside Interface (LA-1) design.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (Masters)
Authors:Hussain, Kamran
Pagination:xii, 116 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Electrical and Computer Engineering
Thesis Supervisor(s):Ait Mohamed, Otmane
Identification Number:LE 3 C66E44M 2007 H87
ID Code:975629
Deposited By: Concordia University Library
Deposited On:22 Jan 2013 16:12
Last Modified:13 Jul 2020 20:08
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