東華大學圖書館 |

語系: 繁體中文

說明(常見問題)

回圖書館首頁

手機版館藏查詢

登入

回首頁

切換: 標籤 | MARC模式 | ISBD

Symbolic algorithms for verification...

Majumdar, Rupak.

FindBook

Google Book

Amazon

博客來

Symbolic algorithms for verification and control.

紀錄類型:	書目-電子資源 : Monograph/item
正題名/作者:	Symbolic algorithms for verification and control./
作者:	Majumdar, Rupak.
面頁冊數:	201 p.
附註:	Source: Dissertation Abstracts International, Volume: 65-02, Section: B, page: 0843.
Contained By:	Dissertation Abstracts International65-02B.
標題:	Computer Science. -
電子資源:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3121592
ISBN:	0496689436

Symbolic algorithms for verification and control.
Majumdar, Rupak.

Symbolic algorithms for verification and control. - 201 p.

Source: Dissertation Abstracts International, Volume: 65-02, Section: B, page: 0843.

Thesis (Ph.D.)--University of California, Berkeley, 2003.

Methods for the formal specification and verification of systems are indispensible for the development of complex yet correct systems. In formal verification, the designer describes the system in a modeling language with a well-defined semantics, and this system description is analyzed against a set of correctness requirements. Model checking is an algorithmic technique to check that a system description indeed satisfies correctness requirements given as logical specifications. While successful in hardware verification, the potential for model checking for software and embedded systems has not yet been realized. This is because traditional model checking focuses on systems modeled as finite state-transition graphs. While a natural model for hardware (especially synchronous hardware), state-transition graphs often do not capture software and embedded systems at an appropriate level of granularity. This dissertation considers two orthogonal extensions to finite state-transition graphs making model checking techniques applicable to both a wider class of systems and a wider class of properties.

ISBN: 0496689436Subjects--Topical Terms:

626642
Computer Science.

Symbolic algorithms for verification and control.
LDR:03138nmm 2200289 4500 001 1844206
005 20051017073445.5
008 130614s2003 eng d
020 $a 0496689436
035 $a (UnM)AAI3121592
035 $a AAI3121592
040 $a UnM $c UnM
100 1 $a Majumdar, Rupak. $3 908062
245 1 0 $a Symbolic algorithms for verification and control.
300 $a 201 p.
500 $a Source: Dissertation Abstracts International, Volume: 65-02, Section: B, page: 0843.
500 $a Chair: Thomas A. Henzinger.
502 $a Thesis (Ph.D.)--University of California, Berkeley, 2003.
520 $a Methods for the formal specification and verification of systems are indispensible for the development of complex yet correct systems. In formal verification, the designer describes the system in a modeling language with a well-defined semantics, and this system description is analyzed against a set of correctness requirements. Model checking is an algorithmic technique to check that a system description indeed satisfies correctness requirements given as logical specifications. While successful in hardware verification, the potential for model checking for software and embedded systems has not yet been realized. This is because traditional model checking focuses on systems modeled as finite state-transition graphs. While a natural model for hardware (especially synchronous hardware), state-transition graphs often do not capture software and embedded systems at an appropriate level of granularity. This dissertation considers two orthogonal extensions to finite state-transition graphs making model checking techniques applicable to both a wider class of systems and a wider class of properties.
520 $a The first direction is an extension to infinite-state structures finitely represented using constraints and operations on constraints. Infinite state arises when we wish to model variables with unbounded range (e.g., integers), or data structures, or real time. We provide a uniform framework of symbolic region algebras to study model checking of infinite-state systems. We also provide sufficient language-independent termination conditions for symbolic model checking algorithms on infinite state systems.
520 $a The second direction supplements verification with game theoretic reasoning. Games are natural models for interactions between components. We study game theoretic behavior with winning conditions given by temporal logic objectives both in the deterministic and in the probabilistic context. For deterministic games, we provide an extremal model characterization of fixpoint algorithms that link solutions of verification problems to solutions for games. For probabilistic games we study fixpoint characterization of winning probabilities for games with o-regular winning objectives, and construct (epsilon-)optimal winning strategies.
590 $a School code: 0028.
650 4 $a Computer Science. $3 626642
690 $a 0984
710 2 0 $a University of California, Berkeley. $3 687832
773 0 $t Dissertation Abstracts International $g 65-02B.
790 1 0 $a Henzinger, Thomas A., $e advisor
790 $a 0028
791 $a Ph.D.
792 $a 2003
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3121592