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

• 作者: 周宇 张鹏程 徐宝文 李必信
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 时态逻辑 场景 属性序列图 B(u)chi自动机 模型检验
• 年，卷（期）: 2008,（2）
• 所属期刊栏目: 数据库技术与软件工程
• 页码范围: 318-328
• 页数: 11页
• 分类号: TP311
• 字数: 6174字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐宝文	东南大学计算机科学与工程学院	118	3034	31.0	51.0
2	李必信	东南大学计算机科学与工程学院	39	305	9.0	15.0
3	周宇	东南大学计算机科学与工程学院	12	128	7.0	11.0
4	张鹏程	东南大学计算机科学与工程学院	12	61	5.0	7.0