Skip to Main content Skip to Navigation
Conference papers

From Passive to Active FSM Inference via Checking Sequence Construction

Abstract : The paper focuses on the problems of passive and active FSM inference as well as checking sequence generation. We consider the setting where an FSM cannot be reset so that its inference is constrained to a single trace either given a priori in passive inference scenario or to be constructed in active inference scenario or aiming at obtaining checking sequence for a given FSM. In each of the last two cases, the expected result is a trace representing a checking sequence for an inferred machine, if it was not given. We demonstrate that this can be achieved by a repetitive use of a procedure that infers an FSM from a given trace (identifying a minimal machine consistent with a trace) avoiding equivalent conjectures. We thus show that FSM inference and checking sequence construction can be seen as two sides of the same coin. Following an existing approach of constructing conjectures by SAT solving, we elaborate first such a procedure and then based on it the methods for obtaining checking sequence for a given FSM and inferring a machine from a black box. The novelty of our approach is that it does not use any state identification facilities. We only assume that we know initially the input set and a bound on the number of states of the machine. Experiments with a prototype implementation of the developed approach using as a backend an existing SAT solver indicate that it scales for FSMs with up to a dozen of states and requires relatively short sequences to identify the machine.
Complete list of metadata

Cited literature [27 references]  Display  Hide  Download
Contributor : Hal Ifip <>
Submitted on : Tuesday, January 9, 2018 - 3:43:31 PM
Last modification on : Friday, March 26, 2021 - 3:30:28 AM
Long-term archiving on: : Wednesday, May 23, 2018 - 4:37:05 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Alexandre Petrenko, Florent Avellaneda, Roland Groz, Catherine Oriat. From Passive to Active FSM Inference via Checking Sequence Construction. 29th IFIP International Conference on Testing Software and Systems (ICTSS), Oct 2017, St. Petersburg, Russia. pp.126-141, ⟨10.1007/978-3-319-67549-7_8⟩. ⟨hal-01678991⟩



Record views


Files downloads