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

沈陽(yáng)+齊德昱

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

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

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

現(xiàn)今現(xiàn)代流水型多工位加工設(shè)備的控制系統(tǒng)存在以下不足：（1）系統(tǒng)設(shè)計(jì)開(kāi)發(fā)思路仍然停留在“一機(jī)一程序”的時(shí)代（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)致思路局限，可能帶來(lái)功能上的隱患；（5）與外部系統(tǒng)缺乏足夠豐富的交互接口，難以與新技術(shù)集成（如云計(jì)算，自診斷）；（6）缺乏領(lǐng)域?qū)Ｓ玫脑O(shè)計(jì)，開(kāi)發(fā)和仿真測(cè)試工具。

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

1 使用線(xiàn)性時(shí)序邏輯語(yǔ)法描述制卡流程

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

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

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

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

我們用這樣一個(gè)四元組來(lái)表示這個(gè)順序圖：SD=。Obj、 Msg、 Loc分別表示順序圖中對(duì)象的集合、消息的集合以及位點(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對(duì)該順序圖主要事件進(jìn)行形式化表示的語(yǔ)義描述如下：

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

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

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

制卡時(shí)，卡片首先進(jìn)行初始化操作，以確定是否準(zhǔn)備就緒，然后立即進(jìn)入DEMAND狀態(tài)。當(dāng)接到doServiceProcess事件時(shí)，接收到機(jī)器的ACK響應(yīng)后，進(jìn)入激活狀態(tài)（ACTIVE），ACTIVE無(wú)條件進(jìn)入ACK狀態(tài)。在ACK狀態(tài)中進(jìn)行等待阻塞，監(jiān)聽(tīng)機(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事件時(shí)，卡片也進(jìn)入FINISH狀態(tài)[6]。

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

圖2所示的狀態(tài)，設(shè)轉(zhuǎn)換動(dòng)作為T(mén)ranslate，狀態(tài)集類(lèi)為States，則可形式化如下：

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

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

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

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

狀態(tài)的可達(dá)性：（1）如果動(dòng)作滿(mǎn)足以下條件，則稱(chēng)狀態(tài)是可達(dá)的；（2）如果動(dòng)作是可實(shí)現(xiàn)的，則狀態(tài)是可達(dá)的；（3）假設(shè)有動(dòng)作和，如果和都可實(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é)語(yǔ)

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

參考文獻(xiàn)

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

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

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