基于Token追踪的分布式互斥算法

本文首先提出一切合实际的互斥信件量度量方法,该方法不仅考虑请求结点所发的信息数,同时还考虑信件的存储转发次数,然后针对任一拓扑结构,在充分利用局部信息与已知信息的基础上,给出了互斥信件量为0～2(n—1)(n为结点数)的有效互斥算法,该算法不仅在互斥信件量上是目前最优的,而且充分体现了分布式算法设计的一个重要原则,充分利用一切已知信息作为未来决策的依据。     

一种广域网中的分布式互斥算法

广域网可简单地看作由多个局域网通过远程通信线路互连组成。为了适应广域网环境的特点,文章提出了一种两层结构的分布式互斥算法模型,把广域网系统组织成由局部进程组成的局部网络的由每个局部网络中的协调进程组成的全局两层。为了互斥地访问共享资源,局部进程必须首先获得局部令牌,然后再向本地协调进程申请全局令牌,只有获得了局部和全避令牌的局部进程才能进入临界区。还讨论了对该算法可能的扩展。     

改进的分布式互斥请求集生成算法

在分布式系统中,各节点必须互斥地访问临界区.节点的请求集的长度决定了系统的效率、性能.虽然最优请求集的节点数最少(大约n),但已有的解决方案该类问题算法类似于穷举法,随着节点的增加,该方法变得不可计算.提出了一种快速的请求集生成算法,该算法以循环差集请求集生成算法的理论和贪心算法的基本思想为基础,在每次迭代的过程中,选出一个当前条件下最优的节点加入请求集.与其他的方法相比较,该方法能对任意给定的整数快速、有效地生成对称的请求集.本算法时间复杂度为O(n2),生成的请求集长度为n～2n.     

分布式互斥算法的研究与改进

在几种基于令牌算法的基础上,提出了一个对网络逻辑结构无要求的分布式互斥算法。算法不但能够在逻辑结构无要求的计算机网络中通过发送消息和传递令牌来同步对临界资源的访问,而且可以很好地解决请求丢失、令牌丢失等问题。通过对算法的性能进行分析验证了该算法是高效的,并给出了正确性证明。     

自适应Ad hoc分布式互斥算法

Ad hoc网络的动态拓扑结构和节点自组织给分布式算法的实现带来了诸多困难.针对Ad hoc分布式互斥算法研究滞后的现状,提出了一种自适应的Ad hoc分布式算法ADMUTEX. ADMUTEX算法基于令牌查询方法,它采用Lamport逻辑时戳保证消息的时序性,避免了节点饿死.同时,它在消息复杂度与同步延迟之间作了折衷,而且它不需要节点了解系统的全局信息,能够适应Ad hoc网络的动态拓扑结构和节点频繁出入的情况.分析与仿真结果表明该算法具有较低的消息复杂度、小响应延迟和公平性.     

基于优先级组的分布式互斥算法的改进

主要介绍了一种分布式互斥算法的改进方案，首先简要介绍了基于权标的常规算法，然后提出了优先级组算法的另一种方案，并详细阐述算法的设计思想及其数据结构，本算法最主要的特点是在分布式互斥中引入了优先级和树的概念，从而将Raymond和Ricart_Agrawala互斥算法较好地结合了起来。     

多副本访问控制的分层结构分布式互斥算法

提出了一种用于分布式系统中多副本对象访问控制的分层结构分布式互斥实现方法,可以显著降低分布式系统中互斥访问算法的消息复杂度,并提高了系统和算法的容错能力和稳定性,为构建超大规模分布式系统,保证分布式系统中的多副本对象的互斥和一致访问提供了实现手段。     

分布式系统进程互斥算法的研究与改进

本文分析比较了传统互斥算法，提出了一种新的基于令牌的算法，并详细阐述算法的设计思想及其数据结构。本算法最主要的特点是在分布式互斥中引入了优先级和树的概念，能有效的降低进程问的通信量，以及保证互斥和预防死锁。     

