基于时间扩展的ASEHA建模与验证

• 作者: 余兴超 王雪红 董荣胜
• 来源期刊: 桂林电子科技大学学报
• 学科: 工学
• 关键词: 实时系统 ASEHA 时钟约束 模型检测 UPPAAL
• 年，卷（期）: 2011,（2）
• 页码范围: 125-129
• 分类号: TP301.1
• 字数: 4665字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-808X.2011.02.009

摘要

为了有效地分析实时系统,在原计算模型的基础上,引入了时钟变量,在迁移上增加了时钟约束,扩展了异步扩展层次自动机的语义.运用基于时间扩展的ASEHA,分析了ATM系统,建立了用户和ATM的模型,并使用模型检测工具UPPAAL对模型进行验证,从无死锁、活性及可达性性质出发,验证了ATM系统的安全性.实验表明,提出的基于时间扩展的ASEHA能够降低系统分析的复杂性,有助于实时系统的建模与验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	董荣胜	桂林电子科技大学计算机科学与工程学院	115	1521	13.0	37.0
2	余兴超	桂林电子科技大学计算机科学与工程学院	6	8	2.0	2.0
3	王雪红	桂林电子科技大学计算机科学与工程学院	1	0	0.0	0.0