Efficient validation of self-adaptive applications by counterexample probability maximization

Self-adaptive applications' executions can be affected by uncertainty factors like unreliable sensing and flawed adaptation and therefore often error-prone. Existing methods can verify the applications suffering uncertainty and report counterexamples. However, such verification results can deviate from reality when the uncertainty specification used in verification is itself imprecise. This thus calls for further validation of reported counterexamples. One outstanding challenge in counterexample validation is that the probabilities of counterexamples occurring in real environment are usually very low, which makes the validation extremely inefficient. In this paper, we propose a novel approach to systematically deriving path-equivalent counterexamples with respect to original ones. The derived counterexamples guarantee to have higher probabilities, making them capable of being validated efficiently in field test. We evaluated our approach with real-world self-adaptive applications. The results reported that our approach significantly increased counterexample probabilities, and the derived counterexamples were also consistently and efficiently validated in both real environment and simulation.