%0 Conference Proceedings
%T Homing Sequence Derivation with Quantified Boolean Satisfiability
%+ National Taiwan University [Taiwan] (NTU)
%+ Tomsk State University [Tomsk]
%+ Méthodes et modèles pour les réseaux (METHODES-SAMOVAR)
%+ Département Réseaux et Services Multimédia Mobiles (TSP - RS2M)
%+ Centre National de la Recherche Scientifique (CNRS)
%A Wang, Hung-En
%A Tu, Kuan-Hua
%A Jiang, Jie-Hong, R.
%A Kushik, Natalia
%Z Part 4: Test Selection and Quality Estimation
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 29th IFIP International Conference on Testing Software and Systems (ICTSS)
%C St. Petersburg, Russia
%Y Nina Yevtushenko
%Y Ana Rosa Cavalli
%Y Hüsnü Yenigün
%I Springer International Publishing
%3 Testing Software and Systems
%V LNCS-10533
%P 230-242
%8 2017-10-09
%D 2017
%R 10.1007/978-3-319-67549-7_14
%K Nondeterministic finite state machine
%K Homing sequence
%K Quantified Boolean formula
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01678974/document
%2 https://inria.hal.science/hal-01678974/file/449632_1_En_14_Chapter.pdf
%L hal-01678974
%U https://inria.hal.science/hal-01678974
%~ INSTITUT-TELECOM
%~ CNRS
%~ TELECOM-SUDPARIS
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-ICTSS
%~ UNIV-PARIS-SACLAY
%~ TELECOM-SUDPARIS-SACLAY
%~ IFIP-LNCS-10533
%~ INSTITUTS-TELECOM