一种逐步精化的自适应软件建模与验证方法
EasyModel: A Refinement-Based Modeling and Verification Approach for Self-Adaptive Software
-
摘要: 1、研究背景（context）：近年来，随着软件规模和复杂程度的不断增加、软件运行环境和用户需求的频繁变化，导致对软件自适应的需求愈加强烈。自适应软件能够在运行时通过对自身结构和行为进行调整，及时应对运行环境、用户需求及软件自身发生的变化。在开发初期对自适应软件进行建模设计和形式化验证能够提高其可靠性、降低开发成本。然而，现有研究工作难以有效应对自适应软件复杂程度高、验证困难等问题。
2、目的（Objective）：本文旨在对自适应软件的建模设计、模型转换与形式化验证问题展开研究，实现自适应软件结构特征、自适应行为特性、自适应环等要素的显式建模，并在建模过程中分解系统复杂度、降低建模难度，在此基础上对自适应行为、自适应逻辑、自适应策略等性质进行高效分析与验证，提高自适应软件可靠性。
3、方法（Method）：本文提出一种逐步精化的自适应软件建模与验证方法（简称EasyModel方法）。首先，通过扩展UML构造Adapt Profile方法和工具，实现自适应软件结构特征和行为特性的显式建模；其次，研究一种模型转换方法和工具，将自适应软件扩展UML模型转换为Event-B模型，填补自适应软件设计模型和形式化模型之间的鸿沟；然后，定义并证明一组Event-B精化模式，实现复杂自适应逻辑的逐步精化建模；最后，研究一种模型检验与定理证明相结合的自适应性质分析与验证方法，提高自适应软件可靠性。
4、结果（Result&Findings）：案例应用和实验评估表明，本文提出的EasyModel方法能够有效处理自适应软件复杂程度高、分析验证困难等问题。同时，综合评估自适应特性显式描述、自适应软件复杂性处理、自适应软件可靠性验证等建模指标，EasyModel方法要优于同类方法。
5、结论（Conclusions）：论文提出的EasyModel方法汲取了UML直观易理解和Event-B逐步精化、构造即正确的优点，能够有效处理自适应软件复杂程度高、分析验证困难等问题。上述可视化UML与逐步精化的Event-B相结合的思想也可为信息物理融合系统、大型Web服务系统等复杂软件系统的建模与设计提供借鉴。
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.
下载: