欢迎来到天天文库
浏览记录
ID:31359594
大小:110.00 KB
页数:7页
时间:2019-01-09
《基于uppaal磁性材料生产线的建模与验证》由会员上传分享,免费在线阅读,更多相关内容在学术论文-天天文库。
1、基于UPPAAL磁性材料生产线的建模与验证 摘要:随着工业的发展,产品的生产制造逐渐向智能化迈进。磁性材料生产线主要研究智能化生产过程。该生产线由多种设备及控制器构成,涉及不同工序间设备的交互,及同一工序间不同设备的并行。采用时间自动机建立生产线模型,利用控制器传输信号,实现生产线的有效调度。并通过模型检验工具UPPAAL验证模型性质,保证生产线的正确性和安全性。 关键词:磁性材料生产线;时间自动机;模型检验;形式化方法;UPPAAL 中图分类号:TP391文献标识码:A文章编号:1009-3044(2016)28-0252-02 Abstract
2、:Withthedevelopmentofindustry,manufactureoftheproductsaregraduallymovingtowardsintelligent.Magneticmaterialproductionlineismainlyresearchaboutintelligentmanufacturingprocess.Thisproductionlineconsistsofacontrolleranddiverseequipment,involvesequipment’sinteractionbetweendifferentpr
3、ocessandparallelequipmentbetweenthesameprocess.Theproductionlinemodelisestablishedbytimedautomata,andtransferringsignalbycontroller,realizingtheeffectiveschedulingoftheproductionline.ThemodelisverifiedthroughthemodelcheckingtoolsUPPAALproperties,ensurevalidityandsecurityoftheprodu
4、ctionline.7 Keywords:magneticmaterialproductionline;timedautomata;modelchecking;formalmethod 1背景 磁性材料是电子行业非常重要的材料,已成为推进我国经济发展中不可或缺的电子产品元件。不仅常见于日常生活家电、汽车、电脑、通讯等,并且在医疗、航太、军事等领域的应用十分广泛。磁性材料生产线的调度算法设计将有效提高生产效率,为企业降低能耗;其安全性验证,可以保证系统的正确性及企业的生产安全,为企业带来更好的经济效益。 磁性材料生产线具有加工周期长、工序多、设备复杂
5、等特点,是众多离散事件与连续事件混合的生产过程。本文采用时间自动机建立生产线模型,引入核心调度算法,模拟控制器运行,实现生产线各工件及设备的调度。并通过模型检验工具UPPAAL进行模型检验,验证系统安全性和响应受限。 2研究内容 2.1生产线描述 本文研究的是基于磁业智能工厂的磁芯加工生产线。该生产线由1台制粉机(FM)、2台成型机(PM01、PM02)、2台烧结窑炉(SF01、SF02)、2台刨光机(PL01、PL02)、2台清洗机(CM01、CM02)和5台分检机(SM01、SM02、SM03、SM04、SM05)六个工序组成。在生产线中,信号传
6、输非常复杂,采用控制器CR与各设备之间通讯。图1为磁性材料生产线的生产流程。下面以一个工件Z由原料到最终成品的生产为例,描述生产线的运行。其中工件在各工序间的传输时间忽略不计。7 StepA:控制器CR接到一批订单,向FM发送请求;当FM准备完毕,返回信号,并开始工作。 StepB:该工序加工完毕,工件进入下一工序进行加工。 StepC:在SF工序,窑炉烧结过程为每台窑炉每17min向炉内输送一个工件进行加工,同时输出一个加工完毕的工件,因此在窑炉生产环节设计一个方法,使得窑炉每17min发送信号,通知CR可以放入一个工件。 StepD:当工件在S
7、F工序加工完毕,向CR发送信号。 StepE:CR收到SF加工完毕的信号后,立即向PL发送信号,PL进入准备工作,并返回信号,表示其已准备完毕。 StepF:当最后一个工序SM加工完毕,向CR发送信号,CR将统计已加工工件个数。 2.2时间自动机建立 时间自动机由R.Alur和Dill在1994年首次提出,是一种有效描述实时系统行为的计算模型,极大促进了系统建模[1]。磁性材料生产线的模型是由七个自动机组成的自动机网,分别是六个工序和一个控制器CR。下面详细描述每个自动机的状态、状态迁移及各自动机与控制器CR之间的通讯。 2.2.1制粉机(FM)
8、 原料Z进入生产线,7CR发送消息FM_pre_ok[Z]给FM
此文档下载收益归作者所有