基于交互式马尔可夫链的模型检验

研究了基于交互式马尔可夫链（IMC)的模型检验，IMC是集功能描述和性能刻画为一体的并发系统模型，模型检验是一种自动功能验证与性能评价技术。文中提出的模型检验算法结合了传统的功能验证与性能评价的功能，并且与现有的算法相一致。实验分析表明，该算法具有较高的性能，适用于大型复杂系统的验证和评价。

Model checking interactive Markov chains

Model checking algorithm was investigated for Interactive Markov Chains (IMC). IMC is a concurrent system model, combining functional feature and performance properties. Model checking is one kind of automatic function confirmation and the performance evaluation technology. The presented algorithm is a combination of traditional function confirmation and performance evaluation, and which is in consistency with the original algorithm. Experimental results have shown the algorithm can achieve a good performance and can be used to evaluate for large and complex systems.