计算机光盘软件与应用
計算機光盤軟件與應用
계산궤광반연건여응용
COMPUTER CD SOFTWARE ADN APPLICATIONS
2013年
18期
74-75
,共2页
行为时序逻辑%PlusCal%ToolBox%DEKKER算法
行為時序邏輯%PlusCal%ToolBox%DEKKER算法
행위시서라집%PlusCal%ToolBox%DEKKER산법
行为时序逻辑TLA是由Leslie Lamport提出的新的逻辑，它结合了行为逻辑和时序逻辑的特点，增强了表达能力。Dekker互斥算法最早是由荷兰数学家Dekker提出的一种解决并发进程互斥与同步的软件实现方法。本文以PlusCal语言和TLA+预言描述了Dekker算法，并利用ToolBox模型检测工具对DEKKER并发算法进行了验证。证明该算法满足互斥属性和非饥饿属性。
行為時序邏輯TLA是由Leslie Lamport提齣的新的邏輯，它結閤瞭行為邏輯和時序邏輯的特點，增彊瞭錶達能力。Dekker互斥算法最早是由荷蘭數學傢Dekker提齣的一種解決併髮進程互斥與同步的軟件實現方法。本文以PlusCal語言和TLA+預言描述瞭Dekker算法，併利用ToolBox模型檢測工具對DEKKER併髮算法進行瞭驗證。證明該算法滿足互斥屬性和非饑餓屬性。
행위시서라집TLA시유Leslie Lamport제출적신적라집，타결합료행위라집화시서라집적특점，증강료표체능력。Dekker호척산법최조시유하란수학가Dekker제출적일충해결병발진정호척여동보적연건실현방법。본문이PlusCal어언화TLA+예언묘술료Dekker산법，병이용ToolBox모형검측공구대DEKKER병발산법진행료험증。증명해산법만족호척속성화비기아속성。
