Verification And Counterexample Validation For Self-adaptive Software Systems Suffering Uncertain Environmental Interactions

The execution environments for modern software systems with increasing scales are becoming more and more diverse.They are no longer limited to the traditional computer platform,but shift to a more open,dynamic and complex environment,such as the network and physical environments.Under these new environments,software systems need to conduct effective interactions with the environments.To meet this requirement,researchers proposed self-adaptive software systems to make the software artifact capable of responding to the environmental changes by changing its behavior patterns.However,because of the complexity of the system itself and the uncertainty in the interaction between the system and environment,the self-adaptive software system is often error-prone.As a common quality assurance technology,verification can find some hidden subtle system errors.However,when it comes to verifying self-adaptive software systems,existing work overlooked the interaction uncertainty between the system and environment caused by factors such as unreliable sensing,and thus may report many false positives or false negatives.Therefore,in order to obtain accurate verification results,it is necessary to explicitly model the interaction uncertainty.Nevertheless,it can be difficult to model interaction uncertainty precisely enough in the beginning,because of the uncontrollable noise of sensors and insufficient data sample size.Verification results based on the imprecise models may also be inaccurate,and thus need to be further validated.If the uncertainty model is confirmed to be imprecise,calibration is necessary to obtain more accurate verification results.However,problems like how to verify the self-adaptive software system accurately by modeling the interaction uncertainty,how to efficiently validate the inaccurate verification results due to the use of imprecise models,and how to calibrate the imprecise uncertainty models used in the verification have not been well resolved by existing pieces of work.To address these problems,we present a series of approaches to verifying self-adaptive software systems suffering uncertainty to obtain accurate verification results,and the major work presented in this article is as follows:1.We propose an approach to verifying self-adaptive software systems suffering uncertainty.Interactive State Machine and Interactive State Machine Network are proposed for self-adaptive software systems to intuitively and concisely model their "monitoring-analyzing-planning-executing" behavior.For the modeling of interaction uncertainty between the self-adaptive software system and environment,error ranges and distributions are proposed,and for the modeling of effect of system's adaptation on the environment,environmental constraints are proposed.By encoding the above models as SMT formula,our approach can effectively verify whether the system will fail or not,and provide counterexamples depicting failing behavior.By considering interaction uncertainty and effects of system's adaptation on the environment,the issue of having numerous false positives and false negatives in existing verification work has been well resolved,resulting in the accuracy of verification results being significantly improved.2.We propose an approach to accelerating the process of validating counterexamples by counterexample probability maximization.The verification results can deviate from reality because of the imprecise models used in verification,and this stresses the need for further validation of counterexample in actual environment.Since the validation cost can be excessively high due to the counterexample's low probability of occurrence,this approach proposes to accelerating counterexample validation by finding the path-equivalent counterexample of highest probability that shares the same path as the original one.By formulating counterexample's probability function and inputs' value constraints,the above problem of finding path-equivalent counterexample is transformed into a constrained optimization problem.Meanwhile,multiple techniques such as optimization problem separation and indicator function elimination are proposed to simplify the problem,and a customized genetic algorithm is employed to solve the problem.By accelerating the validation process,the cost of validation is significantly reduced.3.We propose an approach to calibrating the imprecise uncertainty models by leveraging the differences between counterexamples' calculated probabilities and actual probabilities.The inaccurate counterexamples caused by imprecise uncertainty models can demonstrate a deviation between their calculated and actual probabilities in the validation.Our approach innovatively proposes to use this deviation to calibrate the uncertainty models.By using the differences between counterexamples' calculated probabilities and actual probabilities as the fitness function,the calibration problem of imprecise uncertainty models is transformed to a Search-Based Software Engineering problem,and a genetic algorithm is employed to search for the uncertainty models minimizing the fitness function.Meanwhile,hypothesis testing is used to help decide whether the calibrated uncertainty models are precise enough.This technique can effectively improve the precision degrees of existing uncertainty models,and thus improve the accuracy of verification results in turn.These approaches complement each other.First,by modeling interaction uncertainty,the verification approach can well resolve the issue of having numerous false positives and false negatives in existing verification work;Second,the validation approach can efficiently validate counterexamples obtained from verification,which can further reduce false positives and identify the possible imprecision of the uncertainty models;Last,for imprecise uncertainty models,calibration approach can calibrate them by using the experimental data from counterexample validation.The calibrated models can be used for future verification to obtain more accurate verification results.The three approaches form an iterative verification process,and together contribute to the improvement of verification accuracy of self-adaptive software systems.