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

摘要：

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

关键词：AADL行为模型、实时系统、时间一致性、Prolog

所属期刊栏目：27

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

资助基金："十三五"重点基础科研项目JCKY2016206B001

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

页数：共5页

页码：1-5