邏輯控制的安全檢驗(yàn)技術(shù)研究.pdf

1、隨著計(jì)算機(jī)越來越多的應(yīng)用于工業(yè)生產(chǎn)中，尤其是以DCS和PLC控制系統(tǒng)為代表的計(jì)算機(jī)控制系統(tǒng)的廣泛應(yīng)用。而且計(jì)算機(jī)控制系統(tǒng)常用于高溫高壓等臨界控制當(dāng)中。那么計(jì)算機(jī)控制系統(tǒng)的安全性就越來越引起人們的注意，在這其中邏輯控制因?yàn)槠湓谠O(shè)計(jì)過程中極有可能存在錯(cuò)誤，所以更加是保證安全的重中之重。在計(jì)算機(jī)控制系統(tǒng)正式應(yīng)用于生產(chǎn)過程前，必須要做安全分析和安全測(cè)試，保證邏輯控制的安全性。傳統(tǒng)的人工安全測(cè)試方法，根據(jù)安全條件逐條設(shè)計(jì)試驗(yàn)，十分消耗時(shí)間和資源，

2、而且測(cè)試結(jié)果也不能保證覆蓋了所有的工況下的安全性。所以雖然邏輯控制安全問題在世界范圍內(nèi)越來越受到重視，但是目前并沒有成熟和實(shí)用的方法。因此，開展邏輯控制的安全測(cè)試技術(shù)的研究具有重要的實(shí)用意義。
　　模型檢測(cè)技術(shù)是一種形式化驗(yàn)證技術(shù)，該技術(shù)在時(shí)序電路設(shè)計(jì)和通訊協(xié)議設(shè)計(jì)的驗(yàn)證領(lǐng)域得到了廣泛的應(yīng)用。模型檢測(cè)技術(shù)能夠高效、自動(dòng)并完全地對(duì)軟件進(jìn)行安全性分析。因此針對(duì)邏輯控制的安全性檢測(cè)的問題，本文主要對(duì)基于形式化模型檢測(cè)技術(shù)的邏輯控制的安全

3、性檢驗(yàn)進(jìn)行研究，完成了以下工作:
　　1.首先說明了形式化模型檢測(cè)的應(yīng)用背景以及發(fā)展?fàn)顩r，提出了基于模型檢測(cè)的邏輯控制安全性檢驗(yàn)的一般應(yīng)用框架。
　　2.說明邏輯控制進(jìn)行安全檢驗(yàn)前的建模過程，提出了針對(duì)控制對(duì)象中包含連續(xù)變量而采取的離散建模的原則和方法。
　　3.說明了形式化描述安全性質(zhì)的方法，提出針對(duì)邏輯控制的安全屬性描述方法。
　　4.選取適合于邏輯控制的模型檢測(cè)工具。針對(duì)帶連續(xù)變量的過程，采用了符號(hào)化模型檢

4、測(cè)工具SMV對(duì)其安全性分析;對(duì)于含有時(shí)間約束的控制過程，采用了自動(dòng)機(jī)模型檢測(cè)工具UPPAAL對(duì)其安全性分析。
　　5.對(duì)有無時(shí)間約束的邏輯控制的安全檢驗(yàn)分別舉例驗(yàn)證。
　　模型檢測(cè)方法對(duì)邏輯控制的狀態(tài)全覆蓋，完全自動(dòng)搜索的過程，既保證了邏輯控制的全覆蓋檢測(cè)避免微小錯(cuò)誤存在，又是自動(dòng)檢測(cè)過程大大減少了人力物力的消耗。本文最后使用這兩種檢測(cè)工具分別進(jìn)行的實(shí)例檢測(cè)過程，結(jié)果證明這兩種檢測(cè)方法適用于邏輯控制的安全性檢測(cè)。如果將模型檢