使用TLA對(duì)一個(gè)工業(yè)級(jí)安全協(xié)議的建模實(shí)現(xiàn).pdf

1、目前越來(lái)越多的安全臨界系統(tǒng)被應(yīng)用到我們的日常生活中，以至于安全工程也越來(lái)越受到關(guān)注。在這種情況下，國(guó)際電子技術(shù)協(xié)會(huì)頒布了國(guó)際功能安全標(biāo)準(zhǔn)《IEC61508》。這套功能安全標(biāo)準(zhǔn)使用安全集成度來(lái)描述系統(tǒng)安全性，并推薦了很多形式化方法作為安全檢證的手段。
　　形式化方法主要檢驗(yàn)系統(tǒng)三個(gè)方面的屬性是否滿足，即：安全性，活性以及公平性。但是在實(shí)際操作中面臨三個(gè)主要問(wèn)題：其一，驗(yàn)證結(jié)論很難使用功能安全標(biāo)準(zhǔn)中安全集成度的度量標(biāo)準(zhǔn)進(jìn)行描述；其二，

2、形式化方法對(duì)系統(tǒng)所處的環(huán)境以及人機(jī)交互方面的處理比較薄弱，需要人為地針對(duì)性的加以處理；其三，絕大多數(shù)形式化方法是基于狀態(tài)枚舉原理的，無(wú)法回避狀態(tài)爆炸問(wèn)題。
　　在論文探討使用TLA對(duì)系統(tǒng)進(jìn)行建模與分析之前，我們首先簡(jiǎn)單地介紹了一下TLA以及建模所需要的基礎(chǔ)數(shù)學(xué)知識(shí)。隨后我們?cè)谡撐闹刑岢隽艘环N分治策略用于對(duì)系統(tǒng)規(guī)格說(shuō)明進(jìn)行抽象簡(jiǎn)化。其基本思想是將復(fù)雜的系統(tǒng)簡(jiǎn)單化，先提出一個(gè)最簡(jiǎn)單抽象的概念模型，然后逐層細(xì)化各個(gè)模塊，將系統(tǒng)的功能和數(shù)

3、據(jù)交互添加到這些模塊中去。在這一過(guò)程中，我們由簡(jiǎn)入繁地反向分析哪些系統(tǒng)因素是安全相關(guān)的，哪些系統(tǒng)因素是可以在將來(lái)的模型中簡(jiǎn)化甚至省略掉的。這對(duì)簡(jiǎn)化系統(tǒng)復(fù)雜度起到了相當(dāng)關(guān)鍵的作用。同時(shí)，我們可以逐漸分析出系統(tǒng)需要滿足哪些安全性，活性以及公平性屬性。為了更好地配合TLA建模，我們?cè)诜种尾呗灾羞€提出了針對(duì)模塊功能分析的模塊狀態(tài)機(jī)（Module State Machine）機(jī)制。分治簡(jiǎn)化結(jié)束后，其模塊狀態(tài)機(jī)可以很容易地轉(zhuǎn)化為T(mén)LA模型。