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

作     者：沈宁敏 李静 白海洋 庄毅 SHEN Ning-min;LI Jing;BAI Hai-yang;ZHUANG Yi

作者机构：南京航空航天大学计算机科学与技术学院南京210016 

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

出 版 物：《计算机科学》 (Computer Science)

年 卷 期：2016年第43卷第1期

页      码：211-217页

摘      要：体系结构分析设计语言AADL是一种可支持软硬件一体化建模及同一模型多元分析的形式化与图形化建模语言。采用时间自动机形式化模型检验方法对AADL模型中的数据流进行转换和验证。考虑到单一数据流与混合数据流的差异性,分别设计了数据流到时间自动机模型的转换规则,并通过时间自动机网络实现数据流的综合分析。设计开发了自动化模型转换的插件AADLToUppaal Plug-in,将其嵌入到OSTATE工具中,使用时间自动机建模与验证工具Uppaal对转换得到的时间自动机进行模拟和验证,等价地验证所设计的AADL模型数据流时延是否满足系统实时性要求。仿真实验结果表明,所设计的数据流模型转换方法能有效地将AADL模型转换到时间自动机模型,并能在Uppaal中正确地分析原模型的数据流时延特性。

主 题 词：AADL 时间自动机模型 数据流时延 Uppaal 软件验证 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.11896/j.issn.1002-137X.2016.1.047

馆 藏 号：203566982...