# Timed-SAS: Modeling and Analyzing the Time Behaviors of Self-Adaptive Software under Uncertainty
## 6 Related Work and Discussion  
Recently, the study on the SAS systems has become a hot topic in the software engineering community. Particularly, formal methods for the SAS systems are attracting increasing interest. The self-adaptive software community has made several comprehensive surveys [28; 29; 30], focusing on modeling dimensions, engineering approaches and formal methods of self-adaptive systems, respectively. This study focuses on formal modeling and analysis of the self-adaptation processes and the time behaviors for the SAS systems, and we review studies that are relevant to our Timed-SAS approach. **Formal modeling and verification on the self-adaptation processes. ** In order to formally describe and verify the self-adaptation processes, researchers have proposed many approaches, such as the CSP-based approaches [31; 32], the Petri-Net based approaches [33; 34], the NTA-based approaches [10; 11; 12], the Event-B based approaches [18; 21; 35], the approaches based on domain specific language [36; 37], etc. One popular approach is the NTA-based approach, owing to its simplicity and ease-of-use features. On basis of the timed automata model, the AdaptWise research group of Linnaeus University proposed the ActivFORMS approach [10], the MAPE-K formal templates [11], and the eARF approach [12] for the SAS systems. The above research concentrates on formal modeling and verification of the dynamic self-adaptation processes, but they lack a systematic definition and description on the time behaviors within the SAS systems. In addition, model checking of the above formal models encounters the problem of state-space explosion when system scales increase. By contrast, our Timed-SAS approach provides a systematic definition on the time behaviors within the SAS systems and supports formal modeling and quantitative analysis of the dynamic self-adaptation processes as well as the time behaviors. Furthermore, the Timed-SAS approach can avoid the state-space explosion problem with the Statistical Model Checking technique. **Formal modeling and verification on the time behaviors of the SAS systems. ** Time behavior is an important characteristic for the self-adaptive systems. [PERSON] and [PERSON] [38] have long pointed out the need to specify the adaptation requirements with temporal logic. Furthermore, they have proposed the Adapt operator-extended LTL (ALTL) [39] to specify adaptation semantics. Similarly, [PERSON] et al. [40] have proposed the mode-supported Linear Temporal Logic (mLTL) to specially describe global specifications of the self-adaptive software. The above studies have treated time behaviors as first-class elements to handle, but they lack a systematic definition on the time behaviors within the SAS systems. As for definitions on the time behaviors, the authors in [18] defined the time behaviors of deadline, delay, and expiry for the self-adaptive systems. On the basis of these definitions, the authors proposed to extend the Event-B model with timing semantics, and defined the refinement patterns for deadline, delay and expiry, which can reduce modeling difficulties of time behaviors. Unfortunately, the above modeling patterns cannot describe the time behaviors under uncertainty environment. Apart from definitions on the deterministic time behaviors, we have defined the uncertainty time behaviors to describe the delay time under uncertainty environment. **Quantitative analysis on the SAS systems. ** In order to quantitatively analyze the system behaviors under uncertainty, the researchers have proposed the Probabilistic Model Checking based approaches [41; 42; 43; 44] for the SAS systems. These approaches possess the advantages of automatic analysis and quantitative verification and can avoid the state-space explosion problem of model checking. However, there is still a lack of quantitative metrics to evaluate the self-adaptation logic [45].