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

沈陽+齊德昱

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

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

中圖分類號：TP316 文獻(xiàn)標(biāo)識碼：A 文章編號：1007-9416（2017）05-0083-03

現(xiàn)今現(xiàn)代流水型多工位加工設(shè)備的控制系統(tǒng)存在以下不足：（1）系統(tǒng)設(shè)計開發(fā)思路仍然停留在“一機(jī)一程序”的時代（PC或PLC程序亦然）；（2）未能適應(yīng)除機(jī)械標(biāo)準(zhǔn)件以外其他自定義部件的快速替換；（3）機(jī)器控制代碼難以復(fù)用與重構(gòu)，存在不必要的重復(fù)或冗余；（4）勉強(qiáng)復(fù)用或擴(kuò)展現(xiàn)有代碼導(dǎo)致思路局限，可能帶來功能上的隱患；（5）與外部系統(tǒng)缺乏足夠豐富的交互接口，難以與新技術(shù)集成（如云計算，自診斷）；（6）缺乏領(lǐng)域?qū)Ｓ玫脑O(shè)計，開發(fā)和仿真測試工具。

總而言之，其根源在于缺乏一個以形式化理論支持的領(lǐng)域?qū)Ｓ密浖蚣堋Ｎ覀兠鎸Φ膯栴}是：一個怎樣的程序結(jié)構(gòu)（框架）才能滿足現(xiàn)代流水型加工設(shè)備控制系統(tǒng)的需要？作為這類設(shè)備的設(shè)計與制造商，需要不斷根據(jù)產(chǎn)品及用戶的需求，來設(shè)計與生產(chǎn)各種各樣的設(shè)備，因此有必要研發(fā)一種通用設(shè)備服務(wù)來支持實(shí)現(xiàn)這種流水型多工位系統(tǒng)的要求，并具有很強(qiáng)的開放性和擴(kuò)展性。如果采用UML的方式對該系統(tǒng)建模，盡管其靜態(tài)語義由元模型給出，但其動態(tài)語義卻十分模糊，不利于對其所描述的需求進(jìn)行形式化的驗(yàn)證和確認(rèn)，本文將采用線性時序邏輯對流水型加工設(shè)備控制系統(tǒng)中的部分功能進(jìn)行形式化建模和驗(yàn)證，以保證其無二義性以及準(zhǔn)確性[1]。

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

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

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

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

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

我們用這樣一個四元組來表示這個順序圖：SD=。Obj、 Msg、 Loc分別表示順序圖中對象的集合、消息的集合以及位點(diǎn)的集合；F則表示從消息到位點(diǎn)的函數(shù)，即，其中，s表示發(fā)送消息，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對該順序圖主要事件進(jìn)行形式化表示的語義描述如下：

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

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

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

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

該狀態(tài)圖的靜態(tài)語義形式化如下：

圖2所示的狀態(tài)，設(shè)轉(zhuǎn)換動作為Translate，狀態(tài)集類為States，則可形式化如下：

對應(yīng)的部分語義為：

3 可達(dá)性驗(yàn)證

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

對于動作（包括上述的原子動作或復(fù)雜動作），如果存在解釋和，使?jié)M足，則稱動作是可實(shí)現(xiàn)的。

狀態(tài)的可達(dá)性：（1）如果動作滿足以下條件，則稱狀態(tài)是可達(dá)的；（2）如果動作是可實(shí)現(xiàn)的，則狀態(tài)是可達(dá)的；（3）假設(shè)有動作和，如果和都可實(shí)現(xiàn)，則狀態(tài)是可達(dá)的。

例如上述形式化中的，有，由于都是可實(shí)現(xiàn)的，所以是可實(shí)現(xiàn)的，可知狀態(tài)是可達(dá)的。狀態(tài)圖中具備可達(dá)性的狀態(tài)有：INITIALIZE， DEMAND， ACTIVE， COMPLETE， FINISH。

4 結(jié)語

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

參考文獻(xiàn)

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

[2]丁明.基于線性時序邏輯的業(yè)務(wù)流程驗(yàn)證[J].西北大學(xué)學(xué)報（自然科學(xué)版），2012（2）：226-230.

[3]蔣慧，林東.UML狀態(tài)機(jī)的形式語義[J].軟件學(xué)報，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]辛宗生，魏國豐.自動化制造系統(tǒng)[M].北京：北京大學(xué)出版社，2012.endprint