導(dǎo)航：安全管理網(wǎng)>> 安全論文>> 綜合安全論文>>正文

互斥協(xié)議的安全性分析

文檔作者：趙夢龍１唐鄭熠２萬良3 韋立４文檔來源：１．貴州職業(yè)技術(shù)學(xué)院信息技術(shù)系２．福建工程學(xué)院 3．貴州大學(xué)計算機科學(xué)與技術(shù)學(xué)院４．貴州師范大學(xué)數(shù)學(xué)與計算機科學(xué)學(xué)院			點擊數(shù)：
下載地址：點擊這里	文件大小： 812.40 KB 共3頁	文檔格式： PDF	下載點數(shù)： 1 點（VIP免費）

全屏查看

內(nèi)容預(yù)覽 [文件共3頁]

本文件共3頁，如需編輯使用，請下載。

注：預(yù)覽效果可能會出現(xiàn)部分文字亂碼（如口口口）、內(nèi)容顯示不全等問題，下載是正常的。

	文件大?。?12.40 KB 共3頁文件格式：PDF 下載點數(shù)：1 點（VIP會員免費）

下一篇：基于LEACH協(xié)議的安全節(jié)能路由算法研究

上一篇：基于匹配策略的安全協(xié)議重構(gòu)分析

文本預(yù)覽

僅提取頁面文字內(nèi)容，供快速閱讀使用。

