Abstract: 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.

Key words: Function and performance, Continuous time Markov decision process, Model checking, hrusted verification,Reachabihty probabilities