面向数据流的ROS2数据分发服务形式建模与分析

机器人操作系统(robot operating system,简称ROS)是一种开源的元操作系统,能够在异种计算簇上提供基于消息机制的结构化通信层.为改善ROS1中存在的数据分发实时性、可靠性问题,ROS2提出了面向数据流的数据分发服务机制.采用概率模型检验的方法,分析、验证ROS2系统数据分发机制的实时性和可靠性.首先,提出一种面向数据流的ROS2数据分发服务的形式化验证框架,并对通信系统模块建立概率时间自动机模型;其次,运用概率模型检测器,通过数据丢失率和系统响应时间等参数分析、验证ROS2面向数据流的数据分发服务的实时性、可靠性;最后,基于重传机制、服务质量(quality of service,简称QoS)策略分析,通过设置和调整服务质量参数,实现不同的数据需求和传输方式的量化性能分析,为ROS2应用的设计人员以及基于数据流的分布式数据分发服务的形式化建模、验证和量化性能分析提供参考.

一种基于Petri网的安全协议验证方法

安全协议是实现网络安全的关键,如何验证安全协议的安全性是一个非常重要的工作。论文提出一种基于着色Petri网的安全协议形式化描述与安全验证方法,此方法建立在逆向状态分析和着色petri网可达性矩阵的基础之上,并采用具体协议来验证该方法的有效性。