Distinguishing extended finite state machine configurations using predicate abstraction


  • Khaled El-Fakih American University of Sharjah, P.O. Box 26666, Sharjah, United Arab Emirates
  • Nina Yevtushenko Tomsk State University, Tomsk, Russia
  • Marius Bozga Verimag, Grenoble, France
  • Saddek Bensalem Verimag, Grenoble, France


Model based conformance testing, Mutation testing, Model transformation, Extended finite state machines, Predicate abstraction, Distinguishing sequences



Extended Finite State Machines (EFSMs) provide a powerful model for the derivation of functional tests for software systems and protocols. Many EFSM based testing problems, such as mutation testing, fault diagnosis, and test derivation involve the derivation of input sequences that distinguish configurations of a given EFSM specification.;

Method and Results

In this paper, a method is proposed for the derivation of a distinguishing sequence for two explicitly given or symbolically represented, possibly infinite, sets of EFSM configurations using a corresponding FSM abstraction that is derived based on finite sets of predicates and parameterized inputs. An abstraction function that maps configurations and transitions of the EFSM specification to corresponding abstract states and transitions of the abstraction FSM is proposed. Properties of the abstraction are established along with a discussion on a proper selection of the sets of predicates and parameterized inputs used while deriving an FSM abstraction. If no distinguishing sequence is found for the current FSM abstraction then a refined abstraction is constructed by extending the sets of predicates and parameterized inputs. Simple heuristics for the selection of additional predicates are discussed and application examples are provided.;


The work can be applied in various domains such as EFSM-based test derivation, mutation testing, and fault diagnosis.;



Download data is not yet available.




How to Cite

El-Fakih, K., Yevtushenko, N., Bozga, M., & Bensalem, S. (2016). Distinguishing extended finite state machine configurations using predicate abstraction. Journal of Software Engineering Research and Development, 4, 1:1 – 1:26. Retrieved from https://sol.sbc.org.br/journals/index.php/jserd/article/view/429



Research Article