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

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

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

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