基于半环仲裁集的环网分布式互斥算法

分布式互斥是环网分布式系统的重要问题.根据此类系统的特点,提出了新型的分布式互斥算法.该算法以请求者自身为中心,基于半环生成分布式互斥仲裁集;采用Lamport逻辑时戳保证消息的时序性;算法采用"探测"消息进行系统的容错处理.分析与仿真证明,该算法具有较低的消息复杂度、较短的响应延迟以及较好的容错性能.     

基于概率模型检测的软件缺陷定位方法

软件缺陷的存在导致软件无法满足用户的需求,如何高效高质量地定位缺陷是消除软件缺陷的关键.基于模型的缺陷定位技术是当前的研究热点,可以用于检测软件系统故障找到软件失效的原因.现有基于模型的缺陷定位技术中,未考虑非相邻节点间传递依赖和测试用例对可疑度的影响,导致缺陷定位精度和效率低.提出了基于概率模型检测的软件缺陷定位方法(probabilistic model checking method for software fault location,PMC-SFL),首先提出一种程序概率模型用于提高模型的推理能力;然后设计了基于执行路径构建程序概率模型的学习算法;最后设计了基于概率模型检测的软件缺陷定位算法,用于缺陷定位分析.通过在公共数据集Siemens上进行实验和分析,表明了PMC-SFL方法与五种现有的缺陷定位方法RankCP、BNPDG、Tarantula、SOBER和CT相比,具有更高的软件缺陷定位精度和效率.     

动态环境下基于概率模型检测的路径规划方法

提出了一种动态复杂环境下采用概率模型检测技术进行路径规划的新方法。考虑到实际应用中机器人其移动行为总是受到外界因素的影响,将机器人移动行为看作一个不确定事件,提取环境中的影响因素,构建马尔可夫决策过程模型。采用时态逻辑语言描述机器人目标任务,表达复杂多样的需求行为。运用工具PRISM验证属性,得到满足任务需求的全局优化路径。另外,在全局路径的基础上提出了一种动态避障策略,实现避障局部规划的同时尽量保证机器人最大概率完成任务。通过理论和仿真实验结果证明该方法的正确性和有效性。     

Performance Evaluation of a Real-time Simulation Architecture using Probabilistic Model Checking

The goal of this paper is to show how to use probabilistic model checking techniques in order to achieve quantitative performance evaluation of a real-time distributed simulation. A simulation based on the High Level Architecture (HLA) is modelled as a stochastic process, a Continuous Time Markov Chain (CTMC), using the stochastic algebra PEPA. Next a property representing a performance constraint is evaluated applying Continuous Stochastic Logic CSL formula on the CTMC model using the probabilistic model checker PRISM. Finally a first experiment is made to compare the model with a real case.     

一种高效的动态概率广播算法及其概率模型检测分析

在Ad Hoc网络中,广播有着相当广泛的应用,其算法的效率极大地影响着网络的性能.本文基于DP算法提出了BN-DP算法,考虑了节点分布、计数器值以及收发节点间距离对广播算法的影响,赋予处于接收边缘的节点更高的转发概率.然后使用概率模型检测工具PRISM,分析了计数器值和节点分布对BN-DP算法性能的影响.结果表明:在相同可达率的情况下,所提出的BN-DP算法与FP、DP算法相比,减少了转发分组的数量,提高了广播效率.     

匿名通信协议MACP概率模型检验

匿名通信技术是保护互联网用户隐私的最有力手段之一,但匿名通信协议的形式化验证仍是亟待解决的难题。对P2P匿名通信协议MACP进行了形式化验证与分析,将MACP协议的匿名路径建立过程模型化为一个离散时间马尔可夫链;然后利用概率计算树逻辑PCTL描述MACP协议的匿名性质,并采用概率模型检验器对MACP协议的匿名性进行检验。检验结果表明,通过增加匿名通道数,提高了MACP协议的匿名等级和抗攻击能力;MACP协议的匿名性随着规模的增大而增强,并没有因控制匿名路径的长度而降低。     

