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

摘要：

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

关键词：模型检测、概率时间并发博弈结构、概率时间策略逻辑、概率时间自动机、区域图、实时并发系统、博弈模型

所属期刊栏目：12

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金项目61502196

在线出版日期：2017-12-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：694-701