基于UPPAAL磁性材料生产线的建模与验证.docVIP

基于UPPAAL磁性材料生产线的建模与验证 　　摘要：随着工业的发展，产品的生产制造逐渐向智能化迈进。磁性材料生产线主要研究智能化生产过程。该生产线由多种设备及控制器构成，涉及不同工序间设备的交互，及同一工序间不同设备的并行。采用时间自动机建立生产线模型，利用控制器传输信号，实现生产线的有效调度。并通过模型检验工具UPPAAL验证模型性质，保证生产线的正确性和安全性。 　　关键词：磁性材料生产线；时间自动机；模型检验；形式化方法；UPPAAL 　　中图分类号：TP391 文献标识码：A 文章编号：1009-3044（2016）28-0252-02 　　Abstract： With the development of industry， manufacture of the products are gradually moving towards intelligent. Magnetic material production line is mainly research about intelligent manufacturing process. This production line consists of a controller and diverse equipment， involves equipment’s interaction between different process and parallel equipment between the same process. The production line model is established by timed automata， and transferring signal by controller， realizing the effective scheduling of the production line. The model is verified through the model checking tools UPPAAL properties， ensure validity and security of the production line. 　　Key words： magnetic material production line； timed automata； model checking； formal method 　　1 背景 　　磁性材料是电子行业非常重要的材料，已成为推进我国经济发展中不可或缺的电子产品元件。不仅常见于日常生活家电、汽车、电脑、通讯等，并且在医疗、航太、军事等领域的应用十分广泛。磁性材料生产线的调度算法设计将有效提高生产效率，为企业降低能耗；其安全性验证，可以保证系统的正确性及企业的生产安全，为企业带来更好的经济效益。 　　磁性材料生产线具有加工周期长、工序多、设备复杂等特点，是众多离散事件与连续事件混合的生产过程。本文采用时间自动机建立生产线模型，引入核心调度算法，模拟控制器运行，实现生产线各工件及设备的调度。并通过模型检验工具UPPAAL进行模型检验，验证系统安全性和响应受限。 　　2 研究内容 　　2.1 生产线描述 　　本文研究的是基于磁业智能工厂的磁芯加工生产线。该生产线由1台制粉机（FM）、2台成型机（PM01、PM02）、2台烧结窑炉（SF01、SF02）、2台刨光机（PL01、PL02）、2台清洗机（CM01、CM02）和5台分检机（SM01、SM02、SM03、SM04、SM05）六个工序组成。在生产线中，信号传输非常复杂，采用控制器CR与各设备之间通讯。图1为磁性材料生产线的生产流程。下面以一个工件Z由原料到最终成品的生产为例，描述生产线的运行。其中工件在各工序间的传输时间忽略不计。 　　Step A：控制器CR接到一批订单，向FM发送请求；当FM准备完毕，返回信号，并开始工作。 　　Step B：该工序加工完毕，工件进入下一工序进行加工。 　　Step C：在SF工序，窑炉烧结过程为每台窑炉每17min向炉内输送一个工件进行加工，同时输出一个加工完毕的工件，因此在窑炉生产环节设计一个方法，使得窑炉每17min发送信号，通知CR可以放入一个工件。 　　Step D：当工件在SF工序加工完毕，向CR发送信号。 　　Step E：CR收到SF加工完毕的信号后，立即向PL发送信号，PL进入准备工作，并返回信号，表示其已准备完毕。 　　Step F：当最后一个工序SM加工完毕，向CR发送信号，CR将统计已加工工件个数。 　　2.2 时间自动机建立 　　时间自动机由R.Alur和Dill在1994年首次提出，是一种有