Hierarchical featured state machines

Variants of the Finite State Machine (FSM) model have been extensively used to describe the behavior of reactive systems. In particular, several model-based testing techniques have been developed to support test case generation from FSMs and test case execution. Most of such techniques require several validation properties to hold for the underlying test models. Featured Finite State Machine (FFSM) is an extension of the FSM model proposed in our earlier publication that represents the abstract behavior of an entire Software Product Line (SPL). By validating an FFSM, we validate all valid products configurations of the SPL looking forward configurable test suites. However, modeling a large SPL using flat FFSMs may lead to a huge and hard-to-maintain specification. In this paper, we propose an extension of the FFSM model, named Hierarchical Featured State Machine (HFSM). Inspired by Statecharts and UML state machines, we introduce the HFSM model to improve model readability by grouping up FFSM conditional states and transitions into abstracted entities. Our ultimate goal is to use HFSMs as test models. To this end, we first define some syntactic and semantical validation criteria for HFSMs as prerequisites for using them as test models. Moreover, we implement an adapted graphical Eclipse-based editor from the Yakindu Project for modeling, derivation, and checking feature-oriented properties using Satisfiability Modulo Theory (SMT) solver tools. We investigate the applicability of our approach by applying it to an HFSM for a realistic case study (the Body Comfort System). The results indicate that HFSMs can be used to compactly represent and efficiently validate the behavior of parallel components in SPLs.