从活性顺序图到时态逻辑的转化方法

摘要：

为了将活性顺序图用于模型检测,方便描述系统的场景需求,提出了一种将活性顺序图转换成时态逻辑的转化方法.分析活性顺序图语言并且定义一种基于路径的语义,用活性顺序图表述系统的场景需求.根据提出的语义,给出了一个将场景需求显式转化为时态逻辑的一般方法,针对并发消息较多的系统扩展和优化此方法,以得到更简短的时态逻辑公式.通过实例说明活性顺序图到线性时态逻辑的转化过程.

关键词：活性顺序图、时态逻辑、路径语义、场景需求、模型检测

所属期刊栏目：33

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

资助基金：国家863高技术研究发展计划基金项目2007AA010408

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

页数：共5页

页码：3437-3441