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 i...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 Easy Model.Easy Model 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-const ruction merit of Event-B.展开更多
基金supported by the National Key Research and Development Program of China under Grant No.2017YFC0704100.
文摘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 Easy Model.Easy Model 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-const ruction merit of Event-B.
