自适应软件系统的建模与验证

摘要

自适应软件系统能够根据自身需求和环境的变化自动改变自己的行为。此时，在软件运行时，运行环境的变化将产生新的需求，而传统软件模型是对固定的需求进行建模，因此它无法适应这些新的需求。我们必须对自适应软件建立新的模型，它们能够适应实时产生的新需求。此外，由于环境的连续性和不确定性，这类模型刻画的是不定的、无限的状态，因此在建立自适应软件模型后，还需要对模型进行准确性和性质的验证。
　　本文主要研究了两类自适应软件系统的建模与验证。第一类是基于控制理论的自适应软件系统，主要研究了两类行为的切换系统：切换模糊系统和切换随机系统。切换模糊系统由全局切换规则、局部模糊规则和常微分方程组构成；首先对模糊系统去模糊化，然后用混合自动机对其建模，最后通过 PHAVer计算可达状态空间来分析系统的稳定性。切换随机系统包括由 Markov链描述的切换规则和由随机微分方程描述的子系统；本文提出了一种新的Petri网——随机微分Petri网对系统的离散切换行为、连续和随机行为进行建模；然后通过等价类的划分，化无限可达状态为有限Markov行为，最后利用PRISM进行验证。第二类是环境感知的自适应软件系统。对此，本文提出了一种新的建模语言——自适应Petri网来对其进行建模，并分析了模型的自适应性。自适应Petri网是混合Petri网的扩展，在其中嵌入了神经网络，用来对环境的变化做出决策。自适应Petri网具有如下一些优点：对运行环境进行建模、不同组件通过合作来完成决策过程、通过神经网络的局部计算达到全局的自适应行为。最后，通过一个制造系统的例子给出了自适应Petri网的应用。
　　本文主要进行了如下四个方面的工作：
　　1）提出了对具有模糊行为的自适应系统——切换模糊系统的形式化建模方法和系统稳定性的验证技术，从而避免传统方法中寻找Lyapunov函数的困难；
　　2）提出了一种能同时描述离散、连续和随机行为的形式化建模语言，它可以对具有随机行为的自适应系统——切换随机系统进行建模和模型检查；
　　3）提出了一种对环境感知的自适应系统的建模语言——自适应 Petri网。它既能描述系统的行为，又能对运行环境进行建模，同时具有良好的可扩展性；
　　4）提出了对系统的可达状态构造等价类，通过等价类划分，化无限状态为有限行为，从而在一定程度上解决自适应模型在验证时产生的状态爆炸问题。

目录

封面

声明

中文摘要

英文摘要

目录

图 清 单

1 绪论

1.1 研究意义

1.2 国内外研究现状

1.3 本文研究内容

2 预备知识

2.1 Petri网

2.2 混合自动机

2.3 神经网络

3 第一类自适应软件系统的建模与验证

3.1 基于模糊行为的自适应系统——切换模糊系统的建模与分析

3.2 基于随机行为的自适应系统——切换随机系统的建模与分析

3.3 本章小结

4 第二类自适应软件系统的建模与验证

4.1 引例

4.2 引例分析——需要对哪些方面进行建模

4.3 自适应Petri 网的定义和语义

4.4 自适应Petri网的自适应性分析

4.5 本章小结

5 实例分析

5.1 第一类自适应系统的实例分析

5.2 第二类自适应系统的实例分析

5.3 本章小结

6 总结和展望

参考文献

附录A 文中编写的部分代码和数据

A1 文5.1.1节中模型验证时编写的主要PHAVer代码

A1.1 图5.3中所示仿射自动机的PHAVer描述

A1.2 计算图5.3中仿射自动机的可达状态的PHAVer代码

A1.3 由上述代码获得的部分可达图的表示

A2 文5.1.2节中模型验证时编写的主要PRISM代码

A2.1 Markov链切换控制的PRISM描述

A2.2 off子系统的PRISM描述

A2.3 on模式的PRISM描述

A2.4 几个验证形式

A3 文5.2节中自适应Petri网中的神经网络的训练数据和结果

A3.1 神经网络NN1和NN2的训练样本数据

A3.2 神经网络的训练结果

攻读硕士期间的研究成果

致谢