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

摘要：

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

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

所属期刊栏目：43

分类号：TP311.5(计算技术、计算机技术)

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

在线出版日期：2016-05-24（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：211-217