隨著自動化技術的發(fā)展,工業(yè)控制系統(tǒng)在工業(yè)、能源、交通、水利等領域得到了廣泛的運用。它在我國基礎設施的自動化運轉中發(fā)揮著重要作用,尤其是在一些安全攸關領域,例如核設施、航空航天等。因此,工業(yè)控制系統(tǒng)的控制軟件一般都需要經(jīng)過嚴格的、系統(tǒng)的測試,以確�？刂栖浖馁|(zhì)量。然而隨著軟件規(guī)模的不斷上升,測試的難度也相應地不斷增加。加之測試技術本身具有一定的局限性,例如不能保證發(fā)現(xiàn)軟件中所有的漏洞,也不能發(fā)現(xiàn)軟件邏輯實現(xiàn)上的錯誤等。這使得測試技術并不能勝任安全攸關領域中控制軟件的驗證工作。而形式化驗證技術能夠以數(shù)學的方式證明系統(tǒng)在設計或實現(xiàn)上的正確性,因此近些年來受到了安全攸關領域的青睞,是學術界和工業(yè)界都十分關注的研究熱點。IEC 61131-3是工控領域中關于控制軟件編程語言的國際標準。結構化文本（ST,即Structured Text）是其提供的一種高級文本編程語言。與標準中的其他語言不同,ST允許用戶使用數(shù)組、結構體等數(shù)據(jù)結構和分支、循環(huán)、函數(shù)調(diào)用等控制結構。因此它是用戶實現(xiàn)具有復雜控制邏輯或算法的控制軟件時的首選編程語言。工業(yè)化和信息化的深度融合使得控制軟件越來越復雜,為ST語言的使用提供了... 

【文章來源】：華東師范大學上海市 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：81 頁

【學位級別】：碩士

【文章目錄】：
摘要
Abstract
第一章 緒論
    1.1 研究背景
    1.2 研究現(xiàn)狀
        1.2.1 工業(yè)控制領域中模型檢查技術的研究現(xiàn)狀
        1.2.2 工控編程語言形式化語義的研究現(xiàn)狀
    1.3 本文研究內(nèi)容及主要貢獻
        1.3.1 研究內(nèi)容
        1.3.2 主要貢獻
    1.4 本文組織結構
第二章 預備知識
    2.1 工業(yè)控制系統(tǒng)簡介
        2.1.1 典型體系結構
        2.1.2 基本運行方式
    2.2 IEC61131-3標準概述
        2.2.1 標準軟件模型
        2.2.2 標準編程語言
    2.3 模型檢查技術概述
        2.3.1 相關術語
        2.3.2 使用模型檢查的一般步驟
        2.3.3 優(yōu)缺點分析
    2.4 K框架簡介
        2.4.1 語法定義
        2.4.2 語義定義
    2.5 本章小結
第三章 結構化文本程序的形式化驗證方法概述
    3.1 基于模型檢查的形式化驗證方法概述
    3.2 基于K框架的形式化操作語義概述
    3.3 本章小結
第四章 基于模型檢查的結構化文本程序形式化驗證方法
    4.1 行為模型的形式化定義
        4.1.1 定義
        4.1.2 相關概念
    4.2 形式化建模方法
        4.2.1 ST程序的圖形化表示方式
        4.2.2 從ICFG中構建形式化模型BM
        4.2.3 變量狀態(tài)分析
    4.3 LTL性質(zhì)驗證方法
        4.3.1 線性時態(tài)邏輯
        4.3.2 基于自動機的LTL驗證方法
    4.4 本章小結
第五章 基于K框架的結構化文本語言形式化操作語義
    5.1 形式化操作語義KST
        5.1.1 語法
        5.1.2 形式化操作語義
        5.1.3 IEC61131-3標準中存在的二義性描述
    5.2 KST的正確性測試
    5.3 本章小結
第六章 結構化文本程序形式化驗證方法在實際生產(chǎn)中的應用
    6.1 工具實現(xiàn)
    6.2 齒輪生產(chǎn)線上的質(zhì)檢工位
    6.3 本章小結
第七章 總結
    7.1 工作總結
    7.2 未來工作展望
參考文獻
致謝
作者在學期間所取得的科研成果


【參考文獻】：
期刊論文
[1]模型檢測中狀態(tài)爆炸問題研究綜述[J]. 侯剛,周寬久,勇嘉偉,任龍濤,王小龍.  計算機科學. 2013(S1)
[2]近年重大工業(yè)控制系統(tǒng)安全事件一覽[J].   中國信息安全. 2012(03)



本文編號：3172445