呂靖

摘要：隨著工業(yè)的發(fā)展，產(chǎn)品的生產(chǎn)制造逐漸向智能化邁進(jìn)。磁性材料生產(chǎn)線主要研究智能化生產(chǎn)過程。該生產(chǎn)線由多種設(shè)備及控制器構(gòu)成，涉及不同工序間設(shè)備的交互，及同一工序間不同設(shè)備的并行。采用時(shí)間自動(dòng)機(jī)建立生產(chǎn)線模型，利用控制器傳輸信號(hào)，實(shí)現(xiàn)生產(chǎn)線的有效調(diào)度。并通過模型檢驗(yàn)工具UPPAAL驗(yàn)證模型性質(zhì)，保證生產(chǎn)線的正確性和安全性。

關(guān)鍵詞：磁性材料生產(chǎn)線；時(shí)間自動(dòng)機(jī)；模型檢驗(yàn)；形式化方法；UPPAAL

中圖分類號(hào)：TP391 文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：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 背景

磁性材料是電子行業(yè)非常重要的材料，已成為推進(jìn)我國經(jīng)濟(jì)發(fā)展中不可或缺的電子產(chǎn)品元件。不僅常見于日常生活家電、汽車、電腦、通訊等，并且在醫(yī)療、航太、軍事等領(lǐng)域的應(yīng)用十分廣泛。磁性材料生產(chǎn)線的調(diào)度算法設(shè)計(jì)將有效提高生產(chǎn)效率，為企業(yè)降低能耗；其安全性驗(yàn)證，可以保證系統(tǒng)的正確性及企業(yè)的生產(chǎn)安全，為企業(yè)帶來更好的經(jīng)濟(jì)效益。

磁性材料生產(chǎn)線具有加工周期長、工序多、設(shè)備復(fù)雜等特點(diǎn)，是眾多離散事件與連續(xù)事件混合的生產(chǎn)過程。本文采用時(shí)間自動(dòng)機(jī)建立生產(chǎn)線模型，引入核心調(diào)度算法，模擬控制器運(yùn)行，實(shí)現(xiàn)生產(chǎn)線各工件及設(shè)備的調(diào)度。并通過模型檢驗(yàn)工具UPPAAL進(jìn)行模型檢驗(yàn)，驗(yàn)證系統(tǒng)安全性和響應(yīng)受限。

2 研究內(nèi)容

2.1 生產(chǎn)線描述

本文研究的是基于磁業(yè)智能工廠的磁芯加工生產(chǎn)線。該生產(chǎn)線由1臺(tái)制粉機(jī)（FM）、2臺(tái)成型機(jī)（PM01、PM02）、2臺(tái)燒結(jié)窯爐（SF01、SF02）、2臺(tái)刨光機(jī)（PL01、PL02）、2臺(tái)清洗機(jī)（CM01、CM02）和5臺(tái)分檢機(jī)（SM01、SM02、SM03、SM04、SM05）六個(gè)工序組成。在生產(chǎn)線中，信號(hào)傳輸非常復(fù)雜，采用控制器CR與各設(shè)備之間通訊。圖1為磁性材料生產(chǎn)線的生產(chǎn)流程。下面以一個(gè)工件Z由原料到最終成品的生產(chǎn)為例，描述生產(chǎn)線的運(yùn)行。其中工件在各工序間的傳輸時(shí)間忽略不計(jì)。

Step A：控制器CR接到一批訂單，向FM發(fā)送請(qǐng)求；當(dāng)FM準(zhǔn)備完畢，返回信號(hào)，并開始工作。

Step B：該工序加工完畢，工件進(jìn)入下一工序進(jìn)行加工。

Step C：在SF工序，窯爐燒結(jié)過程為每臺(tái)窯爐每17min向爐內(nèi)輸送一個(gè)工件進(jìn)行加工，同時(shí)輸出一個(gè)加工完畢的工件，因此在窯爐生產(chǎn)環(huán)節(jié)設(shè)計(jì)一個(gè)方法，使得窯爐每17min發(fā)送信號(hào)，通知CR可以放入一個(gè)工件。

