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

• 作者: 庄毅 李静 沈宁敏 白海洋
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: AADL 时间自动机模型 数据流时延 Uppaal 软件验证
• 年，卷（期）: 2016,（1）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 211-217
• 页数: 7页
• 分类号: TP311.5
• 字数: 7179字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2016.1.047

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	庄毅	南京航空航天大学计算机科学与技术学院	126	790	14.0	23.0
2	李静	南京航空航天大学计算机科学与技术学院	38	133	7.0	9.0
3	沈宁敏	南京航空航天大学计算机科学与技术学院	4	20	3.0	4.0
4	白海洋	南京航空航天大学计算机科学与技术学院	4	6	1.0	2.0