[發(fā)明專利]一種基于中間語言的PLC程序驗(yàn)證系統(tǒng)

有效

• 申請?zhí)枺?/td>: 201810667143.6
• 申請日: 2018-06-26
• 公開（公告）號: CN109117362B
• 公開（公告）日: 2020-08-25
• 發(fā)明（設(shè)計(jì)）人: 史建琦;黃滟鴻;何積豐;李昂;蔡方達(dá)
• 申請（專利權(quán)）人: 華東師范大學(xué);上海豐蕾信息科技有限公司
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 北京辰權(quán)知識產(chǎn)權(quán)代理有限公司 11619
• 代理人: 劉廣達(dá)

1.一種基于中間語言的PLC程序驗(yàn)證系統(tǒng)，其特征在于，包括：

中間語言轉(zhuǎn)換模塊，用于對由一種或多種PLC語言編寫的目標(biāo)程序及其運(yùn)行環(huán)境配置進(jìn)行中間語言轉(zhuǎn)換，獲得對應(yīng)所述目標(biāo)程序及其運(yùn)行環(huán)境配置的統(tǒng)一的中間語言程序，其中，所述中間語言為基于CSP通信順序進(jìn)行語言擴(kuò)展的ICIL工業(yè)控制中間語言；

遷移系統(tǒng)構(gòu)造模塊，用于對中間語言程序進(jìn)行定義，并通過中間語言程序的定義、原子謂詞以及標(biāo)記函數(shù)，構(gòu)造中間語言程序的遷移系統(tǒng)；

性質(zhì)驗(yàn)證模塊，用于通過多種邏輯模型對所述遷移系統(tǒng)進(jìn)行性質(zhì)驗(yàn)證，從而對中間語言程序進(jìn)行性質(zhì)驗(yàn)證，得到性質(zhì)驗(yàn)證結(jié)果；

驗(yàn)證結(jié)果處理模塊，用于根據(jù)所述性質(zhì)驗(yàn)證結(jié)果以及對應(yīng)的評估標(biāo)準(zhǔn)對所述遷移系統(tǒng)進(jìn)行評估，對不滿足性質(zhì)驗(yàn)證的中間語言程序給出反例。

2.根據(jù)權(quán)利要求1所述的PLC程序驗(yàn)證系統(tǒng)，其特征在于，所述中間語言轉(zhuǎn)換模塊能夠轉(zhuǎn)換的一種或多種PLC語言包括：梯形圖語言、功能塊圖語言、順序功能圖語言、結(jié)構(gòu)化文本語言以及指令表語言。

3.根據(jù)權(quán)利要求2所述的PLC程序驗(yàn)證系統(tǒng)，其特征在于，通過所述中間語言轉(zhuǎn)換模塊對所述梯形圖語言、功能塊圖語言或順序功能圖語言進(jìn)行的中間語言轉(zhuǎn)換，包括：

將由梯形圖語言、功能塊圖語言或順序功能圖語言編寫的PLC程序轉(zhuǎn)換為PLCOpen XML文件；

對所述PLCOpen XML文件中的每類元素設(shè)計(jì)相應(yīng)的轉(zhuǎn)換規(guī)則，從而將由梯形圖語言、功能塊圖語言或順序功能圖語言編寫的PLC程序轉(zhuǎn)換為中間語言程序。

4.根據(jù)權(quán)利要求2所述的PLC程序驗(yàn)證系統(tǒng)，其特征在于，通過所述中間語言轉(zhuǎn)換模塊對所述結(jié)構(gòu)化文本語言、指令表語言進(jìn)行中間語言轉(zhuǎn)換，包括：

將由結(jié)構(gòu)化文本語言、指令表語言編寫的PLC程序解析為抽象語法樹；

對抽象語法樹中每一類語法元素設(shè)計(jì)轉(zhuǎn)換規(guī)則，從而將文本類編寫的PLC程序轉(zhuǎn)換為中間語言程序。

5.根據(jù)權(quán)利要求1所述的PLC程序驗(yàn)證系統(tǒng)，其特征在于，通過所述遷移系統(tǒng)構(gòu)造模塊對中間語言程序進(jìn)行定義包括：

對所述中間語言程序的程序模型進(jìn)行定義；

以及通過操作語義對中間語言程序狀態(tài)之間的遷移關(guān)系進(jìn)行定義。

6.根據(jù)權(quán)利要求5所述的PLC程序驗(yàn)證系統(tǒng)，其特征在于，所述中間語言程序模型包括：中間語言程序的程序狀態(tài)和初始程序狀態(tài)。

7.根據(jù)權(quán)利要求6所述的PLC程序驗(yàn)證系統(tǒng)，其特征在于，所述中間語言程序的程序狀態(tài)包括：中間語言程序的程序狀態(tài)集合和程序工作集合。

8.根據(jù)權(quán)利要求1所述的PLC程序驗(yàn)證系統(tǒng)，其特征在于，所述性質(zhì)驗(yàn)證模塊中的多種邏輯模型包括：時態(tài)邏輯、計(jì)算樹邏輯、霍爾邏輯以及分離邏輯。

9.根據(jù)權(quán)利要求1所述的PLC程序驗(yàn)證系統(tǒng)，其特征在于，所述驗(yàn)證結(jié)果處理模塊中所述對應(yīng)的評估標(biāo)準(zhǔn)為通過PLC安全評估標(biāo)準(zhǔn)設(shè)計(jì)的適用于所述性質(zhì)驗(yàn)證結(jié)果的評估標(biāo)準(zhǔn)。