AADL行为模型时间一致性验证方法

• 作者: 刘骁 谢红梅
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: AADL行为模型 实时系统 时间一致性 Prolog
• 年，卷（期）: 2017,（7）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 1-5
• 页数: 5页
• 分类号: TP311
• 字数: 4669字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2017.07.001

摘要

任务关键的实时系统对时序及安全要求的特殊性,在实时系统开发的早期阶段进行体系结构的时间一致性分析,能够尽早发现系统设计时出现的有关时序的潜在问题,为此提出了基于时间约束的AADL行为模型的验证方法.针对带有时间约束的AADL行为模型时序验证问题,提出了一种基于节点转换规则的AADL行为模型分解规则,将实时系统的行为模型转换成运行时的路径集合;设计了路径集合到Prolog事实的转换算法;将实时系统的隐式时间约束和显式时间约束转换成Prolog规则,支持实时系统对两种时间约束进行验证.最后应用AADL行为模型时间一致性验证方法对船舶指控系统进行实例验证,验证了实时系统的隐式时间约束和显式时间约束,为实时系统的时序分析提供了一种新的有效途径.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	谢红梅	南京航空航天大学继续教育学院	6	2	1.0	1.0
2	刘骁	南京航空航天大学计算机科学与技术学院	1	0	0.0	0.0