基于UPPAAL磁性材料生產(chǎn)線的建模與驗證

呂靖

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

關(guān)鍵詞：磁性材料生產(chǎn)線；時間自動機；模型檢驗；形式化方法；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 背景

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

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

2 研究內(nèi)容

2.1 生產(chǎn)線描述

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

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

Step B：該工序加工完畢，工件進入下一工序進行加工。

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

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

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

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

2.2 時間自動機建立

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

2.2.1 制粉機（FM）

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

2.2.2 壓機（PM）

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

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

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

2.2.4 刨光機（PL）

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

2.2.5 清洗機（CM）

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

2.2.6 分揀機（SM）

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

2.2.7 控制器（CR）

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

2.3 模型檢驗

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

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

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

A[] not deadlock

P2：可達性驗證，制粉機可以到達制粉狀態(tài)。

E<> FM.MILL；

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

E<> PM（0）.PRESS

3 結(jié)束語

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