EasyModel: A Refinement-Based Modeling and Verification Approach for Self-Adaptive Software
- PDF / 3,536,962 Bytes
- 31 Pages / 595 x 842 pts (A4) Page_size
- 84 Downloads / 208 Views
EasyModel: A Refinement-Based Modeling and Verification Approach for Self-Adaptive Software De-Shuai Han1 , Qi-Liang Yang2,∗ , Jian-Chun Xing2 , and Guang-Lian Ma1,3 1
College of Combat Support, Rocket Force University of Engineering, Xi’an 710025, China
2
College of Defense Engineering, Army Engineering University of PLA, Nanjing 210007, China
3
Teaching and Research Support Center, Rocket Force University of Engineering, Xi’an 710025, China
E-mail: [email protected]; {yql, xjc}@893.com.cn; [email protected] Received April 6, 2020; revised July 25, 2020. Abstract Self-adaptive software (SAS) is gaining popularity as it can reconfigure itself in response to the dynamic changes in the operational context or itself. However, early modeling and formal analysis of SAS systems becomes increasingly difficult, as the system scale and complexity is rapidly increasing. To tackle the modeling difficulty of SAS systems, we present a refinement-based modeling and verification approach called EasyModel. EasyModel integrates the intuitive Unified Modeling Language (UML) model with the stepwise refinement Event-B model. Concretely, EasyModel: 1) creates a UML profile called AdaptML that provides an explicit description of SAS characteristics, 2) proposes a refinement modeling mechanism for SAS systems that can deal with system modeling complexity, 3) offers a model transformation approach and bridges the gap between the design model and the formal model of SAS systems, and 4) provides an efficient way to verify and guarantee the correct behaviour of SAS systems. To validate EasyModel, we present an example application and a subject-based experiment. The results demonstrate that EasyModel can effectively reduce the modeling and formal verification difficulty of SAS systems, and can incorporate the intuitive merit of UML and the correct-by-construction merit of Event-B. Keywords
1
self-adaptive software, formal modeling, Event-B, refinement, correct-by-construction
Introduction
Modern software systems, such as large-scale web service systems and cyber-physical systems, are facing problems of increasing size, incremental complexity and unpredictable environment changes. While addressing the above challenges, it becomes necessary to develop so-called self-adaptive software (SAS) systems. In fact, software self-adaptation has become a hot research issue [1–3] in the software engineering community. Software self-adaptation endows a software system with the capability to to reconfigure itself in response to the dynamic changes in the running context. The early design, modeling and formal analysis of SAS systems is essential to improve development efficiency and to ensure system reliability. As a stan-
dardized object oriented modeling language, Unified Modeling Language (UML) has been widely used to depict SAS systems. The self-adaptive software community has proposed ACML (Adapt Case Modeling Language) [4] to specify SAS requirements, the FAME approach [5] to depict self-adaptation attributes, and the design patterns [6] to
Data Loading...
