论文部分内容阅读
随着嵌入式实时系统的发展,系统的复杂度也越来越高,需要对系统进行抽象建模和验证。体系结构分析与设计语言(Architecture Analysis and Design Language,AADL)自2004年由美国汽车工程师协会(Society of Automotive Engineers,SAE)提出以来,广泛地应用于航空、航天、汽车电子及武器装备等关键信息领域。针对这些领域因系统规模大、布局复杂且多人协同建模导致的模型不一致问题进行了研究,具体的工作如下:首先,针对AADL模型静态结构和动态行为缺乏一致性验证的现状,对AADL模型的静态结构和动态行为进行了研究,并给出了静态结构一致性和动态行为一致性的定义。提出了AADL模型静态结构的相关组件到Prolog(Programming in Logic,Prolog)的转换规则和转换算法,考虑组件交互中的限制,基于Prolog对AADL模型的端口类型一致性、信息流方向一致性及数据类型一致性等静态结构一致性进行验证。通过分析模式转换的特征,建立了基于Prolog的系统初始状态、状态转移函数及触发事件的形式化描述,提出了模型动态行为相关组件到Prolog的转换规则及算法。最后以航空电子系统中模式控制面板案例进行模型静态结构和动态行为一致性的验证与修复。与相关工作对比表明本文方法可以全面地验证AADL模型一致性。其次,针对AADL模型中的时间约束研究欠缺的情况,给出了端到端数据流时间约束一致性验证框架并提出了基于Prolog的端到端数据流时间约束一致性验证方法。从任务处理时延的数据驱动、同步采样及异步采样三个角度给出基于Prolog的端到端数据流计算方法。并基于时间区间的相对时间划分给出了时间约束一致性和时间约束强一致性的定义,设计了基于Prolog的时间约束一致性验证规则。以模式控制面板中的端到端数据流为例进行模型一致性验证与修复。最后,时延分析功能的对比表明基于Prolog的端到端数据流时延分析方法较全面的分析了模型的时间约束。最后,以OSATE(open-source tool platform to support AADL,OSATE)建模平台为基础,设计了AADL模型验证插件,实现了AADL模型的静态结构一致性、动态行为一致性和时间约束一致性的验证功能。以航电系统为例进行建模验证,结果表明AADL模型验证插件能够满足AADL模型一致性验证的需求。