基于Uppaal的实时系统AADL数据流模型的转换与验证  

Transformation and Verification Method of AADL Data Flows for Real-time System Using Uppaal

作　　者：沈宁敏 李静[1] 白海洋[1] 庄毅[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016

出　　处：《计算机科学》2016年第1期211-217,共7页Computer Science

基　　金：中央高校基本科研业务费专项资金(NS2015092)资助

摘　　要：体系结构分析设计语言AADL是一种可支持软硬件一体化建模及同一模型多元分析的形式化与图形化建模语言。采用时间自动机形式化模型检验方法对AADL模型中的数据流进行转换和验证。考虑到单一数据流与混合数据流的差异性,分别设计了数据流到时间自动机模型的转换规则,并通过时间自动机网络实现数据流的综合分析。设计开发了自动化模型转换的插件AADLToUppaal Plug-in,将其嵌入到OSTATE工具中,使用时间自动机建模与验证工具Uppaal对转换得到的时间自动机进行模拟和验证,等价地验证所设计的AADL模型数据流时延是否满足系统实时性要求。仿真实验结果表明,所设计的数据流模型转换方法能有效地将AADL模型转换到时间自动机模型,并能在Uppaal中正确地分析原模型的数据流时延特性。Architecture analysis and design language（AADL）is a modeling language for formalization and graphics,which can support integrated modeling and multi-analysis.We used timed automata formal checking method to transform and verify data flow in AADL models.Considering the difference between single data flow and mixed data flows,we designed corresponding transformation rules from AADL models to timed automata,and analyzed and verified the data flow comprehensively by establishing timed automata network.An automated model conversion Eclipse plug-in was designed and integrated into the AADL modeling tool OSATE.Finally,timed automata modeling and Uppaal were used to simulate and verify the transformed timed automata while verifying whether the AADL model equivalently satisfies the real-time requirement of system.Experimental results show that the model transformation method is valid and flow latency qualities can be verified effectively with Uppaal.

关 键 词：AADL 时间自动机模型 数据流时延 UPPAAL 软件验证 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]