東華大學圖書館 |

Language: English

Help

回圖書館首頁

手機版館藏查詢

Back

Switch To: Labeled | MARC Mode | ISBD

Integration of model checking into s...

Xie, Fei.

Linked to FindBook

Google Book

Amazon

博客來

Integration of model checking into software development processes.

Record Type:	Electronic resources : Monograph/item
Title/Author:	Integration of model checking into software development processes./
Author:	Xie, Fei.
Description:	163 p.
Notes:	Source: Dissertation Abstracts International, Volume: 65-08, Section: B, page: 4123.
Contained By:	Dissertation Abstracts International65-08B.
Subject:	Computer Science. -
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3143493
ISBN:	9780496014507

Integration of model checking into software development processes.
Xie, Fei.

Integration of model checking into software development processes. - 163 p.

Source: Dissertation Abstracts International, Volume: 65-08, Section: B, page: 4123.

Thesis (Ph.D.)--The University of Texas at Austin, 2004.

Testing has been the dominant method for validation of software systems. As software systems become complex, conventional testing methods have become inadequate. Model checking is a powerful formal verification method. It supports systematic exploration of all states or execution paths of the system being verified. There are two major challenges in practical and scalable application of model checking to software systems: (1) the applicability of model checking to software systems and (2) the intrinsic complexity of model checking.

ISBN: 9780496014507Subjects--Topical Terms:

626642
Computer Science.

Integration of model checking into software development processes.
LDR:03486nmm 2200277 4500 001 1827159
005 20061222091107.5
008 130610s2004 eng d
020 $a 9780496014507
035 $a (UnM)AAI3143493
035 $a AAI3143493
040 $a UnM $c UnM
100 1 $a Xie, Fei. $3 1916105
245 1 0 $a Integration of model checking into software development processes.
300 $a 163 p.
500 $a Source: Dissertation Abstracts International, Volume: 65-08, Section: B, page: 4123.
500 $a Supervisor: James C. Browne.
502 $a Thesis (Ph.D.)--The University of Texas at Austin, 2004.
520 $a Testing has been the dominant method for validation of software systems. As software systems become complex, conventional testing methods have become inadequate. Model checking is a powerful formal verification method. It supports systematic exploration of all states or execution paths of the system being verified. There are two major challenges in practical and scalable application of model checking to software systems: (1) the applicability of model checking to software systems and (2) the intrinsic complexity of model checking.
520 $a In this dissertation, we have developed a comprehensive approach to integration of model checking into two emerging software development processes: Model-Driven Development (MDD) and Component-Based Development (CBD), and a combination of MDD and CBD. This approach addresses the two major challenges under the following framework: (1) bridging applicability gaps through automatic translation of software representations to directly model-checkable formal representations, (2) seamless integration of state space reduction algorithms in the translation through static analysis, and (3) scaling model checking capability and achieving state space reduction by systematically exploring compositional structures of software systems. We have integrated model checking into MDD by applying mature model checking techniques to industrial design-level software representations through automatic translation of these representations to the input formal representations of model checkers. We have developed a translation-based approach to compositional reasoning of software systems, which simplifies the proof, implementation, and application of compositional reasoning rules at the software system level by reusing the proof and implementation of existing compositional reasoning rules for directly model-checkable formal representations. We have developed an integrated state space reduction framework which systematically conducts a top-down decomposition of a large and complex software system into directly model-checkable components by exploring domain-specific knowledge. We have designed, implemented, and applied a bottom-up approach to model checking of component-based software systems, which composes verified systems from verified components and integrates model checking into CBD. We have further scaled model checking of component-based systems by exploring the synergy between MDD and CBD, i.e., specifying components in executable design languages, and realizing the bottom-up approach based on model checking of software designs through translation.
590 $a School code: 0227.
650 4 $a Computer Science. $3 626642
690 $a 0984
710 2 0 $a The University of Texas at Austin. $3 718984
773 0 $t Dissertation Abstracts International $g 65-08B.
790 1 0 $a Browne, James C., $e advisor
790 $a 0227
791 $a Ph.D.
792 $a 2004
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3143493