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

摘要：

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

关键词：结构分析与设计语言、时间自动机模型、可调度性、仿真验证

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

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

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

页数：共6页

页码：1032-1037