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: 08 Apr 2019 *

Full-text access for editors Access for subscribers Purchase this article Comment on this article