SpaceWire协议的形式化建模与概率分析

SpaceWire是应用于航空航天领域的高速通信总线标准,保证其设计的可靠性和正确性至关重要.本文通过概率模型检测的方法对SpaceWire的交换层设计进行形式化建模与量化分析.基于马尔科夫决策过程(MDP)对交换层的链路初始化及正常运行过程建立形式化概率模型,模型包括发送方、接收方和信道,提取SpaceWire交换层的4个关键属性,用概率计算树逻辑(PCTL)进行描述,运用PRISM平台对SpaceWire交换层设计进行验证和分析;并获得信道丢包概率不同情况下,链路初始化成功以及正常运行时数据包正确传输的概率,这种定量形式化分析结果可为SpaceWire的设计和实现提供参考依据.     

Probabilistic symbolic model checking with PRISM: a hybrid approach

In this paper we present efficient symbolic techniques for probabilistic model checking. These have been implemented in PRISM, a tool for the analysis of probabilistic models such as discrete-time Markov chains, continuous-time Markov chains and Markov decision processes using specifications in the probabilistic temporal logics PCTL and CSL. Motivated by the success of model checkers such as SMV which use BDDs (binary decision diagrams), we have developed an implementation of PCTL and CSL model checking based on MTBDDs (multi-terminal BDDs) and BDDs. Existing work in this direction has been hindered by the generally poor performance of MTBDD-based numerical computation, which is often substantially slower than explicit methods using sparse matrices. The focus of this paper is a novel hybrid technique which combines aspects of symbolic and explicit approaches to overcome these performance problems. For typical examples, we achieve a dramatic improvement over the purely symbolic approach. In addition, thanks to the compact model representation using MTBDDs, we can verify systems an order of magnitude larger than with sparse matrices, while almost matching or even beating them for speed.     

Optimal algorithm for mutual exclusion in mesh-connected computer networks

A distributed algorithm is presented that realizes mutual exclusion among n nodes in a mesh-connected computer network. The nodes communicate by using messages only, and there is no global controller. The algorithm requires at most 3.5 √n messages per mutual exclusion invocation under light demand, and reduces to approximately four messages under heavy demand. The time required to achieve mutual exclusion is shown to be minimal under some general assumptions.     

Probabilistic model checking for the quantification of DoS security threats

Secure authentication features of communication and electronic commerce protocols involve computationally expensive and memory intensive cryptographic operations that have the potential to be turned into denial-of-service (DoS) exploits. Recent proposals attempt to improve DoS resistance by implementing a trade-off between the resources required for the potential victim(s) with the resources used by a prospective attacker. Such improvements have been proposed for the Internet Key Exchange (IKE), the Just Fast Keying (JFK) key agreement protocol and the Secure Sockets Layer (SSL/TLS) protocol. In present article, we introduce probabilistic model checking as an efficient tool-assisted approach for systematically quantifying DoS security threats. We model a security protocol with a fixed network topology using probabilistic specifications for the protocol participants. We attach into the protocol model, a probabilistic attacker model which performs DoS related actions with assigned cost values. The costs for the protocol participants and the attacker reflect the level of some resource expenditure (memory, processing capacity or communication bandwidth) for the associated actions. From the developed model we obtain a Discrete Time Markov Chain (DTMC) via property preserving discrete-time semantics. The DTMC model is verified using the PRISM model checker that produces probabilistic estimates for the analyzed DoS threat. In this way, it is possible to evaluate the level of resource expenditure for the attacker, beyond which the likelihood of widespread attack is reduced and subsequently to compare alternative design considerations for optimal resistance to the analyzed DoS threat. Our approach is validated through the analysis of the Host Identity Protocol (HIP). The HIP base-exchange is seen as a cryptographic key-exchange protocol with special features related to DoS protection. We analyze a serious DoS threat, for which we provide probabilistic estimates, as well as results for the associated attacker and participants' costs.