中文摘要：

大规模集成电路工艺技术的飞跃发展,掀起了计算机快速发展广泛普及的浪潮,同时又向计算机网络、巨型计算机、智能化方向以及分布式实时处理方向发展.其中,分布式实时系统的需求在各个领域的需求都不断扩大,于是,分布式实时操作系统也随之产生.为了保证设计的可靠性和正确性,通过模型检测的方法对分布式实时操作系统的任务调度建立马尔科夫决策过程（MDP）模型,并以机器人分布式实时操作系统为例,用概率计算树逻辑（PCTL）对一些关键属性进行描述,通过PRISM平台对任务的可调度性进行验证和分析.通过将验证和分析得到的量化结果不断反馈给设计人员,以反馈得到的结果为依据,设计人员可以作出相应的策略,进一步提高设计的可靠性和正确性.

英文摘要：

The rapid development of large scale integrate circuit technology,sets off the w ave of the fast development and extensive popularization of computers. M eanw hile,it also progresses tow ards computer netw orks,supercomputers,intelligent and distributed realtime domains. Whereby,the demand of the distributed real-time systems is constantly expanding in all fields,so distributed real-time operating system comes into being naturally. In order to guarantee the reliability and correctness of the design,this paper harnesses probabilistic model checking to build M DP（ M arkov Decision Process） model of tasks scheduling for distributed real-time operating system. M eanw hile this paper takes the robots＇ distributed real-time operating system as an example,and describes some critical properties in PCTL（ Probabilistic Computation Tree Logic）,then the tasks＇ schedulability is verified and analyzed by the PRISM. Feedback the quantified results to the designers constantly,the designers can take some corresponding measures based on the messages to improve the dependability and validity further.