자료유형  

 학위논문

Control Number  

0017161445

International Standard Book Number  

9798382841991

Dewey Decimal Classification Number  

004

Main Entry-Personal Name  

Ni, Haobin.

Publication, Distribution, etc. (Imprint  

[S.l.] : Cornell University., 2024

Publication, Distribution, etc. (Imprint  

Ann Arbor : ProQuest Dissertations & Theses, 2024

Physical Description  

201 p.

General Note  

Source: Dissertations Abstracts International, Volume: 85-12, Section: B.

General Note  

Advisor: Morrisett, John.

Dissertation Note  

Thesis (Ph.D.)--Cornell University, 2024.

Summary, Etc.  

요약Software systems today struggle to behave as intended in deployment. The problem is made worse by the ever-increasing complexity of systems resulting from the rapid expansion of modern-day software. For instance, almost all systems nowadays utilize concurrency, and unexpected behaviors such as race conditions are quite common. In this case and many others, the number of possible program behaviors suffers from combinatorial explosion, which renders conventional testing insufficient to provide enough assurance at a feasible cost.This dissertation explores alternative approaches that guarantee high assurance systematically and foundationally by building and analyzing formal models of those systems through domain-specific languages. While real-world systems often involve components of many different domains, as a first step, we choose three mission-critical domains as targets: fault-tolerant distributed protocols, concurrent programs, and parsers. For each of those domains, a new language for formally modeling domain-specific systems is proposed. Meta-theoretic analyses of those languages illustrate the relationships between models built in those languages and the realistic behaviors of the systems those models describe, guaranteeing that all those formal models are adequate for analyzing system behaviors. Case studies of systems modeled and analyzed using those languages are also presented to demonstrate the effectiveness of this approach and the developed tools in constructing high-assurance domain-specific systems.

Subject Added Entry-Topical Term  

Computer science.

Subject Added Entry-Topical Term  

Computer engineering.

Subject Added Entry-Topical Term  

Systems science.

Index Term-Uncontrolled  

Concurrent systems

Index Term-Uncontrolled  

Distributed systems

Index Term-Uncontrolled  

Formal method

Index Term-Uncontrolled  

Programming language

Index Term-Uncontrolled  

Syntactic analysis

Index Term-Uncontrolled  

Verification

Added Entry-Corporate Name  

Cornell University Computer Science

Host Item Entry  

Dissertations Abstracts International. 85-12B.

Electronic Location and Access  

로그인을 한후 보실 수 있는 자료입니다.

Control Number  

joongbu:658025