基于行为时序逻辑TLA的算法分析与验证  

作　　者：赵梦龙[1] 

机构地区：[1]贵州广播电视大学,贵阳550004

出　　处：《计算机光盘软件与应用》2013年第18期74-75,共2页Computer CD Software and Application

摘　　要：行为时序逻辑TLA是由Leslie Lamport提出的新的逻辑,它结合了行为逻辑和时序逻辑的特点,增强了表达能力。Dekker互斥算法最早是由荷兰数学家Dekker提出的一种解决并发进程互斥与同步的软件实现方法。本文以PlusCal语言和TLA+预言描述了Dekker算法,并利用ToolBox模型检测工具对DEKKER并发算法进行了验证。证明该算法满足互斥属性和非饥饿属性。

关 键 词：行为时序逻辑 PlusCal TOOLBOX DEKKER算法 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]