Breadcrumb

 
 

First order model checking of w-Automata using multiway decision graphs

Title:

First order model checking of w-Automata using multiway decision graphs

Wang, Fang (2005) First order model checking of w-Automata using multiway decision graphs. PhD thesis, Concordia University.

[img]
Preview
PDF - Accepted Version
4Mb

Abstract

As the complexity of hardware digital systems increases, their correctness becomes a major concern. Traditional verification by simulation is infeasible to exhaustively test and guarantee correctness. More than a decade ago, however, formal verification has been introduced as complement technique to simulation. Formal methods establish that a design implementation satisfies its specification by mathematical reasoning. Among several techniques, model checking is one of the most successful technology, which is based on the exploration of the design state space. In this thesis, we propose a new model checking method based on the theory of }-automata and multiway decision graphs (MDGs). Unlike reduced ordered binary decision diagrams (ROBDDs), MDGs allow system models to be described using abstract state machines (ASMs) through abstract data sorts and uninterpreted function symbols, hence enabling the verification of larger designs independent of the datapath width. Given an ASM and a first-order linear time temporal logic property, the model checking problem proposed in this thesis is reduced to a language emptiness checking of an }-automaton that accepts all }-words produced by the system violating the property formula. The checking method comprises four steps: (1) transforming the first-order property into a propositional formula by constructing ASMs for the atomic formulas of the property; (2) generating an }-automaton from the negation of the transformed propositional formula; (3) computing the product of the generated automaton, the system model ASM and the constructed ASMs; and (4) applying a language emptiness checking algorithm on the product automaton. Three different checking algorithms have been developed, implemented, and proved correct in this thesis. To evaluate the performance of the proposed model checking method and implemented tool, we conducted several experimentations and case studies. We also compared the efficiency of our tool with an existing MDG regular model checking application, as well as with popular ROBDD-based automata model checking tools such as VIS. Our model checker was found to be outperforming the above tools.

Divisions:Concordia University > Faculty of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Wang, Fang
Pagination:xii, 123 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Date:2005
Thesis Supervisor(s):Tahar, Sofiène
ID Code:8869
Deposited By:Concordia University Libraries
Deposited On:18 Aug 2011 14:38
Last Modified:18 Aug 2011 15:06
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