基于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 equipments 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年首次提出，是一种有效描述实时系统行为的计算模型，极大促进了系统建模[1]。磁性材料生产线的模型是由七个自动机组成的自动机网，分别是六个工序和一个控制器CR。下面详细描述每个自动机的状态、状态迁移及各自动机与控制器CR之间的通讯。

2.2.1 制粉机（FM）

原料Z进入生产线， CR发送消息FM_pre_ok[Z]给FM，查询FM状态。如果为IDLE状态，则FM收到消息进入PRE状态；如果为其他状态，则进入排队等待。当FM准备完毕，进入PRE_OK状态，发送消息FM_can_start[Z]给CR。FM收到FM_start[Z]消息进入MILL状态，开始对原料Z进行制粉。加工完成后，向CR回传消息FM_finish[Z]告知加工完毕，后置操作完成后进入IDLE状态。图2为FM自动机模型。

2.2.2 压机（PM）

当CR接收到来自PM[a]（a表示PM设备编号，a=0，1）消息PM_finish[Z]，表示PM[a]已结束上一工件的压制，可以开始加工下一工件。此时工件Z将传送至PM[a]，PM[a]更新状态为PRESS。同时CR发送消息SF_can_start[Z]至SF，选择合适的设备。工件Z在PM[a]工序压制完成后，立即发送PM_finish[Z]告知CR。

2.2.3 烧结窑炉（SF）

当CR收到来自SF[b]（b表示SF设备编号，b=0，1）消息SF_start[Z]后，工件Z将进入下一工序。由于烧结窑炉必须按照特定时间每17min放入一个工件，SF中存在计算时间的方法，当与上一工件间隔不满17min时，SF处于WAIT状态；当时钟到达17min时，SF由WAIT状态转为IDLE状态（该状态为Urgent，时钟在此状态不做停留，若无工件进入将进入WAIT状态继续计算时间），并发送一条消息SF_start，CR立即收到该消息，表示工件可以进入窑炉开始烧结。工件Z到达SF[b]，首先判断该设备状态，发送消息SF_can_start[Z]。当收到SF_start消息，立即传送至窑炉，此时SF状态为PUT。

2.2.4 刨光机（PL）

刨光机在加工前需要准备时间，PL收到来自CR的消息PL_pre_ok[Z]，PL[c]（c表示PL设备编号，c=0，1）将进入PRE状态。烧结完成，SF发送消息SF_finish[Z]。当PL[c]发送消息PL_can_start[Z]表示其准备完毕，可以开始加工。此时工件Z将传送至PL[c]，CR发送消息PL_start开始刨光，状态为PLANE。工件Z在PL加工完毕，CR收到消息PL_finish[Z]。

2.2.5 清洗机（CM）

工件Z在PL加工完成后CR判断是否有CM处于IDLE状态。如果有，则将工件Z传送至该设备；如果没有，则等待有设备CM[d]（d表示CM设备编号，c=0，1）发送消息CM_finish[Z-1]（Z-1表示该设备加工的上一个工件）。工件Z在进入CM[d]清洗（CLEAN状态），并在加工完成时返回CM_finish[Z]。

2.2.6 分拣机（SM）

当CR将工件Z送入SM[e] （e表示SM设备编号，e=0，1，2，3，4）进行分检，状态由IDLE迁移至SORT。此工序为生产线最后一道工序，在工件Z加工完毕，向CR发送信号SM_finish[Z]， CR中TotalNum = TotalNum + 1。

2.2.7 控制器（CR）

自动机CR采用同步信号（Channel Synchronization）与各设备之间通信，通信过程耗时为零，函数TotalNum用来统计该订单订单已生产工件个数的变量。

2.3 模型检验

实时系统的模型检查一个重要原因是无穷多个时钟解释可以被划分为有穷多个域，属于同一个域的时钟解释满足同样的性质[4]。

本文使用模型检验工具UPPAAL对生产线的性质进行验证。通过以下性质验证该模型：

P1：安全l性验证，系统中不存在死锁。

A[] not deadlock

P2：可达性验证，制粉机可以到达制粉状态。

E<> FM.MILL；

P3：压机PM[0]可以到达PRESS状态。

E<> PM（0）.PRESS

3 结束语

本文采用UPPAAL建模工具建立磁性材料生产线时间自动机网络模型，设计调度算法选择合适设备，并通过形式化方法模型检验语言验证系统的安全性，确保设计的正确性。然而，本文设计中并未考虑设备出现故障的概率，因此在后续工作中，将考虑采用概率时间自动机模拟实际生产线，并通过模型检验工具检验其正确性。

参考文献：

[1] Alur R， Dill D L. A theory of timed automata[J]. Theoretical computer science， 1994， 126（2）： 183-235.

[2] Zu Q， Zhang M， Liu J， et al. Designing， Modelling and Verifying a Container Terminal System Using UPPAAL[C]//High Assurance Systems Engineering Symposium， 2008. HASE 2008. 11th IEEE. IEEE， 2008： 445-448.

[3] Abdedda? Y， Asarin E， Maler O. Scheduling with timed automata[J]. Theoretical Computer Science， 2006， 354（2）： 272-300.

[4] 周清雷， 姬莉霞， 王艳梅. 基于UPPAAL的实时系统模型验证[J]. 计算机应用， 2004， 24（9）： 129-131.

[5] Clarke E M， Grumberg O， Peled D. Model checking[M]. MIT press， 1999.

[6] Iversen T K， Kristoffersen K J， Larsen K G， et al. Model-checking real-time control programs： verifying LEGO MINDSTORMS TM systems using UPPAAL[C]//Real-Time Systems， 2000. Euromicro RTS 2000. 12th Euromicro Conference on. IEEE， 2000： 147-155.