Abstract:Self-Adaptive systems (SASs) are required to be capable of adjusting their behaviors in response to changes in operational contexts and themselves. To implement automatic adjustment, SASs must be endowed by abilities of monitoring changes in contexts and themselves, analyzing changes of requirement satisfaction and reasoning about adaptation decisions. The behavior of online decision-making needs to assure functional requirements as well as certain non-functional requirements such as reliability and performance. This paper proposes a verification-based optimal decision-making approach for SASs, for assuring the satisfaction of non-functional requirements. This approach models adaptation mechanisms by identifying adjustable goals and maps goal models to corresponding behavior models expressed by label transition systems. It takes reliability requirements as examples and utilizes tagged goal models to specify reliability of tasks. Then, the system behavior model and reliability specifications are integrated into discrete-time Markov chains with variable states while adaptation candidates are characterized by combinations of different variable states. Via online verification of related requirements, the system derives the optimal decision of configurations under a certain type of contexts. The feasibility and effectiveness of the approach are illustrated through a mobile information system.