论文部分内容阅读
功能正确和性能可满足是复杂系统可信要求非常重要的两个方面。从定性验证和定量分析相结合的角度,对复杂并发系统进行功能验证和性能分析,统一地评估系统是否可信。连续时间Markov决策过程CTMDP（Continu-ous-time Markov decision process）能够统一刻画复杂系统的概率选择、随机时间及不确定性等重要特征。提出用CT-MDP作为系统定性验证和定量分析模型,将复杂系统的功能验证和性能分析转化为CTMDP中的可达概率求解,并证明验证过程的正确性,最终借助模型检测器MRMC（Mar