Multi-valued Model Checking Of Software Product Lines

Software product line engeering(SPLE) manages commonalities and variabilities in software product lines to reduce cost and improve productivity, where commnalities and variabilites are expressed in terms of features. Model checking is an automatic verification technique. Nowadays, SPLE is widespread in industry, including critical areas like automotive and avionics. The emergence and the increasing popularity of SPLs have raised the need for model checking software product lines. Since the design decisions for a feature may be unkown in the early stage of software development, the systems may be with uncertainties. Currently, most attempts to address model checking problems of software product lines do not nicely support uncertain and inconsistent information and we consider model checking partial software product line designs, where incomplete information can be captured by multi-valued logics. This enables detecting design errors earlier, reducing the cost of later development of final products.To this end, we first propose bilattice-based feature transition systems(BFTS) for modeling partial software product line designs, which support description of uncertainty and preserve features as a first class notion; the partial model and final model of product are defined via projection and simulation. We then express system behavioral properties using ACTL formulas and define its semantics over BFTSs. In this thesis, we investigates model checking software product lines basd on bilattice in two efficient ways: 1)we provide the procedures that translated BFTSs to multi-valued Kripke structure and develop a software model checker assistant BPMCA to leverage the power of exstiong model checking engine called c Chek for verification,. 2)we decompose the multi-valued BFTS into 3-valued BFTS so that multi-valued model checking problems are decomposed into 3-valued model checking problems, which lower the complexity of model checking. Finally, we implement our approach and illustrate its effectiveness on a benchmark from literature.