Title: Model checking software product line based on multi-valued logic

Authors: Shuang Liu; Yu-Feng Shi; Ming-Y Huang

Addresses: Department of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nan Jing, Jiang Su, China ' Department of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nan Jing, Jiang Su, China ' Department of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nan Jing, Jiang Su, China

Abstract: Software product line (SPL) maximises commonality between software products to reduce cost and improve productivity. SPL has been widely applied in critical systems, and ensuring correctness of the system is thus of great importance. In this paper, we consider the incomplete designs in the early stage of software development. This enables detecting design errors earlier, reducing the cost of later development of final products. We first propose bilattice-based feature transitions systems (BFTSs), which support description of uncertainty. We then express system behavioural properties using ACTL formulas and define its semantics over BFTSs. On the one hand, we provide the procedures that translate BFTSs to multi-valued Kripke structure and develop a software model checker assistant BPMCA. On the other hand, we decompose the multi-valued BFTS to lower the complexity of model checking. Finally, we implement our approach and illustrate its effectiveness on a benchmark from the literature.

Keywords: model checking; software product line; multi-valued.

DOI: 10.1504/IJRS.2018.096060

International Journal of Reliability and Safety, 2018 Vol.12 No.4, pp.364 - 393

Received: 02 Apr 2018
Accepted: 01 Jun 2018
Published online: 09 Nov 2018 *

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