| LDR | | 00000nam u2200205 4500 |
| 001 | | 000000434080 |
| 005 | | 20200226140609 |
| 008 | | 200131s2019 ||||||||||||||||| ||eng d |
| 020 | |
▼a 9781085625500 |
| 035 | |
▼a (MiAaPQ)AAI13862811 |
| 040 | |
▼a MiAaPQ
▼c MiAaPQ
▼d 247004 |
| 082 | 0 |
▼a 621.3 |
| 100 | 1 |
▼a Jiang, Chuan. |
| 245 | 10 |
▼a Witness Generation in Existential CTL Model Checking. |
| 260 | |
▼a [S.l.]:
▼b Iowa State University.,
▼c 2019. |
| 260 | 1 |
▼a Ann Arbor:
▼b ProQuest Dissertations & Theses,
▼c 2019. |
| 300 | |
▼a 113 p. |
| 500 | |
▼a Source: Dissertations Abstracts International, Volume: 81-03, Section: B. |
| 500 | |
▼a Advisor: Ciardo, Gianfranco. |
| 502 | 1 |
▼a Thesis (Ph.D.)--Iowa State University, 2019. |
| 506 | |
▼a This item must not be sold to any third party vendors. |
| 506 | |
▼a This item must not be sold to any third party vendors. |
| 520 | |
▼a Hardware and software systems are widely used in applications where failure is prohibitively costly or even unacceptable. The main obstacle to make such systems more reliable and capable of more complex and sensitive tasks is our limited ability to design and implement them with sufficiently high degree of confidence in their correctness under all circumstances. As an automated technique that verifies the system early in the design phase, model checking explores the state space of the system exhaustively and rigorously to determine if the system satisfies the specifications and detect fatal errors that may be missed by simulation and testing. One essential advantage of model checking is the capability to generate witnesses and counterexamples. They are simple and straightforward forms to prove an existential specification or falsify a universal specification. Beside enhancing the credibility of the model checker's conclusion, they either strengthen engineers' confidence in the system or provide hints to reveal potential defects.In this dissertation, we focus on symbolic model checking with specifications expressed in computation tree logic (CTL), which describes branching-time behaviors of the system, and investigate the witness generation techniques for the existential fragment of CTL, i.e., ECTL, covering both decision-diagram-based and SAT-based.Since witnesses provide important debugging information and may be inspected by engineers, smaller ones are always preferable to ease their interpretation and understanding. To the best of our knowledge, no existing witness generation technique guarantees the minimality for a general ECTL formula with nested existential CTL operators. One contribution of this dissertation is to fill this gap with the minimality guarantee. With the help of the saturation algorithm, our approach computes the minimum witness size for the given ECTL formula in every state, stored as an additive edge-valued multiway decision diagrams (EV+MDD), a variant of the well-known binary decision diagram (BDD), and then builds a minimum witness. Though computationally intensive, this has promising applications in reducing engineers' workload.SAT-based model checking, in particular, bounded model checking, reduces a model checking problem problem into a satisfiability problem and leverages a SAT solver to solve it. Another contribution of this dissertation is to improve the translation of bounded semantics of ECTL into propositional formulas. By realizing the possibility of path reuse, i.e., a state may build its own witness by reusing its successor's, we may generate a significantly smaller formula, which is often easier for a SAT solver to answer, and thus boost the performance of bounded model checking. |
| 590 | |
▼a School code: 0097. |
| 650 | 4 |
▼a Computer science. |
| 650 | 4 |
▼a Electrical engineering. |
| 690 | |
▼a 0984 |
| 690 | |
▼a 0544 |
| 710 | 20 |
▼a Iowa State University.
▼b Computer Science. |
| 773 | 0 |
▼t Dissertations Abstracts International
▼g 81-03B. |
| 773 | |
▼t Dissertation Abstract International |
| 790 | |
▼a 0097 |
| 791 | |
▼a Ph.D. |
| 792 | |
▼a 2019 |
| 793 | |
▼a English |
| 856 | 40 |
▼u http://www.riss.kr/pdu/ddodLink.do?id=T15490977
▼n KERIS
▼z 이 자료의 원문은 한국교육학술정보원에서 제공합니다. |
| 980 | |
▼a 202002
▼f 2020 |
| 990 | |
▼a ***1816162 |
| 991 | |
▼a E-BOOK |