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

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

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

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

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