# Timed-SAS: Modeling and Analyzing the Time Behaviors of Self-Adaptive Software under Uncertainty
## 1 Introduction  
Nowadays, complex software systems such as the cloud computing systems [1] and the cyber-physical systems [2] are facing new challenges due to increasing size, incremental complexity, and unpredictable environment changes. While addressing these challenges, it becomes necessary to develop self-adaptive software (SAS) [3]. In fact, software self-adaptation has become a research hot topic [4, 5] in the software engineering community. Self-adaptation endows a software system with the capability to satisfy certain objectives by automatically modifying its parameters, structures, or behaviors, with the commonly used MAPE-K (Monitor-Analyze-Plan-Execute, Knowledge) self-adaptation loops [6]. SAS systems run in dynamic and uncertainty environments, and it is necessary to provide rigorous evidence to guarantee that the self-adaptation processes, time behaviors, and properties are correct and satisfied through particular formal models, such as the automaton model [7] and Petri-nets model [8], as discussed in \"_Assumances for Self-Adaptive Systems_\" [9]. The network of timed automata (NTA) seems to be a promising formal model to specify system behaviors for the SAS systems, and many research studies, such as the ActivFORMS method [10], the MAPE-K formal templates [11], and the eARF reasoning framework [12], attempted to formally specify the SAS systems with the NTA model. However, there are still some deficiencies with the NTA-based approaches. Firstly, few studies systematically considered the time behaviors, especially the uncertainty delay time constraints within the self-adaptation loops. The MAPE-K self-adaptation loops can effectively handle dynamic changes within the software systems, but they bring in additional overhead time, such as the monitoring period of the monitor process, the analyzing and judging time of the analyze process, the uncertainty message processing time and network delay time of the self-adaptation loops, etc. The above time behaviors need to be explicitly and quantitatively described and analyzed. Second, to the best of our knowledge, there is a lack of time metrics to systematically evaluate the performance and the time properties of the self-adaptation loops. For example, the time used to return to normal and steady states, and the probabilities to return to normal states within a given time limit. Third, the NTA model suffers from problems such as state-space explosion during formal verification, when the system scale and complexity is large. In order to solve the above problems, this paper proposed the Timed-SAS approach, which was established based on the commonly used MAPE-K self-adaptive software architecture [6]. After a series of case studies and literature research, the deterministic and uncertainty time constraints, which are commonly used during the SAS system design and development processes, were identified, and summarized. Based on this, the Timed-SAS approach provides a set of definitions for the time constraints within each MAPE-K process, and a set of time-based evaluation metrics to evaluate the performance of the self-adaptation loops. To facilitate modeling and quantitative analysis of the above time constraints and time-based evaluation metrics, the Timed-SAS approach established a set of formal modeling templates based on the network of priced timed automata (NPTA) [13] model, and a set of quantitative analysis templates based on the statistical model checking (SMC) [14] formal verification technique. In general, the Timed-SAS approach can be used to define, describe, analyze, and optimize the time behaviors of the SAS systems, and the main contributions of the Timed-SAS approach are as follows:  
1. It proposes a set of systematic definitions on the time behaviors of the SAS systems, which can depict the deterministic time constraints, and the uncertainty time constraints within the self-adaptation processes. In addition, it provides a set of quantitative analysis metrics to evaluate the performance and the response-time of the self-adaptation loops;
2.