实时并发系统的PTSL模型检测

PTSL model checking of timed concurrent system

随着实时并发系统的软件规模越来越大、复杂性日趋增加,如何保证并发实时系统正确性和可靠性成为日益紧迫的问题。模型检测技术采用自动化的验证算法判断系统是否具有某一性质,它不仅包括对系统模型的遍历以及基于图形的分析方法,而且还需要大量的数值计算。本文把实时并发模型看成对并发博弈模型(CGS)的扩展,在此基础上添加了概率与时间性质,提出了概率时间并发博弈结构(PTCGS)。同时本文还提出了新的逻辑语言-概率时间策略逻辑(PTSL),它显式地把策略作为一阶逻辑中的对象,从而使我们能够以简单而自然的方式指定PTCGS系统中的非零和属性。PTSL模型检测方法能够让设计者准确知道模型是否满足用户的需求,从而提高系统的可靠性。最后,本文以ZeroConf协议为例来说明PTSL模型检测方法的正确性。

With the increased scale and complexity of real-time concurrent software systems, ensuringtheir correctness and reliability has become a matter of urgency. Current model-checking technology uses an automated demonstration algorithm to judgesystem properties,which must include the traversal in the system model and graphbased analysis techniques as well asextensive numerical computations. In this paper,we consider the timed concurrency model as an extension of the concurrent game model（ CGS） and addprobability and time properties to propose a new probabilistic timed concurrent game structure（ PTCGS）. We also propose a new logic language called probabilistic timed strategy logic（ PTSL）,which uses strategy as the object in the first-order logic to specify the nonzero-sum attributes in a simple and natural way. Lastly,we give an example usingthe ZeroConf protocol to demonstrate the correctness of the PTSL model checking method.