Leveraging Bigraphical Reactive Systems for Formally Analyzing Context-dependent Properties and Behaviour of Interdependent Heterogenous Models
In the field of software technology there are multiple approaches in use for analyzing models and verifying certain model properties. An interesting challenge is the analysis of heterogenous models, e.g., the analysis of a feature model describing a variability space of software products and a UML-class diagram describing the design of the software. Existing solutions are aiming towards heterogenous models, but are limited to the analysis of specific combinations of heterogenous models, e.g., to the combination of feature models and UML class diagrams. In this work a new approach is developed and presented that is not limited to analyzing specific combinations, but is open for analyzing combinations of arbitrary heterogenous models and that can be easily extended to support new types of models. The approach draws its oppenness from the usage of bigraphs as an uniform intermediate representation for various types of models. The bigraph-formalism is designed around the abstract concepts of locality and connectivity and does therefore allow for representing a wide range of different types of models. Moreover, by defining bigraphical-reactive-systems the semantics of various model types can be described, including non-deterministic behaviour. Due to both properties, using bigraphs it is possible to describe structure and behaviour of various types of models. This renders bigraphs to be the foundation for the verification of diverse properties of combinations of arbitrary heterogenous models using model checking. The approach is evaluated by applying it for analyzing context-dependent feature models. An association of context conditions and feature models is formally described and certain feature defects (e.g., „false-optional features“) can be detected in the feature model associated to the respective context condition. Moreover, it is shown in the evaluation that it is possible to analyze the various products of a software product line for negative feature interactions, using this approach. This analysis requires the support of several different model types, as the solution space is assumed to be modeled as a class diagram the behaviour of whose functions is described using petrinets. So, the approach analyses the petrinets belonging to a common product for negative feature interactions, e.g., an act of setting an external component to a configuration that is not suitable for another feature. Finally, it is shown in the evaluation that the approach can be used easily for analyzing various runtime products of a dynamic software product line (DSPL), whose order of occurence is constrained (1) by a deterministic- and (2) by a non-deterministic feature transition system.