發(fā)布時(shí)間：2018-08-31 18:28

【摘要】：針對(duì)可編程邏輯控制器(PLC)程序在進(jìn)行Nu SMV模型檢測(cè)時(shí)需要手工對(duì)程序進(jìn)行建模,不僅浪費(fèi)人力且容易出錯(cuò)的問題,提出一種基于狀態(tài)轉(zhuǎn)移的PLC程序模型自動(dòng)化構(gòu)建方法。該方法首先分析結(jié)構(gòu)化文本(ST)語(yǔ)言特性并解析ST程序?yàn)槌橄笳Z(yǔ)法樹;其次,在抽象語(yǔ)法樹基礎(chǔ)上,根據(jù)不同的文法結(jié)構(gòu)進(jìn)行控制流分析生成控制流圖;然后,通過(guò)數(shù)據(jù)流分析得到程序依賴圖;最后,根據(jù)程序依賴圖生成Nu SMV的輸入模型。實(shí)驗(yàn)結(jié)果表明,所提方法實(shí)現(xiàn)了ST程序到Nu SMV輸入模型的自動(dòng)化構(gòu)建,并且構(gòu)建的Nu SMV輸入模型既保留了ST程序的原有特性又符合Nu SMV模型檢測(cè)工具輸入的規(guī)范,與傳統(tǒng)手工模型構(gòu)建方法相比,提高了模型生成的效率和準(zhǔn)確率。
[Abstract]:In order to solve the problem that the (PLC) program of programmable logic controller needs to model the Nu SMV model manually, which is not only a waste of manpower but also easy to make mistakes, an automatic construction method of PLC program model based on state transition is proposed. The method firstly analyzes the characteristics of structured text (ST) language and parses the ST program as an abstract syntax tree; secondly, on the basis of abstract syntax tree, the control flow is analyzed according to different grammar structures to generate the control flow graph. The program dependency graph is obtained by data flow analysis. Finally, the input model of Nu SMV is generated according to the program dependency graph. The experimental results show that the proposed method realizes the automatic construction of ST program to Nu SMV input model, and the constructed Nu SMV input model not only retains the original characteristics of ST program, but also conforms to the input specification of Nu SMV model checking tool. Compared with the traditional manual modeling method, the efficiency and accuracy of model generation are improved.
【作者單位】： 信息工程大學(xué);數(shù)學(xué)工程與先進(jìn)計(jì)算國(guó)家重點(diǎn)實(shí)驗(yàn)室;
【基金】：國(guó)家重點(diǎn)研發(fā)計(jì)劃項(xiàng)目(2016YFB0800203) 上海市科研計(jì)劃項(xiàng)目(14DZ1104800)~~
【分類號(hào)】：TP273

【相似文獻(xiàn)】

相關(guān)期刊論文 前10條

1 何青;駱翔宇;蘇開樂;;基于符號(hào)化模型檢測(cè)的對(duì)弈必勝策略驗(yàn)證[J];計(jì)算機(jī)工程與應(yīng)用;2008年17期

2 龍士工;王扣武;;多智體系統(tǒng)時(shí)序認(rèn)知規(guī)范的SPIN模型檢測(cè)[J];計(jì)算機(jī)工程與科學(xué);2011年12期

3 周從華;葉萌;王昌達(dá);劉志鋒;;多智體系統(tǒng)中約簡(jiǎn)狀態(tài)空間的限界模型檢測(cè)算法[J];軟件學(xué)報(bào);2012年11期

4 文中華;黃巍;劉任任;姜云飛;;模型檢測(cè)規(guī)劃中的狀態(tài)之間的可達(dá)關(guān)系研究[J];計(jì)算機(jī)學(xué)報(bào);2012年08期

5 駱翔宇;古天龍;董榮勝;;和與積數(shù)迷的符號(hào)化模型檢測(cè)[J];計(jì)算機(jī)科學(xué);2008年05期

6 文中華;黃巍;劉任任;姜云飛;;模型檢測(cè)規(guī)劃中的狀態(tài)分層方法[J];軟件學(xué)報(bào);2009年04期

7 吳立軍;駱翔宇;;基于固定內(nèi)存和狀態(tài)管理的模型檢測(cè)方法[J];計(jì)算機(jī)應(yīng)用研究;2011年06期

8 吳立軍,蘇開樂;多智體系統(tǒng)時(shí)態(tài)認(rèn)知規(guī)范的模型檢測(cè)算法[J];軟件學(xué)報(bào);2004年07期

9 寧正元;胡山立;賴賢偉;;交互時(shí)態(tài)信念邏輯及其模型檢測(cè)[J];南京大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年02期

10 朱新峰;李斌;吳俊;;模型檢測(cè)中的偏序簡(jiǎn)化[J];揚(yáng)州職業(yè)大學(xué)學(xué)報(bào);2009年04期

相關(guān)博士學(xué)位論文 前3條

1 劉志鋒;模型檢測(cè)中關(guān)鍵技術(shù)的研究及其應(yīng)用[D];南京大學(xué);2011年

2 尹良澤;基于SAT的組合遷移系統(tǒng)模型檢測(cè)技術(shù)研究[D];清華大學(xué);2014年

3 吳駿;多Agent聯(lián)盟規(guī)范系統(tǒng)研究[D];南京大學(xué);2011年

相關(guān)碩士學(xué)位論文 前10條

1 楊樹峰;基于統(tǒng)計(jì)模型檢測(cè)的無(wú)線傳感器網(wǎng)絡(luò)協(xié)議建模與分析[D];鄭州大學(xué);2015年

2 鄧楠軼;基于廣義可能性測(cè)度的模型檢測(cè)器GPoCheck的設(shè)計(jì)與實(shí)現(xiàn)[D];陜西師范大學(xué);2015年

3 王進(jìn)宗;不確定規(guī)劃中帶權(quán)值的觀察信息約簡(jiǎn)[D];湘潭大學(xué);2015年

4 程貝;基于抽象和學(xué)習(xí)的統(tǒng)計(jì)模型檢測(cè)研究[D];華東師范大學(xué);2016年

5 柯進(jìn);基于模型檢測(cè)的硬件驗(yàn)證在金融領(lǐng)域的研究與應(yīng)用[D];湖北工業(yè)大學(xué);2017年

6 楊志剛;基于μ演算的認(rèn)知難題符號(hào)化模型檢測(cè)[D];華僑大學(xué);2017年

7 吳小娟;并行完備模型檢測(cè)技術(shù)的研究[D];電子科技大學(xué);2013年

8 金怡愛;基于模型檢測(cè)方法的規(guī)劃[D];吉林大學(xué);2005年

9 高靜;面向環(huán)境演算系統(tǒng)的模型檢測(cè)算法的研究[D];南京航空航天大學(xué);2009年

10 廉智超;模型檢測(cè)在模型診斷領(lǐng)域中的應(yīng)用[D];吉林大學(xué);2007年

，

本文編號(hào)：2215797