基于線性時序邏輯的制卡流水線控制系統建模研究

沈陽+齊德昱

摘要：多工位制卡流水線設備控制系統是一種相當復雜的計算機控制軟件，要求能夠使用工業控制機或PC機等一般計算機設備控制流水型設備的各工位的生產和協作，保證產品在各工位間傳送、加工過程流暢，出錯率低。本文采用形式語義及方法對金融領域卡片生產設備的通用系統服務框架進行研究和建模，以確保建立一個穩定、可移植性強的通用開發框架，通過這個通用開發框架，可以迅速高效地開發出針對某一特定機型的計算機控制軟件。本文將使用線性時序邏輯語法對多工位制卡設備控制系統進行形式化語義描述和建模，主要針對整個制卡流程以及在卡片在一個模塊中的狀態這兩個方面進行建模。通過形式語義的動作推理，驗證了本模型是動作是可實現的，狀態是可達的，為進一步的全面建模研究工作奠定了基礎。

關鍵詞：形式語義；多工位；建模；線性時序邏輯

中圖分類號：TP316 文獻標識碼：A 文章編號：1007-9416（2017）05-0083-03

現今現代流水型多工位加工設備的控制系統存在以下不足：（1）系統設計開發思路仍然停留在“一機一程序”的時代（PC或PLC程序亦然）；（2）未能適應除機械標準件以外其他自定義部件的快速替換；（3）機器控制代碼難以復用與重構，存在不必要的重復或冗余；（4）勉強復用或擴展現有代碼導致思路局限，可能帶來功能上的隱患；（5）與外部系統缺乏足夠豐富的交互接口，難以與新技術集成（如云計算，自診斷）；（6）缺乏領域專用的設計，開發和仿真測試工具。

總而言之，其根源在于缺乏一個以形式化理論支持的領域專用軟件框架。我們面對的問題是：一個怎樣的程序結構（框架）才能滿足現代流水型加工設備控制系統的需要？作為這類設備的設計與制造商，需要不斷根據產品及用戶的需求，來設計與生產各種各樣的設備，因此有必要研發一種通用設備服務來支持實現這種流水型多工位系統的要求，并具有很強的開放性和擴展性。如果采用UML的方式對該系統建模，盡管其靜態語義由元模型給出，但其動態語義卻十分模糊，不利于對其所描述的需求進行形式化的驗證和確認，本文將采用線性時序邏輯對流水型加工設備控制系統中的部分功能進行形式化建模和驗證，以保證其無二義性以及準確性[1]。

1 使用線性時序邏輯語法描述制卡流程

流水型多工位設備的包括：啟動、重置系統、格式化、數據加載、打印、過卡等多個子過程。主要功能描述如下[2]：

（1）啟動：各組件實例化，系統進行初始化。（2）重置系統：要求對整個流水線進行清理，包括清理殘存在系統中的卡片、清空數據和狀態等。（3）格式化：將客戶端卡片設計軟件中生成的卡片模板（XML文件）與相關變量進行映射并發送到服務器端。（4）打印：該環節最為復雜，機器對卡片的打印包括多個流程，如發卡、打凹凸字，熱轉印、燙金、寫磁、出卡等。本節主要選取打凸字的過程作為線性時序邏輯描述的目標。（5）過卡：只讓卡片從發卡器到出卡端整體過一遍，并不進行打印的過程，作用是確保流水線通道通暢[3]。

除上述子過程之外還是銑槽、IC片加密等過程就不再一一贅述。

打凹凸字過程的順序圖如圖1所示，整個打凹凸字過程中涉及到的對象有：操作員，Client，ModuleServer，Service，工位，分別記為：w，c，ms，sv，pos。

我們用這樣一個四元組來表示這個順序圖：SD=。Obj、 Msg、 Loc分別表示順序圖中對象的集合、消息的集合以及位點的集合；F則表示從消息到位點的函數，即，其中，s表示發送消息，r表示接收消息。

Obj=< w， c， ms， sv， pos >

Msg=

Loc={，，，，， ，，，，， ， ， ， ， ，， ， ， ， ， ， ， }

F（m1，s）=， F（m1，r）=，

F（m2，s）=， F（m2，r）=，

F（m3，s）=， F（m3，r）=， F（m4，s）=， F（m4，r）=

F（m5，s）=， F（m5，r）=， F（m6，s）=， F（m6，r）=

F（m7，s）=， F（m7，r）=， F（m8，s）=， F（m8，r）=

F（m9，s）=， F（m9，r）=， F（m10，s）=， F（m10，r）=

