Formal probabilistic refinement verification of embedded real-time systems

Generally, real-time systems have been specified using timed automata, and moreover model-checking methods of timed automata have been developed. On the other hand, recently, probabilistic timed automata have been developed in order to express the relative likelihood of the system exhibiting certain behavior. In this paper, we develop a verification method of the simulation relation of probabilistic timed automata, and apply this method into stepwise refinement developments of real-time systems.