属性序列图:形式语法和语义

摘要：

在基于场景的软件工程中,时态逻辑被广泛地用来推理并发系统的正确性.模型检验技术允许自动检验系统模型和给定的属性之间的一致性,这些属性常用线性时态逻辑公式来表示.不幸的是,由于这些公式具有复杂的结构使得模型检验技术很难应用在工业实践中.属性序列图可以用来解决这种问题,它是一种基于场景的可视化的语言,容易理解并且具有较强的表达能力,能够克服当前工业中常用的符号中存在的诸多表达缺陷.为了能够完全清晰地描述和理解属性序列图,使其能够广泛地应用,给出其形式语法和基于B(u)chi自动机的形式语义,并进行了实例研究,讨论了其应用前景.

关键词：时态逻辑、场景、属性序列图、B(u)chi自动机、模型检验

所属期刊栏目：45

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

资助基金：国家自然科学基金60473065;60773105;江苏省自然科学基金BK2007513;国家八六三高技术研究发展计划基金2007AA01Z141;国家自然科学基金60425206

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

页数：共11页

页码：318-328