动态环境下自适应软件系统的建模与验证技术研究

The execution environments for modern software systems are increasingly open and dynamic. Under these new environments, software systems need to be able to sense and adapt to environmental changes. To meet this requirement, researchers proposed self-adaptive software systems. Since they were put forward, self-adaptive software systems have attracted much attention and been widely applied. However, because of the complexity of the system itself and the affection of uncertainty, the self-adaptive software system is often error-prone. As a common quality assurance technology, verification can find hidden subtle system errors. However, when it comes to modeling self-adaptive software systems, most existing work adopted static rules to describe the adaptation logics that can actually be complicated and flexible, and only explored the possible behavior of the system in one or several specific static environments and overlooked the uncertainty in verifying self-adaptive software systems. This results in incomplete and inaccurate verification results. Through the research on the modeling of self-adaptive software systems' adaptation logics with Markov Decision Processes, the description for dynamic environments, the dealing of uncertainty and verification of self-adaptive software system models, this project intends to achieve flexible modeling of adaptation logics, and efficient verification of self-adaptive software system with more complete and accurate results, thus providing a theoretical reference and technical support for the quality assurance of self-adaptive software systems.

现代软件系统的运行环境越来越开放与动态。面对这些新环境，软件系统需能感知并适应环境的变化。为此，研究者提出了自适应软件系统。自提出以来，自适应软件系统就备受关注，应用也越来越广泛。然而，由于自适应软件系统自身的复杂性以及不确定性的影响，自适应软件系统常易出错。作为一种常见的质量保障技术，验证可以发现软件系统一些隐藏的错误。但现有工作在建模自适应软件系统时大多采用静态规则式的描述方法，难以满足当前复杂灵活的自适应逻辑描述需求，而且在验证时都只考虑系统在某一或某些特定静态环境下可能的行为，没有考虑到系统在动态环境下可能的行为及不确定的影响，导致验证结果不够完整与准确。本项目拟通过基于马尔可夫决策过程的自适应逻辑建模，动态环境的刻画、不确定性的处理和自适应软件系统的验证等方面的研究，实现自适应软件系统灵活的自适应逻辑建模与高效和准确的验证，从而为自适应软件系统的质量保障提供理论参考和技术支持。

为了解决自适应软件系统验证过程中存在的适应逻辑建模难、动态环境刻画难、不确定性处理难和融合验证难等问题，本项目通过对自适应软件系统的适应逻辑的建模方法、不确定性的处理和自适应软件系统的融合验证技术等内容的深入研究，详细分析了自适应软件系统中不确定性的分类，并基于马尔可夫决策过程提出了一种面向动态环境变化与不确定性的自适应软件系统建模与验证方法，从而为自适应软件系统的正确性保障提供理论参考和技术支持。具体而言，根据自适应软件系统中被广泛认可的技术架构对不确定性进行了分类，详细介绍了该架构每一层次上可能存在的不确定性，并结合典型的自适应软件系统应用进行了举例说明；我们采用马尔可夫决策过程建模了自适应软件系统的适应逻辑，并进一步采用了概率模型检验技术验证了系统的行为的正确性；最后，我们创新地提出了使用部分可观察的马尔可夫决策过程对动态环境下的自适应软件系统进一步建模，从而可以对常见类型的环境变化以及不确定性进行建模，基于该模型还可以生成控制自适应软件系统的策略。