Identifying Counterexamples Without Variability in Software Product Line Model Checking

Product detection based on state abstraction technologies in the software product line(SPL)is more complex when compared to a single system.This variability constitutes a new complexity,and the counterexample may be valid for some products but spurious for others.In this paper,we found that spurious products are primarily due to the failure states,which correspond to the spurious counterexamples.The violated products correspond to the real counterexamples.Hence,identifying counterexamples is a critical problem in detecting violated products.In our approach,we obtain the violated products through the genuine counterexamples,which have no failure state,to avoid the tedious computation of identifying spurious products dealt with by the existing algorithm.This can be executed in parallel to improve the efficiency further.Experimental results showthat our approach performswell,varying with the growth of the system scale.By analyzing counterexamples in the abstract model,we observed that spurious products occur in the failure state.The approach helps in identifying whether a counterexample is spurious or genuine.The approach also helps to check whether a failure state exists in the counterexample.The performance evaluation shows that the proposed approach helps significantly in improving the efficiency of abstraction-based SPL model checking.

Binary Oriented Feature Selection for Valid Product Derivation in Software Product Line

Software Product Line(SPL)is a group of software-intensive systems that share common and variable resources for developing a particular system.The feature model is a tree-type structure used to manage SPL’s common and variable features with their different relations and problem of Crosstree Constraints(CTC).CTC problems exist in groups of common and variable features among the sub-tree of feature models more diverse in Internet of Things(IoT)devices because different Internet devices and protocols are communicated.Therefore,managing the CTC problem to achieve valid product configuration in IoT-based SPL is more complex,time-consuming,and hard.However,the CTC problem needs to be considered in previously proposed approaches such as Commonality VariabilityModeling of Features(COVAMOF)andGenarch+tool;therefore,invalid products are generated.This research has proposed a novel approach Binary Oriented Feature Selection Crosstree Constraints(BOFS-CTC),to find all possible valid products by selecting the features according to cardinality constraints and cross-tree constraint problems in the featuremodel of SPL.BOFS-CTC removes the invalid products at the early stage of feature selection for the product configuration.Furthermore,this research developed the BOFS-CTC algorithm and applied it to,IoT-based feature models.The findings of this research are that no relationship constraints and CTC violations occur and drive the valid feature product configurations for the application development by removing the invalid product configurations.The accuracy of BOFS-CTC is measured by the integration sampling technique,where different valid product configurations are compared with the product configurations derived by BOFS-CTC and found 100%correct.Using BOFS-CTC eliminates the testing cost and development effort of invalid SPL products.

A Feature Model Based Framework for Refactoring Software Product Line Architecture

Software product line （SPL） is an approach used to develop a range of software products with a high degree of similarity. In this approach, a feature model is usually used to keep track of similarities and differences. Over time, as modifications are made to the SPL, inconsistencies with the feature model could arise. The first approach to dealing with these inconsistencies is refactoring. Refactoring consists of small steps which, when accumulated, may lead to large-scale changes in the SPL, resulting in features being added to or eliminated from the SPL. In this paper, we propose a framework for refactoring SPLs, which helps keep SPLs consistent with the feature model. After some introductory remarks, we describe a formal model for representing the feature model. We express various refactoring patterns applicable to the feature model and the SPL formally, and then introduce an algorithm for finding them in the SPL. In the end, we use a real-world case study of an SPL to illustrate the applicability of the framework introduced in the paper.

Feature-Oriented Nonfunctional Requirement Analysis for Software Product Line

Domain analysis in software product line （SPL） development provides a basis for core assets design and imple- mentation by a systematic and comprehensive commonality/variability analysis. In feature-oriented SPL methods, products of the domain analysis are domain feature models and corresponding feature decision models to facilitate application-oriented customization. As in requirement analysis for a single system, the domain analysis in the SPL development should con- sider both flmctional and nonfunctional domain requirements. However, the nonfunctional requirements （NFRs） are often neglected in the existing domain analysis methods. In this paper, we propose a context-based method of the NFR analysis for the SPL development. In the method, NFRs are materialized by connecting nonfunctional goals with real-world context, thus NFR elicitation and variability analysis can be performed by context analysis for the whole domain with the assistance of NFR templates and NFR graphs. After the variability analysis, our method integrates both functional and nonfunc- tional perspectives by incorporating the nonfunctional goals and operationalizations into an initial functional feature model. NFR-related constraints are also elicited and integrated. Finally, a decision model with both functional and nonfunctional perspectives is constructed to facilitate application-oriented feature model customization. A computer-aided grading system （CAGS） product line is employed to demonstrate the method throughout the paper.