Step D：當(dāng)工件在SF工序加工完畢，向CR發(fā)送信號(hào)。

Step E：CR收到SF加工完畢的信號(hào)后，立即向PL發(fā)送信號(hào)，PL進(jìn)入準(zhǔn)備工作，并返回信號(hào)，表示其已準(zhǔn)備完畢。

Step F：當(dāng)最后一個(gè)工序SM加工完畢，向CR發(fā)送信號(hào)，CR將統(tǒng)計(jì)已加工工件個(gè)數(shù)。

2.2 時(shí)間自動(dòng)機(jī)建立

時(shí)間自動(dòng)機(jī)由R.Alur和Dill在1994年首次提出，是一種有效描述實(shí)時(shí)系統(tǒng)行為的計(jì)算模型，極大促進(jìn)了系統(tǒng)建模[1]。磁性材料生產(chǎn)線的模型是由七個(gè)自動(dòng)機(jī)組成的自動(dòng)機(jī)網(wǎng)，分別是六個(gè)工序和一個(gè)控制器CR。下面詳細(xì)描述每個(gè)自動(dòng)機(jī)的狀態(tài)、狀態(tài)遷移及各自動(dòng)機(jī)與控制器CR之間的通訊。

2.2.1 制粉機(jī)（FM）

原料Z進(jìn)入生產(chǎn)線， CR發(fā)送消息FM_pre_ok[Z]給FM，查詢FM狀態(tài)。如果為IDLE狀態(tài)，則FM收到消息進(jìn)入PRE狀態(tài)；如果為其他狀態(tài)，則進(jìn)入排隊(duì)等待。當(dāng)FM準(zhǔn)備完畢，進(jìn)入PRE_OK狀態(tài)，發(fā)送消息FM_can_start[Z]給CR。FM收到FM_start[Z]消息進(jìn)入MILL狀態(tài)，開始對(duì)原料Z進(jìn)行制粉。加工完成后，向CR回傳消息FM_finish[Z]告知加工完畢，后置操作完成后進(jìn)入IDLE狀態(tài)。圖2為FM自動(dòng)機(jī)模型。

2.2.2 壓機(jī)（PM）

當(dāng)CR接收到來自PM[a]（a表示PM設(shè)備編號(hào)，a=0，1）消息PM_finish[Z]，表示PM[a]已結(jié)束上一工件的壓制，可以開始加工下一工件。此時(shí)工件Z將傳送至PM[a]，PM[a]更新狀態(tài)為PRESS。同時(shí)CR發(fā)送消息SF_can_start[Z]至SF，選擇合適的設(shè)備。工件Z在PM[a]工序壓制完成后，立即發(fā)送PM_finish[Z]告知CR。

2.2.3 燒結(jié)窯爐（SF）

當(dāng)CR收到來自SF[b]（b表示SF設(shè)備編號(hào)，b=0，1）消息SF_start[Z]后，工件Z將進(jìn)入下一工序。由于燒結(jié)窯爐必須按照特定時(shí)間每17min放入一個(gè)工件，SF中存在計(jì)算時(shí)間的方法，當(dāng)與上一工件間隔不滿17min時(shí)，SF處于WAIT狀態(tài)；當(dāng)時(shí)鐘到達(dá)17min時(shí)，SF由WAIT狀態(tài)轉(zhuǎn)為IDLE狀態(tài)（該狀態(tài)為Urgent，時(shí)鐘在此狀態(tài)不做停留，若無工件進(jìn)入將進(jìn)入WAIT狀態(tài)繼續(xù)計(jì)算時(shí)間），并發(fā)送一條消息SF_start，CR立即收到該消息，表示工件可以進(jìn)入窯爐開始燒結(jié)。工件Z到達(dá)SF[b]，首先判斷該設(shè)備狀態(tài)，發(fā)送消息SF_can_start[Z]。當(dāng)收到SF_start消息，立即傳送至窯爐，此時(shí)SF狀態(tài)為PUT。

