Model checking software product line based on multi-valued logic

Shuang Liu, Yu-Feng Shi and Ming-Y Huang

International Journal of Reliability and Safety, 2018, vol. 12, issue 4, 364-393

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. (search for similar items in EconPapers)
Date: 2018
References: Add references at CitEc
Citations:

Downloads: (external link)
http://www.inderscience.com/link.php?id=96060 (text/html)
Access to full text is restricted to subscribers.

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:ids:ijrsaf:v:12:y:2018:i:4:p:364-393

Access Statistics for this article

More articles in International Journal of Reliability and Safety from Inderscience Enterprises Ltd
Bibliographic data for series maintained by Sarah Parker ().