Homing sequence derivation with quantified boolean satisfiability

Hung En Wang, Kuan Hua Tu, Jie Hong R. Jiang, Natalia Kushik

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

Homing sequence derivation for nondeterministic finite state machines (NFSMs) has important applications in system testing and verification. Unlike prior methods based on explicit tree based search, in this work we formulate the derivation of a preset homing sequence in terms of a quantified Boolean formula (QBF). The formulation allows implicit NFSM representation and compact QBF encoding for effective computation. Different encoding schemes and QBF solvers are evaluated for their suitability to homing sequence derivation. Experimental results show the generality and feasibility of the proposed method.

Original languageEnglish
Title of host publicationTesting Software and Systems - 29th IFIP WG 6.1 International Conference, ICTSS 2017, Proceedings
EditorsNina Yevtushenko, Ana Rosa Cavalli, Husnu Yenigun
PublisherSpringer Verlag
Pages230-242
Number of pages13
ISBN (Print)9783319675480
DOIs
Publication statusPublished - 1 Jan 2017
Externally publishedYes
Event29th IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2017 - St. Petersburg, Russian Federation
Duration: 9 Oct 201711 Oct 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10533 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference29th IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2017
Country/TerritoryRussian Federation
CitySt. Petersburg
Period9/10/1711/10/17

Fingerprint

Dive into the research topics of 'Homing sequence derivation with quantified boolean satisfiability'. Together they form a unique fingerprint.

Cite this