基于PRISM的分布式实时操作系统任务调度的形式化验证  

Formal Verification of Distributed Real-time Operating System Task Scheduling Based on PRISM

作　　者：霍燕燕[1] 关永[1] 李晓娟[1] 王瑞[1] 张杰[2] 魏洪兴[3] 

机构地区：[1]高可靠嵌入式系统技术北京市工程研究中心电子系统可靠性技术北京市重点实验室,首都师范大学信息工程学院,北京100048 [2]北京化工大学信息科学与技术学院,北京100029 [3]北京航空航天大学机械工程及自动化学院,北京100191

出　　处：《小型微型计算机系统》2015年第9期2125-2129,共5页Journal of Chinese Computer Systems

基　　金：国际科技合作计划项目(2011DFG13000,2010DFB10930)资助;国家自然科学基金项目(61373034,61303014)资助;北京市教委科研基地建设项目(TJSHG201310028014)资助;北京市教委(KM201510028015)资助;北京市属高等学校创新团队建设与教师职业发展计划项目(IDHT20150507)资助

摘　　要：大规模集成电路工艺技术的飞跃发展,掀起了计算机快速发展广泛普及的浪潮,同时又向计算机网络、巨型计算机、智能化方向以及分布式实时处理方向发展.其中,分布式实时系统的需求在各个领域的需求都不断扩大,于是,分布式实时操作系统也随之产生.为了保证设计的可靠性和正确性,通过模型检测的方法对分布式实时操作系统的任务调度建立马尔科夫决策过程(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.

关 键 词：分布式实时操作系统 任务调度 概率模型检测 马尔科夫决策过程 PRISM 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]