PLC系統(tǒng)及其FBD編程語(yǔ)言的形式化建模與實(shí)時(shí)性驗(yàn)證.pdf

1、可編程邏輯控制器（PLC）是一類擁有感應(yīng)器和觸發(fā)器的特殊裝置，它能夠?qū)崿F(xiàn)對(duì)外界的控制、模擬和交互的功能，隨著PLC系統(tǒng)在各個(gè)領(lǐng)域的廣泛應(yīng)用，PLC指令集的不斷擴(kuò)展，系統(tǒng)變得越來(lái)越冗雜，由于PLC系統(tǒng)通常對(duì)可靠性和實(shí)時(shí)性方面需求嚴(yán)格，因此尋找一套有效的系統(tǒng)建模和驗(yàn)證的方法是非常有必要的。
　　本文通過(guò)研究發(fā)現(xiàn)以往在保證 PLC系統(tǒng)設(shè)計(jì)正確性的方法中存在很多缺點(diǎn)。比如傳統(tǒng)的PLC程序驗(yàn)證測(cè)試，依賴于大量的人工勞動(dòng)，在整個(gè)調(diào)試過(guò)程中沒(méi)有

2、一條準(zhǔn)確的反饋信息，最主要是人為測(cè)試無(wú)法發(fā)現(xiàn)全部的邏輯錯(cuò)誤，比如競(jìng)態(tài)和死鎖。形式化方法是以數(shù)學(xué)理論為基礎(chǔ)的特殊方法，它可以采用遍歷的特點(diǎn)的來(lái)驗(yàn)證系統(tǒng)的性質(zhì)和實(shí)事性等，而且可以給出反例的路徑。
　　因此本文分析了PLC系統(tǒng)下標(biāo)準(zhǔn)化的FBD編程語(yǔ)言的語(yǔ)法和語(yǔ)義，采用面向模型的形式化方法提出一套相對(duì)完整的從 FBD語(yǔ)言各指令到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換步驟。在完成了對(duì)控制器編程語(yǔ)言指令的建模后，還抽象建模出PLC系統(tǒng)其余三大模塊（協(xié)調(diào)模塊、外部環(huán)

3、境模塊、循環(huán)控制模塊）的時(shí)間自動(dòng)機(jī)表示形式。在模型選取方面放棄了原有只關(guān)心功能性（例如系統(tǒng)經(jīng)過(guò)一些操作，最終到達(dá)一些狀態(tài)）的目標(biāo)模型（petri或 smv等），采用了時(shí)間自動(dòng)機(jī)模型，添加了對(duì)時(shí)間因子的建模，著重考慮了系統(tǒng)實(shí)時(shí)性的因素。
　　在完成對(duì)單一指令模塊的建模之后，本文結(jié)合FBD順序控制特點(diǎn)和程序邏輯的相關(guān)概念，給出了模塊組合算法，并通過(guò)UPPAAL工具證明了該算法的可靠性。文章的最后，通過(guò)傳送帶實(shí)例，將原系統(tǒng)統(tǒng)一建模為時(shí)間