Automatic Abstraction in Model Checking

دانشگاه آزاد اسلامی اصفهان(خوراسگان)

منو

رکورد قبلی

رکورد بعدی

" Automatic Abstraction in Model Checking "

Document Type	:	Latin Dissertation
Language of Document	:	English
Record Number	:	149204
Doc. No	:	ET20996
Main Entry	:	Yuan Lu
Title Proper	:	Automatic Abstraction in Model Checking
Note	:	This document is digital این مدرک بصورت الکترونیکی می باشد
Abstract	:	As technology advances and demand for higher performance increases hardware de-signs are becoming more and more sophisticated, A typical chip design may containover ten million switching devices. Since the systems become more and more complex,detecting design errors for systems of such scale becomes extremely difficult. Formalverification methodologies can potentially catch subtle design errors. However, manystate-of-the-art formal verification tools suffer from the state explosion problem.This thesis explores abstraction techniques to avoid the state explosion problem. Inour methodology, atomic formulas extracted from an SMV-like concurrent programare used to construct abstractionfinctions. The initial abstract structure is built byusing abstraction techniques. When the model checker disproves a univer-sal property on the abstract structure, it generates a counterexample. However, thisabstract counterexample might be spurious because abstraction is not complete. Weprovide a new symbolic algorithm to determine whether an abstract counterexample isspurious. When a counterexampIe is identified to be spurious, the algorithm will com-pute the shortest.
Subject	:	Electericl tess
	:	برق
electronic file name	:	TL44142.pdf
Title and statement of responsibility and	:	Automatic Abstraction in Model Checking [Thesis]