交互式马尔可夫链(IMC)是一种功能与性能混合的并发系统模型,通过正交结合经典的进程代数模型和连续时间马尔可夫链(CTMC)模型,IMC提供了一个完美的可组合化的性能评价框架。本文主要研究了IMC的理论及其在性能评价与层次化分析方面的应用,主要包括以下三方面的内容:1. IMC上的分支时间等价和前序关系。本文将经典的并发系统功能模型上的强(互)模拟和弱(互)模拟与性能模型上的强(互)模拟和弱(互)模拟概念在一个统一的框架下进行了定义,同时以基于动作的连续随机逻辑aCSL为基础研究了这些分支时间等价和前序关系的逻辑特征,即它们与逻辑等价性之间的联系。通过研究这些等价关系之间的相互联系,我们得到了一个IMC上的分支时间等价关系谱,它基本上包含了功能模型和性能模型上相关研究的结果。2.基于IMC的模型检验。IMC的主要目的是提供一个可组合化的性能评价模型,因此本文研究了IMC上的模型检验算法,以提供一种大规模复杂系统的自动高效的性能评价手段。本文采用aCSL作为性质描述语言,提出了一个完全基于动作的模型检验算法,从而可以充分利用IMC强大的组合建模能力,达到对复杂系统进行自动性能评价的目的。本文提出的算法是纯性能模型CTMC上的模型检验算法的一个推广,并且与原有的算法相一致,当IMC退化成为一个CTMC时,我们的算法也退化成CTMC上的模型检验算法。作为试验,我们同时将该算法用C语言实现了一个原型,并演示了如何应用IMC上的模型检验来对基于动作的系统进行自动性能评价。