發(fā)布時(shí)間：2021-05-06 18:54

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

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

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

【學(xué)位級(jí)別】：碩士

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


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



本文編號(hào)：3172445