F（m11，s）=， F（m11，r）=， F（m12，s）=， F（m12，r）=

使用LTL對該順序圖主要事件進行形式化表示的語義描述如下：

2 使用線性時序邏輯語法描述單一模塊中的卡片狀態

制卡過程中的卡片狀態圖2所示，對于制卡過程中，卡片的狀態圖是最需要關注的，包括重置系統、制卡、過卡等多種狀態。本節將選取在制卡過程中卡片狀態的轉換這個過程，用線性時序邏輯反映卡片狀態以及相關的邏輯驗證[4]。

各狀態含義[5]：（1）DEMAND狀態：卡片已經準備就緒，可以制卡。（2）ACTIVE狀態：制卡過程中的復合狀態。（3）ACK狀態：系統響應卡片請求，由于制片過程與機器的交互是一問一答。首先要收到機器返回的ACK狀態才到進行下一步操作。（4）RETRY狀態：機器由于某種原因暫停工作，卡片進入重試狀態。（5）COMPLETE：機器遇到某些不可恢復的錯誤，卡片進入完成狀態。（6）FINISH：制卡過程結束。

制卡時，卡片首先進行初始化操作，以確定是否準備就緒，然后立即進入DEMAND狀態。當接到doServiceProcess事件時，接收到機器的ACK響應后，進入激活狀態（ACTIVE），ACTIVE無條件進入ACK狀態。在ACK狀態中進行等待阻塞，監聽機器返回的消息，如果是retry，卡片進行TRETRY狀態，如果是ok，則進入FINISH狀態，如果是error，卡片進入COMPLETE狀態。在RETRY狀態中，當接到doServiceRecoverOnRetry事件，則進入ACK狀態。在COMPLETE狀態中，當接到doServiceDeplyOnComplete事件時，卡片也進入FINISH狀態[6]。

該狀態圖的靜態語義形式化如下：

圖2所示的狀態，設轉換動作為Translate，狀態集類為States，則可形式化如下：

對應的部分語義為：

3 可達性驗證

根據2，3節建立的形式語義模型，該模型形式語義的動作推理如下[7-8]：

對于動作（包括上述的原子動作或復雜動作），如果存在解釋和，使滿足，則稱動作是可實現的。

狀態的可達性：（1）如果動作滿足以下條件，則稱狀態是可達的；（2）如果動作是可實現的，則狀態是可達的；（3）假設有動作和，如果和都可實現，則狀態是可達的。

例如上述形式化中的，有，由于都是可實現的，所以是可實現的，可知狀態是可達的。狀態圖中具備可達性的狀態有：INITIALIZE， DEMAND， ACTIVE， COMPLETE， FINISH。

4 結語

使用UML描述圖形簡單明了，但無法分析和驗證系統模型的一致性和準確性。使用UML+形式化方法進行該通用開發框架的建模，可以使系統架構的清晰，同時能夠保證模型的正確性和健壯性。多工位制卡流水線設備控制系統建模一直是業界不斷研究和探討的課題，本文采用線性時序邏輯語法描述流水線整個制卡流程以及一個工位中的卡片狀態，以提高流水線控制系統分析設計的準確性和安全性，為進一步形式化打下基礎。下一步研究將通過全面形式化流水線建模，為流水型產品加工裝備軟硬件的組態化研究打下基礎。

參考文獻

[1]戎玫，張廣泉.UML順序圖的一種形式化描述方法[J].重慶師范大學學報（自然科學版），2007（3）：528-532.

[2]丁明.基于線性時序邏輯的業務流程驗證[J].西北大學學報（自然科學版），2012（2）：226-230.

[3]蔣慧，林東.UML狀態機的形式語義[J].軟件學報，2002（12）：2244-07.

[4]HUANG Xuemei. Modeling and Analysis for Hybrid Dynamic System of Production Line in Integrating Matlab Environment[J]. Modular Machine Tool & Automatic Manufacturing Technique， 2013， 5（5）：9-11.

[5]SEMANCO P， MARTON D. Simulation tools evaluation using theoretical manufacturing model[J]. Alta Polytechnical Hungarica，2013（2）：193-204.

[6]BECKERT， MEYERM， WINDTK. A manufacturing systems network model for thee valuation of complex manufacturing systems [J].International Journal of Productivity and Performance Management，2014（3）：324-340.

[7]LIJ. Modeling and analysis of manufacturing systems with par-allellines[J]. IEEE Transactions on Automatic Control，2004（10）：1824-1829.

[8]辛宗生，魏國豐.自動化制造系統[M].北京：北京大學出版社，2012.endprint