Incremental Verification of Aspectual Feature Module Based on Hierarchical State Machine
Qing Tan · Chinese Journal of Computers · 2009
Aspectual Feature Module(AFM) is a newly-proposed Software Product Line(SPL) programming paradigm,which solves the problems of existing SPL paradigms.But its inherent hybrid of parallel composition and sequential composition of modules prohibits the application of conventional verification technology,e.g.compositional verification and modular model checking.There is no verification method for AFM paradigm now,which restricts its application.This paper firstly establishes a formal model for AFM paradigm,and proposes an incremental verification method based on this model.This method starts from the verification of a small-scale AFM program and increases with the verification of just the recently-composed AFM module.It can avoid the state space exploration problem caused by a direct verification of a large-scale AFM program.