A Product Line Approach to Design an Embedded Web System for Healthcare

With the recent advances in mobile technology and wireless network technology, embedded systems are being widely used in modem society today. Particularly, a home healthcare system is a networked embedded system where the main functions are to control the disease processes and to help patients maintain their independence and maximum level of function within their own homes and communities. It seems to be self-evident to design a system that would support both patients and their healthcare providers in the process of treatment. Nevertheless, little work in integrating embedded devices with intemet for the support of patients have been done to date. In this paper, we show how to design a healthcare system for supporting the management of the conditions of patients with chronic diseases. This system is built around wireless networked embedded devices, and integrates the intemet technology for telemonitoring the patient＇s health and notifying of doctors if emergency action is required. Also, patients themselves may specify personal alerts for condition-related issues.

Efficient software product-line model checking using induction and a SAT solver

Software product line （SPL） engineering is increasingly being adopted in safety-critical systems. It is highly desirable to rigorously show that these systems are designed correctly. However, formal analysis for SPLs is more difficult than for single systems because an SPL may contain a large number of individual systems. In this paper, we propose an efficient model-checking technique for SPLs using induction and a SAT （Boolean satisfiability problem） solver. We show how an induction-based verification method can be adapted to the SPLs, with the help of a SAT solver. To combat the state space explosion problem, a novel technique that exploits the distinguishing characteristics of SPLs, called feature cube enlargement, is proposed to reduce the verification efforts. The incremental SAT mechanism is applied to further improve the efficiency. The correctness of our technique is proved. Experimental results show dramatic improvement of our technique over the existing binary decision diagram （BDD）-based techniques.

STPSO: Optimal Configuration for Cloud Environments

With the increasing number of resources provided by cloud environments, identifying which types of resources should be rent when deploying an application is often a difficult and error-prone process. Currently, most cloud environments offer a wide range of configurable resources, which can be combined in many different ways. Finding an appropriate configuration under cost constraints while meeting requirements is still a challenge. In this paper, software product line engineering is introduced to describe cloud environments, and configurable resources are abstracted as features with attributes. Then, a Self-Tuning Particle Swarm Optimization approach(called STPSO) is proposed to configure the cloud environment. STPSO can automatically adjust the arbitrary configuration to a valid configuration. To evaluate the performance of the proposed approach, we conduct a series of comprehensive experiments. The empirical experiment shows that our approach reduces time and provides a reliable way to find a correct and suitable cloud configuration when dealing with a significant number of resources.

Maintain Optimal Configurations for Large Configurable Systems Using Multi-Objective Optimization

To improve the maintenance and quality of software product lines,efficient configurations techniques have been proposed.Nevertheless,due to the complexity of derived and configured products in a product line,the configuration process of the software product line(SPL)becomes timeconsuming and costly.Each product line consists of a various number of feature models that need to be tested.The different approaches have been presented by Search-based software engineering(SBSE)to resolve the software engineering issues into computational solutions using some metaheuristic approach.Hence,multiobjective evolutionary algorithms help to optimize the configuration process of SPL.In this paper,different multi-objective Evolutionary Algorithms like Non-Dominated Sorting Genetic algorithms II(NSGA-II)and NSGA-III and Indicator based Evolutionary Algorithm(IBEA)are applied to different feature models to generate optimal results for large configurable.The proposed approach is also used to generate the optimized test suites with the help of different multi-objective Evolutionary Algorithms(MOEAs).

VARIABILITY MODELING TO DEVELOP FLEXIBLE SERVICE-ORIENTED APPLICATIONS

To cope with requirement changes flexibly and rapidly,the existing component-based paradigm is being evolved into a service-oriented computing paradigm.The main characteristic of the service-oriented computing paradigm is that service-oriented applications are developed as loosely coupled services that reflect business concerns.This paradigm also promotes business agility,facilitating quick reactions to business changes.Therefore,to enhance and support the benefits of the service-oriented computing paradigm,we must consider how to improve flexibility and reusability during the development of service-oriented applications.We propose the variability modeling approach to specify and control the common and distinguishing characteristics of service-oriented applications.That is,the key concepts of product-line technology can be used to make service-oriented applications more flexible and reusable.This paper describes variability modeling at two levels;the composition level and the specification level.At the composition level,we describe the variability of composition and the flow of domain services that fulfill business processes.At the specification level,we present a domain service that is an abstract service with variability.The use of our systematic variability modeling approach can greatly increase the flexibility,applicability,and reusability of service-oriented applications.