Title: Model checking software product lines based on feature slicing
Authors: Ming-Yu Huang; Yu-Mei Liu
Addresses: Department of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nang Jing, Jiang Su, China ' Department of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nang Jing, Jiang Su, China
Abstract: Feature model is a popular formalism for describing the commonality and variability of a software product line in terms of features. Feature models symbolise a presentation of the possible application configuration space, and can be customised based on specific domain requirements and stakeholder goals. As feature models are becoming increasingly complex, it is desired to provide automatic support for customised analysis and verification based on the specific goals and requirements of stakeholders. This paper first presents feature model slicing based on the requirements of the users. We then introduce three-valued abstraction of behaviour models based on the slicing unit. Finally, based on multi-valued model checker, a case study was conducted to illustrate the effectiveness of our approach.
Keywords: feature model; slicing; three-valued model; model checking.
DOI: 10.1504/IJCSE.2019.099072
International Journal of Computational Science and Engineering, 2019 Vol.18 No.4, pp.340 - 348
Received: 15 May 2016
Accepted: 12 Sep 2016
Published online: 15 Apr 2019 *