K-Branching UIO Sequences for Partially Specified Observable Non-Deterministic FSMs

dc.contributor.authorEl-Fakih, Khaled
dc.contributor.authorHierons, Robert M.
dc.contributor.authorTurker, Uraz Cengiz
dc.date.accessioned2025-10-29T11:13:55Z
dc.date.issued2021
dc.departmentGebze Teknik Üniversitesi
dc.description.abstractIn black-box testing, test sequences may be constructed from systems modelled as deterministic finite-state machines (DFSMs) or, more generally, observable non-deterministic finite state machines (ONFSMs). Test sequences usually contain state identification sequences, with unique input output sequences (UIOS) often being used with DFSMs. This paper extends the notion of UIOS to ONFSMs. One challenge is that, as a result of non-determinism, the application of an input sequence can lead to exponentially many expected output sequences. To address this scalability problem, we introduce K-UIOS: UIOS that lead to at most K output sequences from states of M. We show that checking K-UIO existence is PSPACE-Complete if the problem is suitably bounded; otherwise it is in EXPSPACE and PSPACE-Hard. We provide a massively parallel algorithm for constructing K-UIOS and the results of experiments on randomly generated and real FSM specifications. The proposed algorithm was able to construct UIOS in cases where the existing UIO generation algorithm could not and was able to construct UIOS from FSMs with 38K states and 400K transitions.
dc.description.sponsorshipAUS [eFRG18-SET-CEN-49]
dc.description.sponsorshipEPSRC [EP/R025134/2] Funding Source: UKRI
dc.description.sponsorshipSPF [EP/V026801/2] Funding Source: UKRI
dc.description.sponsorshipThis work is partially supported by AUS under grant eFRG18-SET-CEN-49. Author names are given according to the Hardy-Littlewood Rule, i.e., author names are provided in alphabetical order regarding the family names in ascending order.
dc.identifier.doi10.1109/TSE.2019.2911076
dc.identifier.endpage1040
dc.identifier.issn0098-5589
dc.identifier.issn1939-3520
dc.identifier.issue5
dc.identifier.orcid0000-0001-5976-1945
dc.identifier.orcid0000-0002-4771-1446
dc.identifier.scopus2-s2.0-85074327465
dc.identifier.scopusqualityQ1
dc.identifier.startpage1029
dc.identifier.urihttps://doi.org/10.1109/TSE.2019.2911076
dc.identifier.urihttps://hdl.handle.net/20.500.14854/6967
dc.identifier.volume47
dc.identifier.wosWOS:000650457700010
dc.identifier.wosqualityQ1
dc.indekslendigikaynakWeb of Science
dc.indekslendigikaynakScopus
dc.language.isoen
dc.publisherIEEE Computer Soc
dc.relation.ispartofIEEE Transactions on Software Engineering
dc.relation.publicationcategoryMakale - Uluslararası Hakemli Dergi - Kurum Öğretim Elemanı
dc.rightsinfo:eu-repo/semantics/closedAccess
dc.snmzKA_WOS_20251020
dc.subjectSoftware engineering/software/program verification
dc.subjectsoftware engineering/testing and debugging
dc.subjectsoftware engineering/test design
dc.subjectfinite state machine
dc.subjectunique input output sequence generation
dc.subjectgeneral purpose graphics processing units
dc.titleK-Branching UIO Sequences for Partially Specified Observable Non-Deterministic FSMs
dc.typeArticle

Dosyalar