2.2.4 刨光機(jī)（PL）

刨光機(jī)在加工前需要準(zhǔn)備時(shí)間，PL收到來自CR的消息PL_pre_ok[Z]，PL[c]（c表示PL設(shè)備編號(hào)，c=0，1）將進(jìn)入PRE狀態(tài)。燒結(jié)完成，SF發(fā)送消息SF_finish[Z]。當(dāng)PL[c]發(fā)送消息PL_can_start[Z]表示其準(zhǔn)備完畢，可以開始加工。此時(shí)工件Z將傳送至PL[c]，CR發(fā)送消息PL_start開始刨光，狀態(tài)為PLANE。工件Z在PL加工完畢，CR收到消息PL_finish[Z]。

2.2.5 清洗機(jī)（CM）

工件Z在PL加工完成后CR判斷是否有CM處于IDLE狀態(tài)。如果有，則將工件Z傳送至該設(shè)備；如果沒有，則等待有設(shè)備CM[d]（d表示CM設(shè)備編號(hào)，c=0，1）發(fā)送消息CM_finish[Z-1]（Z-1表示該設(shè)備加工的上一個(gè)工件）。工件Z在進(jìn)入CM[d]清洗（CLEAN狀態(tài)），并在加工完成時(shí)返回CM_finish[Z]。

2.2.6 分揀機(jī)（SM）

當(dāng)CR將工件Z送入SM[e] （e表示SM設(shè)備編號(hào)，e=0，1，2，3，4）進(jìn)行分檢，狀態(tài)由IDLE遷移至SORT。此工序?yàn)樯a(chǎn)線最后一道工序，在工件Z加工完畢，向CR發(fā)送信號(hào)SM_finish[Z]， CR中TotalNum = TotalNum + 1。

2.2.7 控制器（CR）

自動(dòng)機(jī)CR采用同步信號(hào)（Channel Synchronization）與各設(shè)備之間通信，通信過程耗時(shí)為零，函數(shù)TotalNum用來統(tǒng)計(jì)該訂單訂單已生產(chǎn)工件個(gè)數(shù)的變量。

2.3 模型檢驗(yàn)

實(shí)時(shí)系統(tǒng)的模型檢查一個(gè)重要原因是無窮多個(gè)時(shí)鐘解釋可以被劃分為有窮多個(gè)域，屬于同一個(gè)域的時(shí)鐘解釋滿足同樣的性質(zhì)[4]。

本文使用模型檢驗(yàn)工具UPPAAL對(duì)生產(chǎn)線的性質(zhì)進(jìn)行驗(yàn)證。通過以下性質(zhì)驗(yàn)證該模型：

P1：安全l性驗(yàn)證，系統(tǒng)中不存在死鎖。

A[] not deadlock

P2：可達(dá)性驗(yàn)證，制粉機(jī)可以到達(dá)制粉狀態(tài)。

E<> FM.MILL；

P3：壓機(jī)PM[0]可以到達(dá)PRESS狀態(tài)。

E<> PM（0）.PRESS

3 結(jié)束語

本文采用UPPAAL建模工具建立磁性材料生產(chǎn)線時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型，設(shè)計(jì)調(diào)度算法選擇合適設(shè)備，并通過形式化方法模型檢驗(yàn)語言驗(yàn)證系統(tǒng)的安全性，確保設(shè)計(jì)的正確性。然而，本文設(shè)計(jì)中并未考慮設(shè)備出現(xiàn)故障的概率，因此在后續(xù)工作中，將考慮采用概率時(shí)間自動(dòng)機(jī)模擬實(shí)際生產(chǎn)線，并通過模型檢驗(yàn)工具檢驗(yàn)其正確性。

參考文獻(xiàn)：

[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的實(shí)時(shí)系統(tǒng)模型驗(yàn)證[J]. 計(jì)算機(jī)應(yīng)用， 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.