收稿日期： ２0１４-0４-１１; 修回日期： ２0１４-06-09　　基金項目： 國家自然科學(xué)基金資助項目(6１30900);貴州省自然科學(xué)基金資助項目( Ｊ
［２0１１］２3２８);福建工程學(xué)院科研啟動基金資助項目(GＹ-Ｚ１3１１２)
作者簡介：趙夢龍(１9８１-),男(通信作者),河南駐馬店人,講師,碩士,主要研究方向為形式化方法、信息安全等( ｈａppｙboｙｚ＿ｈａo@１２6．coｍ);
唐鄭熠(１9８４-),男,福建福州人,講師,博士,主要研究方向為形式化方法、服務(wù)計算;萬良(１9７４-),男,貴州貴陽人,副教授,博士(后),主要研究方
向為形式化方法、信息安全;韋立(１9８１-),男,廣西都安人,副教授,博士,主要研究方向為可計算性與計算復(fù)雜性．
互斥協(xié)議的安全性分析*
趙夢龍１, 唐鄭熠２, 萬　良3, 韋　立４
(１．貴州職業(yè)技術(shù)學(xué)院信息技術(shù)系, 貴陽5500２3; ２．福建工程學(xué)院信息科學(xué)與工程學(xué)院, 福州350１１８; 3．貴
州大學(xué)計算機科學(xué)與技術(shù)學(xué)院, 貴陽5500２3; ４．貴州師范大學(xué)數(shù)學(xué)與計算機科學(xué)學(xué)院, 貴陽55000４)
摘　要： 安全性和活性是兩大基本的系統(tǒng)屬性,對于指導(dǎo)系統(tǒng)的設(shè)計與驗證具有重要意義。通過對它們原始定
義的形式化梳理,發(fā)現(xiàn)其缺乏對狀態(tài)序列的具體約束。針對這一問題,使用對系統(tǒng)動作刻畫更完善的行為時序
邏輯進(jìn)行了重定義,加入了初始狀態(tài)和轉(zhuǎn)移條件的約束。以此為基礎(chǔ),對互斥這一并發(fā)系統(tǒng)的典型屬性進(jìn)行了
形式化的分析,由此說明如何判斷一個屬性是否滿足安全性或活性的定義。該技術(shù)為實現(xiàn)系統(tǒng)性質(zhì)的自動推理
與驗證提供了形式化基礎(chǔ)。
關(guān)鍵詞： 互斥協(xié)議; 屬性分類; 安全性; 活性; 行為時序邏輯
中圖分類號： ＴＰ309．１　　　文獻(xiàn)標(biāo)志碼： Ａ　　　　　文章編號： １00１-3695(２0１5)05-１４８6-03
ｄoｉ：１0．3969/j．ｉｓｓｎ．１00１-3695．２0１5．05．05２
Sａｆｅｔｙ ａｎａｌｙｓｉｓ oｆ ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ pｒoｔocoｌ
ＺＨＡO Ｍｅｎg-ｌoｎg１, ＴＡＮG Ｚｈｅｎg-ｙｉ２ , ＷＡＮ Ｌｉａｎg3 , ＷＥＩ Ｌｉ４
(１.Ｄｅｐｔ.ｏfＩｎfｏrｍａｔｉｏｎ Ｔｅｃｈｎｏｌｏgy, Gｕｉｚｈｏｕ Ｖｏｃａｔｉｏｎａｌ Ｔｅｃｈｎｏｌｏgy Ｉｎsｔｉｔｕｔｅ, Gｕｉyａｎg 5500２3, Ｃｈｉｎａ; ２.Ｓｃｈｏｏｌ ｏfＩｎfｏrｍａｔｉｏｎ Ｓｃｉｅｎｃｅ ＆
Ｅｎgｉｎｅｅrｉｎg, Ｆｕｊｉａｎ Ｕｎｉvｅrsｉｔy ｏfＴｅｃｈｎｏｌｏgy, Ｆｕｚｈｏｕ 350１１８, Ｃｈｉｎａ; 3.Ｓｃｈｏｏｌ ｏfＣｏｍｐｕｔｅr Ｓｃｉｅｎｃｅ ＆Ｔｅｃｈｎｏｌｏgy, Gｕｉｚｈｏｕ Ｕｎｉvｅrsｉｔy, Gｕｉyａｎg
5500２3, Ｃｈｉｎａ; ４.Ｓｃｈｏｏｌ ｏfＭａｔｈｅｍａｔｉｃs ＆Ｃｏｍｐｕｔｅr Ｓｃｉｅｎｃｅ, Gｕｉｚｈｏｕ Ｎｏrｍａｌ Ｕｎｉvｅrsｉｔy, Gｕｉyａｎg 55000４, Ｃｈｉｎａ)
Ａｂsｔｒａｃｔ: Sａｆｅｔｙ ａｎｄ ｌｉｖｅｎｅｓｓ ａｒｅ ｔoｗ bａｓｉc ｔｙpｅｓ oｆ ｓｙｓｔｅｍ pｒopｅｒｔｙ ａｎｄ ａｒｅ ｖｅｒｙ ｕｓｅｆｕｌ ｆoｒ ｔｈｅ ｄｅｓｉgｎ ａｎｄ ｖｅｒｉｆｉcａｔｉoｎ oｆ ｓｙｓｔｅｍ．
Ｔｈｉｓ pａpｅｒ poｉｎｔｅｄ oｕｔ ｔｈｅ ｄｉｓａｄｖａｎｔａgｅ oｆ ｌａcｋｉｎg ｒｅｓｔｒｉcｔｓ ｔo ｓｔａｔｅ ｓｅｑｕｅｎcｅ ｉｎ ｔｈｅｉｒ oｒｉgｉｎａｌ ｄｅｆｉｎｉｔｉoｎ．Ｆoｒ ｔｈｉｓ pｒobｌｅｍ,
ｉｔ gａｖｅ ｒｅｄｅｆｉｎｉｔｉoｎ bｙ ｔｈｅ ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ ｗｈｉcｈ ｗａｓ ｍoｒｅ ｓｕｉｔａbｌｅ ｔo ｄｅｓcｒｉbｅ ｓｙｓｔｅｍ ａcｔｉoｎ．Ｔｈｅ ｎｅｗ ｆoｒｍａｌ ｄｅｆｉｎｉｔｉoｎ
ａｄｄｅｄ ｉｎｉｔｉａｌ ｓｔａｔｅ ａｎｄ coｎｓｔｒａｉｎｔ coｎｄｉｔｉoｎｓ ｆoｒ ｔｒａｎｓｆｅｒ．Oｎ ｔｈｉｓ bａｓｉｓ, ｉｔ ａｎａｌｙｚｅｄ ｔｈｅ ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ ｗｈｉcｈ ｗａｓ ｔｈｅ
ｔｙpｉcａｌ pｒopｅｒｔｙ oｆ coｎcｕｒｒｅｎｔ ｓｙｓｔｅｍ bｙ ｆoｒｍａｌ ｍｅｔｈoｄ．Ｉｔ ａｌｓo ｓｈoｗｓ ｔｈａｔ ｈoｗ ｔo jｕｄgｅ ｗｈｅｔｈｅｒ ａ pｒopｅｒｔｙ ｍｅｅｔｓ ｔｈｅ ｄｅｆｉｎｉｔｉoｎ
oｆ ｓａｆｅｔｙ oｒ ｌｉｖｅｎｅｓｓ．Ｔｈｉｓ ｔｅcｈｎoｌogｙ pｒoｖｉｄｅｄ ｔｈｅ ｆoｒｍａｌ bａｓｉc ｆoｒ ｔｈｅ ａｕｔoｍａｔｉc ｒｅａｓoｎｉｎg ａｎｄ ｖｅｒｉｆｉcａｔｉoｎ oｆ ｓｙｓｔｅｍ pｒopｅｒｔｙ．
Ｋｅy ｗｏｒｄs: ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ pｒoｔocoｌ; cｌａｓｓｉｆｉcａｔｉoｎ oｆ pｒopｅｒｔｉｅｓ; ｓａｆｅｔｙ; ｌｉｖｅｎｅｓｓ; ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ
O　引言
在操作系統(tǒng)中,為了保證程序最終執(zhí)行結(jié)果的正確性,必
須對并發(fā)執(zhí)行的各進(jìn)程進(jìn)行制約,以控制它們的執(zhí)行速度和對
資源的競爭［１］ 。進(jìn)程之間的間接制約在操作系統(tǒng)中通常叫互
斥,互斥是系統(tǒng)設(shè)計的關(guān)鍵問題之一［２］ ,它保證了相互沖突的
并發(fā)進(jìn)程可以共享資源。本文介紹了安全性與活性的形式化
定義,并針對其對狀態(tài)序列沒有作具體約束的不足,在行為時
序邏輯中對其進(jìn)行了重定義。根據(jù)安全性和活性的形式化定
義,對互斥協(xié)議的安全性進(jìn)行了形式化的分析,證明了互斥協(xié)
議是安全性而不是活性。
1　安全性與活性介紹
１9７７ 年,美國科學(xué)家Ｌａｍpoｒｔ 在驗證多線程程序正確性的
過程中,最早提出了將系統(tǒng)的性質(zhì)分為安全性和活性兩類,并
給出了它們的非形式化定義:
ａ)安全性:規(guī)定一些行為不會在系統(tǒng)中發(fā)生。
b)活性:規(guī)定一些行為必須在系統(tǒng)中發(fā)生。
2　安全性與活性的形式化定義
在１9８４ 年,Ｌａｍpoｒｔ 第一次對安全性進(jìn)行了形式化的定
義,隨后Ａｌpｅｒｎ 和Scｈｎｅｉｄｅｒ 又進(jìn)一步給出了活性的形式化定
義。Ｌａｍpoｒｔ ［3］ 是行為時序邏輯( ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ) 的創(chuàng)
立者,而安全性和活性的定義主要也是由他提出或啟發(fā)的,其
中的很多概念都被他加入到后來的行為時序邏輯當(dāng)中。這使
得安全性和活性能夠方便地使用行為時序邏輯進(jìn)行定義。因
此下面首先介紹安全性和活性的原始定義,然后再以行為時序
邏輯對它們進(jìn)行更精確的定義。
2．1　原始定義
系統(tǒng)的一次運行用系統(tǒng)狀態(tài)的無限序列來表示:
$1 s0 s１ s２
狀態(tài)之間的轉(zhuǎn)移是由于系統(tǒng)執(zhí)行了某個行為而發(fā)生的。
第3２ 卷第5 期
２0１5 年5 月　
計算機應(yīng)用研究
Ａppｌｉcａｔｉoｎ Ｒｅｓｅａｒcｈ oｆ Coｍpｕｔｅｒｓ
Ｖoｌ．3２ Ｎo．5
Ｍａｙ ２0１5
對于一次不可終止的運行,狀態(tài)序列顯然是無限的;而對于一
次可終止的運行,可以通過不斷地重復(fù)序列中的最后一個狀態(tài)
使其成為無限序列［４］ 。
同時,$［ｉ］ 1 sｉ,$［..ｉ］ 1 s0 s１ s２ sｉ －１ ,$［ ｉ..］ 1 sｉ sｉ ＋１
sｉ ＋２ 。對于兩個運轉(zhuǎn)α1 s0 s１ s２ sｉ －１ , β 1 sｉ ＋１ sｉ ＋２ sｉ ＋3 ,
αβ1 s0 s１ s２ sｉ －１ sｉ ＋１ sｉ ＋２ sｉ ＋3 。
一個屬性被看做是運轉(zhuǎn)的集合,其中所包含的元素是滿足
該屬性的運轉(zhuǎn)［5］ 。如果說系統(tǒng)滿足一個屬性,那么該系統(tǒng)所
有可能的運轉(zhuǎn)都包含在屬性所描述的集合中。
定義１　屬性(pｒopｅｒｔｙ) ［6］ 。一個屬性Ｐ 被看做是所有符
合滿足該屬性的運轉(zhuǎn)的集合,一個運轉(zhuǎn)滿足Ｐ 等價于該運轉(zhuǎn)
屬于Ｐ 所表示的集合,即α(Ｐ$｜＝Ｐ。
用Ｓ 表示所有系統(tǒng)狀態(tài)的集合;用Ｓ*表示所有系統(tǒng)狀態(tài)
有限序列的集合,系統(tǒng)狀態(tài)的有限序列用來表示系統(tǒng)一次運行
中的部分時刻;用Ｓw 表示所有系統(tǒng)狀態(tài)無限序列的集合,系統(tǒng)
狀態(tài)的無限序列用來表示系統(tǒng)一次運行。對于有限運轉(zhuǎn)$(
Ｓ*,｜$｜表示它的長度。
安全性的定義是一些“ 壞的事情” 不會發(fā)生,因此如果屬
性Ｐ 是一個安全性,那么當(dāng)一個運轉(zhuǎn)不滿足屬性Ｐ 的約束時,
那么在運轉(zhuǎn)中的某些點上發(fā)生了“壞的事情”。“ 壞的事情” 一
旦發(fā)生就不可補救,因為安全性要求的是“ 壞的事情” 永遠(yuǎn)都
不會發(fā)生。
定義２　安全性( ｓａｆｅｔｙ) ［5］ 。屬性Ｐ 是一個安全性,當(dāng)且
僅當(dāng)($:$(Ｓw:$｜≠Ｐ  (ｉ: ｉ≥0: (β: β(Ｓw: $［..
ｉ］β｜≠Ｐ)))。
安全性的含義是:安全性Ｐ 中的所有運轉(zhuǎn)的任意前綴都
可以被擴(kuò)展為一個或多個屬于Ｐ 的無限運轉(zhuǎn)。這個定義并沒
有對“壞的事情” 作出具體限制,但它一定是一個獨立的原子
行為,因為一旦一個運轉(zhuǎn)中出現(xiàn)了“壞的事情”,那么一定是在
一個可確認(rèn)的點發(fā)生的。
活性的定義是在系統(tǒng)運行的過程中,“ 好的事情” 最終會
發(fā)生。活性要求系統(tǒng)運行到任何時刻都存在著發(fā)生“ 好的事
情”的可能,無論過去“ 好的事情” 是否發(fā)生,至少要存在未來
發(fā)生的可能。
定義3　活性( ｌｉｖｅｎｅｓｓ) ［5］ 。屬性Ｐ 是一個活性,當(dāng)且僅
當(dāng)(α: α(Ｓ*: (β: β(Ｓw: αβ｜＝Ｐ))。
活性的含義是:系統(tǒng)中的任意有限狀態(tài)序列都可以被擴(kuò)展
為一個或多個屬于Ｐ 的無限序列。這個定義同樣沒有對“ 好
的事情”作出具體的規(guī)定,甚至沒有限制它必須是一個獨立的
原子行為。但只要求“好的事情”最終會發(fā)生,但不是一直( ａｌｗａｙｓ)
發(fā)生。
2．2　基于行為時序邏輯的形式化定義
在安全性與活性的原始定義中,對于無限序列集合Ｓw 和
有限序列集合Ｓ*并沒有作出具體的約束。然而一個系統(tǒng)的運
行并不是隨意,系統(tǒng)的初始狀態(tài)和狀態(tài)之間的轉(zhuǎn)移是存在著限
制的［6］ 。因此, 本文在行為時序邏輯中對其進(jìn)行更嚴(yán)格的
定義。
下面首先簡要介紹一些ＴＬＡ 中的定義［７ ～9］ 。
定義４　行為( ａcｔｉoｎ)。由變量、原本變量及常量符號組
成的布爾表達(dá)式。變量與當(dāng)前狀態(tài)相關(guān),原本變量與下一狀態(tài)
相關(guān)。
定義5　啞步(ｓｔｕｔｔｅｒｉｎg ｓｔｅpｓ)。啞步是一種特殊的行為,
在該行為發(fā)生后,系統(tǒng)中所有變量的值都保持不變。
定義6　標(biāo)記轉(zhuǎn)移系統(tǒng):一個標(biāo)記轉(zhuǎn)移系統(tǒng)T＝(Ｓ, Ｉ, ,
%),其中:
ａ)系統(tǒng)中的所有變量的一次有效賦值稱為一個狀態(tài)s,所
有的狀態(tài)(即所有可能的賦值)構(gòu)成狀態(tài)集合,記為Ｓ。
b)初始狀態(tài)ＩＳ。
c) 是所有行為構(gòu)成的集合。
ｄ)%Ｓ × ×Ｓ。
定義７　運轉(zhuǎn)(ｒｕｎ)。運轉(zhuǎn)是由無限或有限多個狀態(tài)組成
的序列,可以被看做是系統(tǒng)的一次運行:$1 s0
Ａ
→
0 s１
Ａ
→
１
s２ ,其中s0(Ｉ,Ａｉ( ,(sｉ, Ａｉ, sｉ ＋１ )(%。由于ＴＬＡ 引入了啞
步,有限長的運轉(zhuǎn)可以通過啞步擴(kuò)展為無限長的運轉(zhuǎn)。此外,
本文定義:$［ ｉ］ 1 sｉ,$［..ｉ］ 1 s0
Ａ
→
0 s１
Ａ
→
１ s２
Ａｉ
→
－１ sｉ －１ ,
(［ｉ..］ 1sｉ
Ａ
→
ｉ sｉ ＋１
Ａｉ
→
＋１ sｉ ＋２ 。
下面是在行為時序邏輯中重新定義表示系統(tǒng)運行集合的
符號:
定義８　系統(tǒng)運行的集合。對于一個標(biāo)記轉(zhuǎn)移系統(tǒng)T＝
(Ｓ,Ｉ, ,%),一個有限的運轉(zhuǎn)$表示系統(tǒng)的一次未終止的運
行,而無限的運轉(zhuǎn)$表示系統(tǒng)的一次運行,有如下標(biāo)記:
ａ)T*
$ 表示滿足標(biāo)記轉(zhuǎn)移系統(tǒng)T 的有限運轉(zhuǎn)的集合,其中
s0(Ｉ,Ａｉ( ,(sｉ, Ａｉ, sｉ ＋１ )(%。
b)Tw
$ 表示滿足標(biāo)記轉(zhuǎn)移系統(tǒng)T 的無限運轉(zhuǎn)的集合,其中
s0(Ｉ,Ａｉ( ,(sｉ, Ａｉ, sｉ ＋１ )(%。
c)(Ｓ, )*
$ 表示有限運轉(zhuǎn)的集合,其中Ａｉ( ,( sｉ, Ａｉ,
sｉ ＋１ )(%。
ｄ)(Ｓ, ) w
$ 表示無限運轉(zhuǎn)的集合,其中Ａｉ( ,( sｉ, Ａｉ,
sｉ ＋１ )(%。
T*
$ 和Tw
$ 表示系統(tǒng)從初始狀態(tài)開始的運行,而( Ｓ, )*
$ 和
(Ｓ, ) w
$ 表示系統(tǒng)從任意狀態(tài)開始的運行。
定義9　安全性。屬性Ｐ 是一個安全性,當(dāng)且僅當(dāng)($:
$(Tw
$: $｜≠Ｐ  (ｉ: ｉ≥0: (β: β(( Ｓ, ) w
$: $［..ｉ］ β｜≠
Ｐ)))。
定義１0　活性。屬性Ｐ 是一個活性,當(dāng)且僅當(dāng)(α: α(
T*
$: (β: β((Ｓ, ) w
$: αβ｜＝Ｐ))。
新的定義是為安全性和活性加入了初始狀態(tài)和狀態(tài)間轉(zhuǎn)
移關(guān)系的限制,將描述的運轉(zhuǎn)限定在符合系統(tǒng)基本要求的范圍
內(nèi),因為只有這樣的運轉(zhuǎn)對于系統(tǒng)而言才有意義。
根據(jù)安全性的定義可知,如果一個屬性Ｐ 不是安全性,那
么就是滿足^($·$(Tw
$: $｜≠Ｐ (ｉ: ｉ≥0: (β: β(
(Ｓ, ) w
$: $［..ｉ］β｜≠Ｐ))),即:$·$(Ｓw: ($｜≠Ｐ)∧(ｉ:
ｉ≥0: β: β(Ｓw: $［..ｉ］β｜＝Ｐ)。
根據(jù)活性的定義可知,如果一個屬性Ｐ 不是活性,那么就
是滿足^(α: α(T*
$: (β: β((Ｓ, ) w
$: αβ｜＝Ｐ)),即α:
α(T*
$: (β: β((Ｓ, ) w
$: αβ｜≠Ｐ)。
3　互斥協(xié)議的安全性
3．1　互斥概述
現(xiàn)代計算機系統(tǒng)的中心方案包括多道程序設(shè)計、多處理和
分布式處理,這些方案的基礎(chǔ)以及操作系統(tǒng)設(shè)計的基礎(chǔ)是并發(fā)
第5 期 趙夢龍,等：互斥協(xié)議的安全性分析 ·１４?。福贰?#183;　
　　
的,并發(fā)進(jìn)程可以按照多種方式進(jìn)行交互。系統(tǒng)中的眾多交互
進(jìn)程可能需要競爭使用資源,如對Ｉ/O 設(shè)備的訪問、主存中的
一塊空間或者一個文件等。此類交互中產(chǎn)生的重要問題就是
互斥。
互斥的定義通常為［１0］ :一組并發(fā)進(jìn)程中的一個或多個程
序段,因共享某一公有資源而導(dǎo)致它們必須以一個不允許交叉
執(zhí)行的單位執(zhí)行。也就是說,不允許兩個以上的共享該資源的
并發(fā)進(jìn)程同時進(jìn)入臨界區(qū)。互斥技術(shù)不但可以用于解決諸如
共享資源競爭等沖突,還可以用于進(jìn)程間同步,使它們可以協(xié)
調(diào)合作［１１］ ,例如著名生產(chǎn)者/消費者問題:一個進(jìn)程向緩沖中
寫入/添加數(shù)據(jù),另外一個或若干個進(jìn)程從緩沖中讀取數(shù)據(jù)。
3．2　安全性分析
假設(shè)一個系統(tǒng)Ｔ 中有兩個進(jìn)程α和β,以及一個資源γ,進(jìn)
行如下約定:
ａ)變量x＝0 表示進(jìn)程α沒有占據(jù)資源γ;
b)變量x＝１ 表示進(jìn)程α占有了資源γ;
c)變量y＝0 表示進(jìn)程β 沒有占據(jù)資源γ;
ｄ)變量y＝１ 表示進(jìn)程β 占有了資源γ;
ｅ)行為x: ＝0 將變量x 賦值為0,表示進(jìn)程α釋放資源γ;
ｆ)行為x: ＝１ 將變量x 賦值為１,表示進(jìn)程α占據(jù)資源γ;
g)行為y: ＝0 將變量y 賦值為0,表示進(jìn)程β 釋放資源γ;
ｈ)行為y: ＝１ 將變量y 賦值為１,表示進(jìn)程β 占據(jù)資源γ。
則存在圖１ 所示的狀態(tài)轉(zhuǎn)移圖。
假如資源γ是一個臨界資源,那么就必須遵循互斥協(xié)議:
不允許被兩個或兩個以上的進(jìn)程同時占有資源γ。因此,就要
加入互斥性Ｍ:(x＝y(tǒng))(x＝0)。
互斥性Ｍ可以用下面的狀態(tài)轉(zhuǎn)移圖２ 來表示。
圖１　系統(tǒng)的Ｔ 狀態(tài)轉(zhuǎn)移圖圖２　互斥性Ｍ的狀態(tài)轉(zhuǎn)移圖
由于狀態(tài)ｑ２ 是系統(tǒng)中唯一不滿足互斥性的狀態(tài),所以可
以把互斥性Ｍ形式化地描述為
Ｍ＝｛$｜($(Tw
$)∧(ｉ≥0: sｉ≠ｑ２ )3
命題１　屬性Ｍ是安全性。
證明　$: $(Tw
$: $｜≠Ｐ (ｉ≥0: sｉ ＝ｑ２ ),取ｊ≥ｉ,
則β: β((Ｓ, ) w
$: $［..ｊ］β｜≠Ｍ。
因此,根據(jù)安全性的定義,屬性Ｍ是安全性。
證畢。
命題２　屬性Ｍ不是活性。
證明　系統(tǒng)中存在圖3 所示的有限運轉(zhuǎn)α:
圖3　系統(tǒng)Ｔ 中的一條有限運轉(zhuǎn)α
由于sｉ(α: sｉ ＝ｑ２ ,所以β((Ｓ, ) w
$,αβ｜≠Ｐ。
因此,屬性Ｐ 不是活性。
證畢。
由命題１ 和２ 可知,互斥協(xié)議屬于安全性而不是活性。它
只能保證系統(tǒng)不發(fā)生兩個進(jìn)程同時使用同一個臨界資源的情
況,但不能保證某個進(jìn)程一定能夠獲得一個臨界資源。
4　結(jié)束語
安全性和活性是兩類最基本的屬性,它們所確保的系統(tǒng)性
質(zhì)是完全不同的。由于對于安全性和活性的驗證使用的是不
同的技術(shù),所以區(qū)分一個屬性是安全性還是活性是十分必要
的。研究屬性的分類、定義和分析技術(shù),對于系統(tǒng)的形式化分
析具有重要的意義。后續(xù)的研究可以在本文工作的基礎(chǔ)上,對
于一些典型的系統(tǒng)屬性進(jìn)行分析,同時也可以探索安全性和活
性在實際系統(tǒng)驗證中的應(yīng)用新途徑。
參考文獻(xiàn)：
［１］ CＨＥＮ Ｒｕｉ, ＬOＮG Sｈｉ-goｎg．Spｅcｉｆｙｉｎg coｎcｕｒｒｅｎｔ pｒogｒａｍ bａｓｅｄ oｎ
ＴＬＡ［C］//Ｐｒoc oｆ ｔｈｅ ２ｎｄ Ｉｎｔｅｒｎａｔｉoｎａｌ Coｎｆｅｒｅｎcｅ oｎ Ｍｅcｈａｎｉcａｌ
Ｄｅｓｉgｎ ａｎｄ Ｐoｗｅｒ Ｅｎgｉｎｅｅｒｉｎg．Ｚｕｒｉcｈ： Ｔｒａｎｓ Ｔｅcｈ Ｐｕbｌｉcａｔｉoｎｓ,
２0１４： ７9８-８0２．
［２］ ＰＡＲＫ Sｕｎg-ｈooｎ, ＫＩＭＹ Ｍ．Ｍｕｔｕａｌ ｅｘcｌｕｓｉoｎ ａｌgoｒｉｔｈｍ ｉｎ ｍobｉｌｅ
cｅｌｌｕｌａｒ ｎｅｔｗoｒｋｓ［ C］//Ｌｅcｔｕｒｅ Ｎoｔｅｓ ｉｎ Ｅｌｅcｔｒｉcａｌ Ｅｎgｉｎｅｅｒｉｎg, ｖoｌ
２１5．２0１3： 695-７0２．
［3］ ＬＡＭＰOＲＴ Ｌ．Ｔｈｅ ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎ［Ｊ］．ＡCＭＴｒaｎｓ oｎ Ｐｒoｇｒaｍｍｉｎｇ
Ｌaｎｇｕaｇｅｓ aｎｄ Sｙｓｔｅｍｓ, １99４, １ 6(3)：８７２-9２3．
［４］ ＬＩ Ｊｕｎ-ｔａo, ＹＩＵ Ｚｉ-ｙｉ．Oｎ ａcｔｉoｎｓ oｆ ｔｅｍpoｒａｌ ｌogｉc oｆ ａcｔｉoｎｓ ［C］//
Ｐｒoc oｆ ｔｈｅ 3ｒｄ Ｉｎｔｅｒｎａｔｉoｎａｌ Coｎｆｅｒｅｎcｅ oｎ Ａｄｖａｎcｅｄ Coｍpｕｔｅｒ Ｔｈｅoｒｙ
ａｎｄ Ｅｎgｉｎｅｅｒｉｎg．Ｎｅｗ Ｙoｒｋ： ＩＥＥＥ Coｍpｕｔｅｒ Socｉｅｔｙ, ２0１0：
４４７４-４４７７．
［5］ CＨＡＵＤＨＵＲＩ Ｋ, ＤOＬＩGＥＺ Ｄ, ＬＡＭＰOＲＴ Ｌ, ｅｔ ａｌ．Ｖｅｒｉｆｙｉｎg ｓａｆｅｔｙ
pｒopｅｒｔｉｅｓ ｗｉｔｈ ｔｈｅ ＴＬＡ ＋pｒooｆ ｓｙｓｔｅｍ［C］//Ｌｅcｔｕｒｅ Ｎoｔｅｓ ｉｎ Coｍpｕｔｅｒ
Scｉｅｎcｅ, ｖoｌ 6１７3．Ｂｅｒｌｉｎ：Spｒｉｎgｅｒ,２0１0： １４２-１４８．
［6］ ＭＥＲＺ S．Ｐｒooｆｓ ａｎｄ pｒooｆ cｅｒｔｉｆｉcａｔｉoｎ ｉｎ ｔｈｅ ＴＬＡ ＋pｒooｆ ｓｙｓｔｅｍ
［C］//Ｐｒoc oｆ ｔｈｅ ２ｎｄ Ｉｎｔｅｒｎａｔｉoｎａｌ Ｗo(hù)ｒｋｓｈop oｎ Ｐｒooｆ Ｅｘcｈａｎgｅ ｆoｒ
Ｔｈｅoｒｅｍ Ｐｒoｖｉｎg．２0１２： １6-２0．
［７］ 唐鄭熠, 李均濤, 李祥．行為時序邏輯中公平性的研究與完善
［Ｊ］．計算機應(yīng)用研究, ２0１0, 27(5)： １７８８-１７9１．
［８］ COＵSＩＮＥＡＵ Ｄ, ＤOＬＩGＥＺ Ｄ, ＬＡＭＰOＲＴ Ｌ, ｅｔ ａｌ．ＴＬＡ ＋pｒooｆｓ
［C］//Ｌｅcｔｕｒｅ Ｎoｔｅｓ ｉｎ Coｍpｕｔｅｒ Scｉｅｎcｅ, ｖoｌ ７４36．Ｂｅｒｌｉｎ：Spｒｉｎgｅｒ,
２0１２： １４７-１5４．
［9］ ＢＡＩ Ｊｉｎ-ｓｈａｎ, ＴＡＮG Ｚｈｅｎg-ｙｉ, ＬＩ Ｊｕｎ-ｔａo, ｅｔ ａｌ．Ｌｉｎｅａｒ ｔｉｍｅ pｒopｅｒｔｉｅｓ
ｉｎ ＴＬＡ［ Ｊ］．ＪoｕｒｎaＩ oｆ Coｎｖｅｒｇｅｎcｅ Ｉｎｆoｒｍaｔｉoｎ Ｔｅcｈｎo-
Ｉoｇｙ, ２0１１, 6(１)： ２８４-２８８．
［１0］ ＷＡＮ Ｌｉａｎg, SＨＩ Ｗｅｎ-cｈａｎg．Spｅcｉｆｙｉｎg ａｎｄ cｈｅcｋｉｎg ｎｅｔｗoｒｋ pｒoｔocoｌ
bａｓｅｄ oｎ ＴＬＡ［C］//Ｐｒoc oｆ ｔｈｅ Ｉｎｔｅｒｎａｔｉoｎａｌ Coｎｆｅｒｅｎcｅ oｎ Ａｎｔｉ-
Coｕｎｔｅｒｆｅｉｔｉｎg, Sｅcｕｒｉｔｙ ａｎｄ Ｉｄｅｎｔｉｆｉcａｔｉoｎ．Ｗａｓｈｉｎgｔoｎ ＤC： ＩＥＥＥ
Coｍpｕｔｅｒ Socｉｅｔｙ, ２0１２： １８７-１95．
［１１］ ＺＨＡＮG Ｊｕｎ-ｍｉｎg, ＷＡＮG Ｋoｕ-ｗｕ．Ｔｈｅ ｓａｆｅｔｙ ａｎｄ ｌｉｖｅｎｅｓｓ pｒopｅｒｔｉｅｓ
oｆ ｔｈｅ ｎｅｔｗoｒｋ pｒoｔocoｌ bａｓｅｄ oｎ ＴＬＡ ［C］//Ｐｒoc oｆ ｔｈｅ Ｉｎｔｅｒｎａｔｉoｎａｌ
Coｎｆｅｒｅｎcｅ oｎ Ｉｎｆoｒｍａｔｉoｎ ａｎｄ Coｍｍｕｎｉcａｔｉoｎｓ Ｔｅcｈｎoｌogｉｅｓ．
Sｔｅｖｅｎａgｅ： Ｉｎｓｔｉｔｕｔｉoｎ oｆ Ｅｎgｉｎｅｅｒｉｎg ａｎｄ Ｔｅcｈｎoｌogｙ, ２0１3： ２１８-
２２２．
·１４８８· 計 算 機 應(yīng) 用 研 究 　 第3２ 卷

網(wǎng)友評論 more

綜合安全論文最新內(nèi)容

02-06