University of Leicester
paper_HFSM_vanderson_v20(2).pdf (1.57 MB)

Hierarchical featured state machines

Download (1.57 MB)
journal contribution
posted on 2019-04-04, 09:53 authored by VH Fragal, A Simao, MR Mousavi
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.



Science of Computer Programming, 2019, 171, pp. 67-88

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Informatics


  • AM (Accepted Manuscript)

Published in

Science of Computer Programming







Acceptance date


Copyright date


Publisher version


The file associated with this record is under embargo until 12 months after publication, in accordance with the publisher's self-archiving policy. The full text may be available through the publisher links provided above.



Usage metrics

    University of Leicester Publications