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