基于uppaal磁性材料生产线的建模与验证

《基于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