基于Prolog的AADL行为模型时间一致性验证方法

摘要

本发明公开了基于Prolog的AADL行为模型时间一致性验证方法，属于软件工程的技术领域。本发明在AADL行为附件的基础上进行扩展以建立带有时间约束的AADL行为模型，AADL行为模型描述了节点状态信息、时间约束信息，节点状态信息能够定性描述实时系统的属性，时间约束能够定量描述实时系统的时间区间，为完整验证实时系统时间一致性奠定了基础，将AADL行为模型分解得到的执行路径转换为Prolog事实，将形式化描述的隐式时间约束以及显式时间约束转换为Prolog规则，利用Prolog规则刻画实时系统的一致性，即可实现实时系统时间一致性的完整验证。

主权项

基于Prolog的AADL行为模型时间一致性验证方法，其特征在于，包括如下步骤：A、建立包含隐式时间约束和显式时间约束的AADL行为模型，形式化描述AADL行为模型的隐式时间约束和显式时间约束；B、将步骤A建立的AADL行为模型分解为仅包含活动节点的执行路径集合；C、将步骤B中所述执行路径中活动节点及时间约束转换为Prolog事实；D、借助步骤C所述Prolog事实将步骤A中形式化描述后的隐式时间约束和显式时间约束转换为Prolog规则；E、结合步骤C所述Prolog事实及步骤D所述Prolog规则对实时系统的时间一致性进行验证。