.png){kind=icon}
.png){kind=icon}
Return
Homing Sequence Derivation With Quantified Boolean Satisfiability
.png){kind=icon}
OA
AI
DOI：10.1109/TC.2021.3058302.png)
.png){kind=icon}
.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Homing sequence derivation for nondeterministic finite state machines (NFSMs) has important applications in software/hardware system testing and verification. Unlike prior methods based on explicit tree-based search, in this article we formulate the derivation of a preset/adaptive homing sequence in terms of quantified Boolean formula (QBF) solving. This formulation exploits compact circuit representation of NFSMs and QBF encoding of the existence condition of homing sequence for effective computation. The implicit circuit representation effectively avoids explicit state enumeration, and can be more scalable. Different encoding schemes and QBF solvers are evaluated for their suitability for the homing sequence derivation. Experiments on various computation methods and benchmarks show the generality and feasibility of a proposed approach.
Keywords:
Testing
Vegetation
Encoding
Monitoring
Complexity theory
Benchmark testing
Labeling
Homing sequence
nondeterministic finite state machine
quantified Boolean formula
AI Summary
Key information extracted from the uploaded paper, including a brief overview, abstract, background, key highlights, visual analysis, and future outlook.
Journal
IF:
3.8
Papers:
5.3K
Citations:
9.8K
Organization
View more organizations