Submitted Abstract
Software systems are increasingly often made configurable in order to adapt to a variety of contexts, like new customer requirements or changing environmental conditions. Given an envisaged context, engineers have to build, deploy and run an appropriate variant of the system, so as to guarantee that intended requirements are/remain satisfied. To achieve this, they start a configuration process during which the configuration parameters (i.e. the variation points) of the system are set to specific values in order to form the desired variant. In many real-world cases (e.g. embedded systems), the assessment of variants w.r.t. intended requirements necessitate in-depth analyses of their behaviour. We designate such a case where behavioural analyses are required to carry on the configuration process by the term behaviour-induced configuration. This type of configuration suffers from three sources of complexity. First, the number of variants explodes as more variation points are added to the system, making the exhaustive analysis of all of them intractable. Second, due to the numerous functional and quality requirements to which today’s systems are typically confronted, the choice of which variant is the most appropriate becomes a multi-criteria decision-making process. Third, systems are typically deployed in stochastic environments that system engineers cannot completely anticipate or control. The ultimate objective of the BEEHIVE project is to provide engineers with theories, techniques and tools that support behaviour-induced configuration and address the three sources of complexity. To achieve this, we envision a behaviour-induced configuration process relying on smart sampling and statistical model checking to master the sources of complexity. From a variability model defining the set of valid variants, we sample some of those to undergo behavioural analysis. The behaviour of all variants is concisely represented in a single model (in the form of an automaton or state machine). Statistical model checking methods are used to simulate sampled behaviours of the selected variants, which are then assessed against given (functional and quality) requirements as well as against a cost function representing trade-offs between the quality attributes. In the end, the process identifies which variants satisfy the requirements and which, among those, optimize the quality attributes.