基于时间自动机的嵌入式软件模型可调度性验证  

Schedulability validation of embedded software model based on time automaton

作　　者：白海洋[1] 李静[1] 赵娜[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京210016

出　　处：《计算机工程与科学》2013年第3期121-127,共7页Computer Engineering & Science

基　　金：基本科研业务业务费专项科研项目可信嵌入式软件的建模与验证方法(NS2012136);横向课题嵌入式软件可信性验证方法研究(KFA1151901)

摘　　要：结构分析与设计语言AADL在工业控制、汽车、航空航天等任务关键和实时领域的嵌入式系统开发中得到了广泛的应用。为在开发早期验证模型的可调度性,提出了AADL模型到时间自动机模型的转换方法,将AADL模型中的调度策略映射到时间自动机模型中的调度模板中,并给出了执行模型和附件模型的具体转换规则。转换后的模型可在UPPAAL工具中进行模拟和验证,分析原模型的可调度性。最后给出了AADL建模、模型转换和模型验证的全过程,证实了方法的有效性。The Architecture Analysis and Design Language （AADL） is a popular language for em- bedded system development in industrial control, automotive, aerospace and other mission critical and real-time fields. In order to validate the schedulability of the established model at early stage, we pro- pose a new method which can translate the AADL model into time automaton model. The scheduling strategy of the AADL model is mapped to the template of time automaton model, and we define the spe- cific rules of translating the AADL execution model and behavior model. The generated model can be simulated and checked through the tool UPPAAL, to analyze the schedulability of the original model. Finally, the project describes the whole process of AADL modeling, model transformation and model verification, and proves the validation of the method.

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

分 类 号：TP311.53[自动化与计算机技术—计算机软件与理论]