随机模型检测连续时间Markov过程

功能正确和性能可满足是复杂系统可信要求非常重要的两个方面。从定性验证和定量分析相结合的角度，对复杂并发系统进行功能验证和性能分析，统一地评估系统是否可信。连续时间Markov决策过程CTMDP(Continuous time Markov decision process)能够统一刻画复杂系统的概率选择、随机时间及不确定性等重要特征。提出用CTMDP作为系统定性验证和定量分析模型，将复杂系统的功能验证和性能分析转化为CTMDP中的可达概率求解，并证明验证过程的正确性，最终借助模型检测器MRMC(Markov Reward Model Chcckcr)实现模型检测。理论分析表明，提出的针对CI'MDP模型的验证需求是必要的，验证思路和方法具有可行性。

Stochastic Model Checking Continuous Time Markov Process

the trustworthiness of a dynamic system includes the correctness of function and the satisfiabihty of per-formance mainly. I}his paper proposed an approach to verify the function and performance of a system under consideralion integratedly. Continuous-time Markov decision process(CTMDP) is a model that contains some aspects such as probabilistic choice, stochastic timing and nondeterminacy, and it is the model by which we verify function properties and analyze performance properties uniformly. We can verify the functional and performance specifications by computing the rcachability probabilities in the product CI}MDP. We proved the correctness of our approach, and obtained our verification results by using model checker MRMC(Markov Reward Model Checker). The theoretical results show that model checking CTMDP model is necessary and the model checking approach is feasible.