基于ROS通信机制的形式化建模与验证

来源 :华东师范大学 | 被引量 : 0次 | 上传用户:libing09006
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
机器人操作系统(Robot Operating System,ROS)在现代机器人工业中得到了广泛的应用。ROS的通信方式主要分为话题通信和服务通信。话题通信是ROS通信层的一个基本实现,其底层的基本原理是发布/订阅机制。服务通信类似于C/S架构的请求和响应模式。通信层的无死锁性和安全性直接影响整个机器人系统的稳定性,所以很有必要对ROS的通信机制进行验证。形式化方法是基于数学理论,采用非常严格的数学方法在计算机领域对一个系统进行构建、设计和验证。本文提出了一个面向ROS通信层的形式化验证框架。该框架基于对ROS底层通信的功能包“ros_comm”(roscpp版本)进行代码分析并通过模型检测方法对ROS的通信机制进行形式化验证。将ROS的话题通信模型抽象为6个功能模块,并分别建立形式化模型,各模块之间用同步信号进行关联。根据所建立的模型提取出了3种共5个关键性质。接着将所建立的模型实例化为一个三节点通信实例,并且在Uppaal中实现,仿真。根据CTL公式将提取的性质转化为Uppaal中具体的查询语句并进行验证。对验证的结果进行分析,发现ROS话题通信机制中的一个缺陷,进而提出了解决方案。在代码修正的基础上对部分模型做了更正后,再进行验证,性质得到了满足。随后将该形式化框架同样应用到ROS的服务通信的验证中,最终验证了ROS服务通信满足无死锁性和安全性。
其他文献
在《2018年道路安全全球状况报告》中显示,道理交通伤害是5到29岁人群死亡的主要原因。造成道路交通伤害的因素复杂多样,但儿童自身交通行为不规范的原因也不容忽视,而更深层次的原因是儿童交通安全意识缺乏,因此提升交通安全意识是使其免受道路交通伤害的重要举措。对此,笔者使用《儿童交通安全意识问卷》对昆明市W社区的160名中小学生进行偶遇抽样,了解交通安全意识状况。通过数据分析,笔者发现调查对象的交通安
弱视是儿童时期较为常见的视觉发育相关性眼病,是导致儿童低视力眼病的首要因素,极大地威胁我国儿童的视力健康。据调查显示,我国弱视儿童患病率为1.2%~5.3%,有2000多万儿童视力受到影响,近年来呈上升趋势。家庭训练是目前儿童弱视治疗的主要模式,在家庭训练中,一些家长难以保证长期耐心有效地指导和督促儿童训练,加之长期性的单调训练,一些儿童不能保持积极配合的状态,儿童依从性较差,训练效果不佳。本研究
马克思认为革命实践是实现人的解放的根本途径,并将劳动实践与政治革命统一于革命实践的概念中。在近代社会转型过程中,中国共产党以马克思革命实践理论为指导,以劳工权利的保障为线索,通过语言维度的意识形态灌输,对工人阶级进行充分地动员、改造和吸纳,并将劳工解放与中国社会革命相连接,进行了一系列早期的人权探索与革命实践。近代中国劳工在国家层面的政治地位低下,广大劳工没有任何民主参与的机会;在经济生活方面,中
二十世纪七十年代互联网技术以军事应用目的诞生,发展到如今已经彻底改变了人类的生活方式、融入人们的生活,伴随着互联网技术的不断成熟,各领域互联网公司不断诞生与壮大,并与人们衣食住行直接联系。中国在境内外上市的互联网公司总市值高达16.8万亿人民币,上市公司总数达147家。随着互联网企业规模与数量的增加,IPO、并购、再融资商业行为都会对互联网企业估值提出更多的要求,无论站在投资者、管理层、监管层的角
随着“对赌协议”效力认定的司法态度不断改变,“对赌协议”效力的认定对于衡平投融资双方的权利与义务,保护债权人的利益以及规范市场交易秩序都具有重要意义。本文除导论和结语外,共分为四部分:第一部分,“对赌协议”及其正当性。“对赌协议”符合合同法的定义,按照合同法对射幸合同的规定,应当与具有射幸性的赌博合同相区分。从主体上看,“对赌协议”投融资双方权利义务对等,遵循等价有偿原则。从内容看,协议约定是双方
2008年由美国次贷危机引发的全球性金融危机,使各国政府和监管当局开始重视金融机构的系统性风险及溢出效应。近年来,我国监管当局也高度重视系统性金融风险,党的十九大报告提出,“要健全金融监管体系,守住不发生系统性金融风险”。从我国金融行业结构来看,银行在金融行业中占据着重要地位,银行的风险状况直接影响我国金融系统的稳定和发展。因此防范系统性金融风险重要的是防范银行业的系统性风险。本文在梳理和分析国内
做大做强是企业的经营目标之一,而为了实现这个目标,企业必须进行规模的扩张。但是过快的扩张速度、过大的扩张程度都有可能给企业带来风险,如果企业的管理者只关注于扩张带来的规模增大、股价上升等影响而忽视伴随的风险,那么企业必将沦入危险处境。而现实中往往就是这样,高管为了追求企业规模、自身薪酬、公司股价等目标,忽视扩张伴随的风险,最终导致公司陷入财务困境。企业扩张是一个复杂的过程,受到众多因素的影响,除了
将军印是汉印发展史上一朵璀璨的奇葩,而且其风格面貌的多样性也告知着世人“将军印”一词只能做一个宽泛笼统的概念。梳理其发展脉络后大致可以按时间分为三个阶段:两汉时期为早期;魏晋为中期;南北朝为后期。三个时期内,虽依然有不同的风格,但整体上的审美感受是能体悟出这种时代差距的。将军印风格形成与发展的背景,不止与天下大乱战事紧急以及统治者维稳笼络人心所定制的政策有关,甚至还可能与当时的审美风尚有着密切关联
《中华人民共和国反不正当竞争法》中将不正当竞争行为定义为经营者在生产经营活动中,扰乱市场竞争秩序,损害其他经营者或者消费者的合法权益的行为。而《律师和律师事务所违法行为处罚办法》第6条已经明确列举了律师的四种不正当承揽业务行为,但对于此行为的规制在实务中出现了行政规制与司法规制的争议问题。律师本质上肩负双重义务,一是履行基于与当事人订立的合同而产生为当事人提供服务的义务,另一是保障法律的正确实施,
伴随着我国上市公司数量和规模的不断发展和壮大,上市公司扮演着越来越重要的角色。近年来,面对国际经济形势动荡、国内经济发展增速放缓等大环境,部分上市公司开始出现资产流动性不足、债务偿还压力加大等问题。同时,上市公司融资方式的多样性也决定了其在债券市场、股票市场中的重要地位。2020年1月至2020年12月,共有10家上市公司披露了债券违约公告,其中就包括曾位列2019年中国民营企业500强之首的海航