野王,日本xxxx片免费观看,丁香五月婷婷亚洲,六月丁香婷婷大团结

會員中心
加入VIP
微信

客服微信網站公眾號

　煤礦　化工　建筑
　機械　電力　冶金
　消防　交通　特種

　論壇　活動　視頻
　問答　投稿　 MSDS
　簽到　超市　招聘

導航：安全管理網>> 安全論文>> 綜合安全論文>>正文

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

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

內容預覽 [文件共3頁]

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

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

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

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

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

文本預覽

僅提取頁面文字內容，供快速閱讀使用。

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

網友評論 more

綜合安全論文最新內容

05-04

服務器虛擬化安全措施…

04-23

風險社會與風險治理

04-23

風險投資的風險防范及…

03-25

試論危巖穩(wěn)定性評價與…

03-23

安全文化助力核電企業(yè)…

03-20

云計算安全防護技術探…

03-20

云計算安全性探討

03-20

云計算下網絡安全技術…

綜合安全論文熱點內容

265831

淺談如何做好安全生…

139935

淺析安全生產管理措…

93803

淺析安全生產管理的…

65119

淺談安全生產監(jiān)督管理

64535

淺析安全生產事故頻…

55213

網絡安全存在的問題…

49209

淺析安全生產監(jiān)管工…

35551

淺談安全生產風險管…

相關內容

沒有相關信息!

創(chuàng)想安科網站簡介會員服務廣告服務業(yè)務合作提交需求會員中心在線投稿版權聲明友情鏈接聯(lián)系我們