摘要：CAN总线是一种基于消息的事件触发通信服务,主要应用于汽车、机器人等实时通信系统.CAN总线上有多个节点互相独立工作,当多个节点访问总线时出现消息碰撞,由于CAN总线采用按位仲裁算法决定节点访问总线的优先级,导致低优先级节点访问失败,而高优先级节点继续传输消息,这种方式导致低优先级节点饥饿现象而丢失消息,因此CAN总线调度算法随之被提出.目前调度策略已从静态发展到动态,但是随着节点的增多,系统维护和调度难度增加,单条总线调度策略难以维持系统性能需要.因此本文考虑将系统中的节点挂载到多条CAN总线上构成CAN网络,针对CAN网络提出了一种层次化的动态调度算法,将节点优先级仲裁分为:单条总线本地优先级仲裁和系统全局优先级仲裁,确定系统优先级最高的节点,使其进行数据传输.利用MATLAB中的Stateflow工具,建立分层动态调度模型,依据CAN总线数据传输机制和仲裁机制,设计实现了节点模块、总线模块、函数模块等,在总线模块实现了两级调度.实验结果表明,本算法在增加了节点总数目的基础上,满足高优先级节点传输且避免了低优先级节点的饿死现象.

摘要：SpaceWire是应用于航空航天领域的高速通信总线标准,保证其设计的可靠性和正确性至关重要.本文通过概率模型检测的方法对SpaceWire的交换层设计进行形式化建模与量化分析.基于马尔科夫决策过程(MDP)对交换层的链路初始化及正常运行过程建立形式化概率模型,模型包括发送方、接收方和信道,提取SpaceWire交换层的4个关键属性,用概率计算树逻辑(PCTL)进行描述,运用PRISM平台对SpaceWire交换层设计进行验证和分析;并获得信道丢包概率不同情况下,链路初始化成功以及正常运行时数据包正确传输的概率,这种定量形式化分析结果可为SpaceWire的设计和实现提供参考依据.

摘要：作为一种开源的机器人操作系统,ROS在家用或服务性机器人上也得到广泛应用,保证其设计的正确性相当重要.本文通过定理证明的方法对ROS的节点间通信进行形式化建模与属性验证.对通信层的节点间连接建立和消息传递过程进行抽象建模,模型融合网络拓扑、主题匹配和路由机制等部分,定义函数对其进行描述,提取路由函数的存在性、可达性及正确性等3个关键属性,运用定理证明工具ACL2对ROS节点间通信的功能正确性进行自动验证,证明消息从源节点出发并选择有效的传输路径到达目的节点.这种满足属性要求的参数化模型具有一般性和易扩展性,并能保证ROS节点间通信的终止属性和功能正确性,可为ROS通信层设计的正确性验证工作提供一个有效的方法参考.

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