【摘要】：符號約束描述了程序中的變量關(guān)系,被廣泛運(yùn)用于模型檢測、符號執(zhí)行等程序的靜態(tài)分析方法中。將符號約束應(yīng)用于可編程邏輯控制器(PLC)程序的正確性驗(yàn)證,能夠發(fā)現(xiàn)程序中的邏輯錯誤。人工計(jì)算符號約束不僅冗雜枯燥,而且錯誤率高。針對語句表形式的PLC程序,提出一種基于符號約束的正確性驗(yàn)證方法,通過分析PLC源代碼的控制流及數(shù)據(jù)流,構(gòu)造程序的控制流圖并將其轉(zhuǎn)換為靜態(tài)單賦值形式的三地址碼,最后使用迭代計(jì)算的方法求出每個變量的符號約束。
[Abstract]:Symbolic constraints describe variable relationships in programs and are widely used in static analysis of programs such as model checking, symbolic execution, and so on. The logic errors in the program can be found by applying the symbolic constraint to the correctness verification of the (PLC) program of the programmable logic controller. The symbol constraint of manual calculation is not only boring, but also has high error rate. This paper presents a correctness verification method based on symbolic constraints for PLC programs in the form of statement tables. By analyzing the control flow and data flow of the PLC source code, the control flow diagram of the program is constructed and converted into three address codes in the form of static single assignment. Finally, the symbolic constraints of each variable are obtained by iterative computation.
【作者單位】： 合肥電子工程學(xué)院;
【分類號】：TP273

【相似文獻(xiàn)】

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

1 譚華;王建軍;陳蕭;;PLC程序在數(shù)控機(jī)床故障診斷中的應(yīng)用[J];無錫商業(yè)職業(yè)技術(shù)學(xué)院學(xué)報(bào);2006年06期

2 許云理;;PLC程序在數(shù)控機(jī)床故障診斷中的應(yīng)用[J];制造技術(shù)與機(jī)床;2006年10期

3 張淑俠;;PLC程序的可讀性研究[J];新課程學(xué)習(xí)(中);2011年12期

4 孫建華,高廣章,蔣志強(qiáng),施進(jìn)發(fā);程序分析法在產(chǎn)線平衡中的應(yīng)用[J];機(jī)械設(shè)計(jì)與制造;2005年05期

5 龔仲華;802S/C夾緊/松開PLC程序的改進(jìn)[J];制造技術(shù)與機(jī)床;2005年11期

6 寧曉東;廣鋼4號高爐PLC程序改進(jìn)[J];冶金叢刊;2002年01期

7 劉海濤;;合成氣壓縮機(jī)PLC程序改進(jìn)[J];化工自動化及儀表;2013年02期

8 袁力強(qiáng);SN368回放處理程序分析[J];石油儀器;1993年02期

9 劉建功;范力e，

本文編號：2197590