基于時間自動機(jī)的時序約束活動異常監(jiān)測系統(tǒng)形式化驗證.pdf

1、物聯(lián)網(wǎng)被認(rèn)為是繼計算機(jī)、互聯(lián)網(wǎng)和移動通信網(wǎng)絡(luò)之后的第三次信息產(chǎn)業(yè)浪潮。物聯(lián)網(wǎng)通過傳感設(shè)備獲取“物”信息，并通過網(wǎng)絡(luò)實(shí)現(xiàn)信息交換，以實(shí)現(xiàn)智能化識別、定位、跟蹤監(jiān)控和管理的目的?；谖锫?lián)網(wǎng)的車間生產(chǎn)過程異常狀態(tài)監(jiān)控系統(tǒng)越來越多，這類系統(tǒng)通過采集生產(chǎn)車間的數(shù)據(jù)并進(jìn)行分析處理，以實(shí)現(xiàn)車間智能化管理從而提高企業(yè)的經(jīng)濟(jì)利益。但在生產(chǎn)車間監(jiān)控系統(tǒng)中，參與信息交互的對象包含人、機(jī)、物等不同類型對象，系統(tǒng)需要處理的是大量結(jié)構(gòu)異質(zhì)的信息，同時隨著車間規(guī)模的

2、擴(kuò)大，監(jiān)控也變得更加復(fù)雜，無法保證監(jiān)控系統(tǒng)投入運(yùn)行之前完全符合設(shè)計要求。因此，提出一種車間生產(chǎn)監(jiān)控系統(tǒng)建模和驗證方法，在系統(tǒng)實(shí)施之前使用形式化方法對生產(chǎn)車間監(jiān)控系統(tǒng)建模并驗證，盡早發(fā)現(xiàn)系統(tǒng)設(shè)計的不合理和不正確之處，顯得尤為必要。
　　本文以物聯(lián)網(wǎng)環(huán)境下離散生產(chǎn)車間異常監(jiān)測系統(tǒng)為研究背景，研究了基于時間自動機(jī)的時序約束活動異常監(jiān)測系統(tǒng)形式化驗證方法，利用時間自動機(jī)驗證方面的優(yōu)勢驗證監(jiān)測系統(tǒng)設(shè)計的有效性和完備性。本文首先綜述了復(fù)雜事件

3、檢測的國內(nèi)外研究現(xiàn)狀；分析了生產(chǎn)車間現(xiàn)場的若干特征，定義了基于時間自動機(jī)的生產(chǎn)車間現(xiàn)場模型，用狀態(tài)不變式中的時間約束刻畫操作人員等的自主隨機(jī)性，用狀態(tài)和變遷分別刻畫不同類型的活動，同時對生產(chǎn)對象的感知行為抽象表示；然后說明了不同的事件使用策略和消耗策略建模方法，分析了事件和事件約束模型構(gòu)造方法，并提出了復(fù)合事件模式采用若干時序相關(guān)事件操作符的時間自動機(jī)模型構(gòu)造方法，其中提出了控制模型時間自動機(jī)建模方法，控制模型減小了一個事件模式對應(yīng)自動

4、機(jī)模型的規(guī)模；接著為了簡化異常監(jiān)測時間自動機(jī)模型性質(zhì)驗證，建立了包含正常生產(chǎn)情況的輔助生產(chǎn)過程自動機(jī)模型；針對生產(chǎn)車間異常監(jiān)控系統(tǒng)的特點(diǎn)，提出從系統(tǒng)功能性、實(shí)時性、冗余性及未定義的異常行為四個方面驗證系統(tǒng)設(shè)計的正確性和完備性；最后使用時間自動機(jī)驗證工具UPPAAL，以粘合加工車間異常監(jiān)測為例，對提出的方法進(jìn)行了驗證。
　　本文的研究表明：時間自動機(jī)形式化方法能夠較好刻畫生產(chǎn)車間異常監(jiān)測系統(tǒng)的相關(guān)特性。利用時間自動機(jī)形式化建模及驗證