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

1、物聯(lián)網(wǎng)被認(rèn)為是繼計(jì)算機(jī)、互聯(lián)網(wǎng)和移動(dòng)通信網(wǎng)絡(luò)之后的第三次信息產(chǎn)業(yè)浪潮。物聯(lián)網(wǎng)通過傳感設(shè)備獲取“物”信息，并通過網(wǎng)絡(luò)實(shí)現(xiàn)信息交換，以實(shí)現(xiàn)智能化識(shí)別、定位、跟蹤監(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)中，參與信息交互的對(duì)象包含人、機(jī)、物等不同類型對(duì)象，系統(tǒng)需要處理的是大量結(jié)構(gòu)異質(zhì)的信息，同時(shí)隨著車間規(guī)模的

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

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

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