Model checking software product line based on multi-valued logic Online publication date: Fri, 09-Nov-2018
by Shuang Liu; Yu-Feng Shi; Ming-Y Huang
International Journal of Reliability and Safety (IJRS), Vol. 12, No. 4, 2018
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.
Existing subscribers:
Go to Inderscience Online Journals to access the Full Text of this article.
If you are not a subscriber and you just want to read the full contents of this article, buy online access here.Complimentary Subscribers, Editors or Members of the Editorial Board of the International Journal of Reliability and Safety (IJRS):
Login with your Inderscience username and password:
Want to subscribe?
A subscription gives you complete access to all articles in the current issue, as well as to all articles in the previous three years (where applicable). See our Orders page to subscribe.
If you still need assistance, please email subs@inderscience.com
Our Blog 
Follow us on Twitter 
Visit us on Facebook