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

【摘要】：針對可編程邏輯控制器(PLC)程序在進行Nu SMV模型檢測時需要手工對程序進行建模,不僅浪費人力且容易出錯的問題,提出一種基于狀態(tài)轉(zhuǎn)移的PLC程序模型自動化構(gòu)建方法。該方法首先分析結(jié)構(gòu)化文本(ST)語言特性并解析ST程序為抽象語法樹;其次,在抽象語法樹基礎(chǔ)上,根據(jù)不同的文法結(jié)構(gòu)進行控制流分析生成控制流圖;然后,通過數(shù)據(jù)流分析得到程序依賴圖;最后,根據(jù)程序依賴圖生成Nu SMV的輸入模型。實驗結(jié)果表明,所提方法實現(xiàn)了ST程序到Nu SMV輸入模型的自動化構(gòu)建,并且構(gòu)建的Nu SMV輸入模型既保留了ST程序的原有特性又符合Nu SMV模型檢測工具輸入的規(guī)范,與傳統(tǒng)手工模型構(gòu)建方法相比,提高了模型生成的效率和準確率。
[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é)工程與先進計算國家重點實驗室;
【基金】：國家重點研發(fā)計劃項目(2016YFB0800203) 上海市科研計劃項目(14DZ1104800)~~
【分類號】：TP273

【相似文獻】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

，

本文編號：2215797