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

摘要

In the early development of real time system,a time consistency of system structure is analyzed due to the specialty of time series and security for real time system with critical tasks,which can discover the potential issue related time series in system design as soon as possible.Therefore,the validation method of AADL behavior model based on time restraint is proposed.In view of correctness verification problems of the AADL behavior model with time restriction,a kind of model decomposition rule based on node switching rule is presented to transform the AADL behavior model into execution trace set.Also a transformation algorithm from the trace set to Prolog language is designed,transforming the implicit and explicit time constraint into Prolog rules,supporting the validation of the real-time system with two time constraints.Finally,a special example of shipborne combat system with time restriction is verified by means of the time consistency validation approach of AADL behavior model.The approach verifies the implicit and explicit time constraint and provides a new effective way for the real time system of time series analysis.%任务关键的实时系统对时序及安全要求的特殊性,在实时系统开发的早期阶段进行体系结构的时间一致性分析,能够尽早发现系统设计时出现的有关时序的潜在问题,为此提出了基于时间约束的AADL行为模型的验证方法.针对带有时间约束的AADL行为模型时序验证问题,提出了一种基于节点转换规则的AADL行为模型分解规则,将实时系统的行为模型转换成运行时的路径集合;设计了路径集合到Prolog事实的转换算法;将实时系统的隐式时间约束和显式时间约束转换成Prolog规则,支持实时系统对两种时间约束进行验证.最后应用AADL行为模型时间一致性验证方法对船舶指控系统进行实例验证,验证了实时系统的隐式时间约束和显式时间约束,为实时系统的时序分析提供了一种新的有效途径.