基于PLC运动控制程序的形式化建模与验证

来源 :杭州电子科技大学 | 被引量 : 0次 | 上传用户:liongliong453
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
目前,可编程控制器(Programmable Controller,PLC)已在工业控制领域中得到广泛运用。PLC实现的运动控制系统可以采用多种语言,其中功能块图(Function Block Diagram,FBD)和梯形图(Ladder Diagram,LD)是在工业控制及自动化领域中常用的编程语言,但是很少有针对这两种编程语言的验证。因此,本论文以验证运动控制程序的可信性为目标,结合国家重大课题,对如何提高功能块和梯形图的可信性进行研究,提出了针对PLCopen运动控制功能块和梯形图的模型转换方法,从而验证运动控制程序的可信性。本文重点研究对功能块图程序和梯形图程序的验证,在程序描述和模型转换等方面做了以下研究:1)根据可编程控制器的周期扫描特性,本文采用时间自动机作为建模方法,提出可编程控制器循环执行模型。围绕功能块图语言和基于Uppaal系统的时间自动机模型展开研究,针对运动控制系统的可信性问题,提出功能块图到Uppaal系统的转换方法(D-U转换),将功能块图程序转换为基于Uppaal系统的时间自动机模型。2)结合国际标准IEC 61131-3,根据梯形图的程序结构以及可编程控制器的周期性执行方式,提出将梯形图程序抽象成布尔表达式,建立梯形图程序的有色Petri网模型。在实现运动控制的梯形图程序中,通过使用计时器在两个指令之间增加延时,可以用于确保两个指令顺序进入PLC的内部CPU,因此本文针对三种不同功能的计时器建立有色Petri网模型。对功能块图模型和梯形图模型分别进行实现和验证。利用Uppaal模型检测工具对功能块图到时间自动机的转换方法进行建模和验证。通过CPN Tools自动化分析工具以及CPN ML语法,对基于梯形图的有色Petri建模方式进行仿真和验证。实验结果证明文章提出的功能块图模型和梯形图模型的可信性。通过实验结果,开发人员可以发现程序或系统的安全性问题或性能问题,从而更好地改进系统。
其他文献
近年来,随着互联网规模不断扩大和异构动态应用的持续增加,网络体系架构也显露出各种各样的问题,例如:灵活性差、可靠性不够、管理和控制困难、能耗差。因此,它无法满足互联网异构动态应用的新需求,网络基础设施处于一种“僵化”状态。网络虚拟化(network virtualization,NV)可以使新的应用场景与当前的互联网无缝集成,从而促进互联网网络架构的快速发展,被认为是解决网络“僵化”问题的最佳方案
在市场环境变化莫测的今天,创新是企业迅速适应外部变化、满足市场需求的必不可少的手段。为保持竞争优势,企业需要员工更加主动地投入工作,在产品、流程、技术和商业模式等方面表现出更多的创造性行为。“创造力是促进创新的必要因素”,是创新成果产生的源泉。个体创造力是团队层面和组织层面创造力的基础,是创造力研究的起点。因此,如何提高员工创造力一直是企业面临的重点和难点问题。一方面,知识是创造力形成的基础,在中
目前红外热成像系统已经广泛应用于军事和民用领域,其核心器件是红外焦平面阵列。由于制造工艺和材料的限制导致在图像中出现非均匀性,其中条纹非均匀性尤其明显,严重影响图像质量。传统的条纹非均匀性校正方法使用复杂的图像先验知识,校正后的图像存在伪影及边缘模糊问题。本文使用深度学习方法对条纹非均匀性进行实时校正,并尽可能保留图像中的热细节信息,对提高后续处理精度具有重要的意义。本文将从以下三个方面进行研究:
临近空间高超声速飞行器以10~25马赫的高超声速在大气层中飞行时,飞行器周围的气体与飞行器表面发生剧烈的摩擦,产生了包覆于飞行器表面的等离子鞘套。等离子鞘套内含有大量的自由电子,当雷达波入射等离子鞘套后,会对不同频段的雷达波产生不同程度的幅度和相位影响,还会造成雷达波极化信息丢失,极化旋向发生反转,造成地面站的雷达接收天线出现极化失配现象,对高超声速飞行器雷达探测的有效性和准确性产生了极大的干扰。
电力线路安全运行是保障社会稳定的重要因素,极端天气下的冰冻灾害会导致输电线路覆冰,所引发的各种事故不仅会对电力设施造成不可逆转的破坏,增加电力工作人员的巡检难度,而且会给各用电单位带来不可避免的经济损失,同样也会给人民群众生活带来极大的不便。电网企业对此高度重视,为保障在冰冻环境中的输电安全,研究以光纤传感器为基础的电力线路覆冰监测系统,可以有效地对事故进行识别和预警。本文根据云南电网滇东北重度覆
近年来,随着无人设备的自主性和智能型愈加提高,应用场景也愈加广泛。现在旋翼无人机随船执行任务的情况较多,可以将无人艇与旋翼无人机二者的优势相结合,而旋翼无人机在执行任务时起飞和降落两个阶段是重要也容易出现故障的阶段,因此研究旋翼无人机在运动无人艇上实现自主起飞和自主降落具有重要的意义。本文以旋翼无人机和无人艇为实验平台,从旋翼无人机在运动无人艇上自主起飞和降落的控制策略和旋翼无人机与无人艇的硬件构
赋予计算机人的智能,实现准确表情识别在人工智能高速发展的今天一直具有重要的研究和应用价值r然而表情识别易受到光照、姿态、遮挡等非受控的环境因素影响,同时现有数据集具有较小的样本容量和样本空间内具有明显的类间相似性与类内差异性给精确识别带来了诸多挑战。本文从特征层面溁入分析表情识别任务,旨在通过对不同性质的特征的提取与融合以获得更加鲁棒的表情特征,从而显著提高识别效果。本文的研究内容和主要贡献包括:
单壁碳纳米管(single-walled carbon nanotubes,SWNTs)自1993年被发现以来,一直是纳米科学领域研究的热点之一,主要得益于其完美的共轭管状结构和优异的物理化学性能。这使得
随着科学技术的进步,增材制造技术得到了迅速发展,受到了国内外的广泛关注。选择性激光熔化(Selective Laser Melting,SLM)技术是一种基于激光烧结金属的增材制造技术,其突出优点在于可成型复杂的零件结构、材料的利用率较高、对于产品结构设计的变化可作出快速响应。在本文中,将SLM和结构轻量化设计结合在一起,系统地分析了基于SLM技术的零件轻量化设计约束和设计规则;针对SLM技术成型
电力物联网(Power Internet of Things,PIo T)将物联网技术应用于传统电力系统,以期达到提高电力系统自动化、信息化、智能化的目的。电力物联网通信要求在低信噪比下信号能够可靠传输。其次,在电力物联网末端接入设备数量迅速增加的趋势下,提高网络的吞吐量也成为电力物联网发展的必然要求。IEEE 802.15.4g是适合智能抄表应用制定的无线通信标准,适合于超低复杂性、低成本、低功