基于时间自动机的嵌入式系统 AADL 模型可调度性验证

• 作者: 周培云 李静 沈宁敏 白海洋
• 来源期刊: 东南大学学报（自然科学版）
• 学科: 工学
• 关键词: 结构分析与设计语言 时间自动机模型 可调度性 仿真验证
• 年，卷（期）: 2015,（6）
• 页码范围: 1032-1037
• 页数: 6页
• 分类号: TP311.5
• 字数: 5260字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-0505.2015.06.002

摘要

采用时间自动机形式化模型检验方法建立了结构分析与设计语言（AADL）调度模型的自动机，实现了从 AADL 模型到时间自动机模型的自动转换与验证。首先，设计了周期、非周期的线程时间自动机模板及抢占、非可抢占的调度器时间自动机模板，建立了 AADL 调度模型到时间自动机模型的语义映射法则。然后，设计了自动化模型转换插件，并将其集成到 OSATE 建模工具中，实现了建模、转换、验证的集成开发环境。最后，利用 UPPAAL 工具对时间自动机模型进行模拟与验证。仿真实验结果表明，所建立的模型转换方法能够有效、实时地将 AADL 模型转换为时间自动机模型，并可在 UPPAAL 中分析原模型的可调度性。

作者信息

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