A survey of formal methods in self-adaptive systems

One major challenge in self-adaptive systems is to assure the re-quired quality properties. Formal methods provide the means to rigorously specify and reason about the behaviors of self-adaptive systems, both at design time and runtime. To the best of our knowl-edge, no systematic study has been performed on the use of formal methods in self-adaptive systems. As a result, there is no clear view on what methods have been used to verify self-adaptive sys-tems, and what support these methods offer to software develop-ers. As such insight is important for researchers and engineers, we performed a systematic literature review covering 12 main soft-ware engineering venues and 4 journals, resulting in 75 papers used for data collection. The study shows that the attention for self-adaptive software systems is gradually increasing, but the number of studies that employ formal methods remains low. The main fo-cus of formalization is on modeling and reasoning. Model check-ing and theorem proving have gained limited attention. The main concerns of interest in formalization of self-adaptation are effi-ciency/performance and reliability. Important adaptation concerns, such as security and scalability, are hardly considered. To verify the concerns of interest, a set of new properties are defined, such as in-terference freedom, responsiveness, mismatch, and loss-tolerance. A relevant part of the studies use formal methods at runtime, but the use is limited to modeling and analysis. Formal methods can be applied to other runtime activities of self-adaptation, and there is a need for light-weight tools to support runtime verification.