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

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