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

J4 ›› 2013, Vol. 35 ›› Issue (3): 121-127.

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

白海洋，李静，赵娜

（南京航空航天大学计算机科学与技术学院,江苏南京 210016）

收稿日期:2012-08-01 修回日期:2012-11-21 出版日期:2013-03-25 发布日期:2013-03-25
基金资助:
基本科研业务业务费专项科研项目可信嵌入式软件的建模与验证方法（NS2012136）；横向课题嵌入式软件可信性验证方法研究（KFA1151901）

Schedulability validation of embedded
software model based on time automaton

BAI Haiyang,LI Jing,ZHAO Na

（College of Computer Science and Technology,Nanjing University of Aeronautics & Astronautics,Nanjing 210016,China）

Received:2012-08-01 Revised:2012-11-21 Online:2013-03-25 Published:2013-03-25

摘要/Abstract

摘要：

结构分析与设计语言AADL在工业控制、汽车、航空航天等任务关键和实时领域的嵌入式系统开发中得到了广泛的应用。为在开发早期验证模型的可调度性，提出了AADL模型到时间自动机模型的转换方法，将AADL模型中的调度策略映射到时间自动机模型中的调度模板中，并给出了执行模型和附件模型的具体转换规则。转换后的模型可在UPPAAL工具中进行模拟和验证，分析原模型的可调度性。最后给出了AADL建模、模型转换和模型验证的全过程，证实了方法的有效性。

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

Abstract:

The Architecture Analysis and Design Language (AADL) is a popular language for embedded 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 propose 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 specific 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.

Key words: architecture analysis and design language;time automata model;model transformation;UPPAAL;schedulability verification

白海洋，李静，赵娜. 基于时间自动机的嵌入式软件模型可调度性验证[J]. J4, 2013, 35(3): 121-127.

BAI Haiyang,LI Jing,ZHAO Na. Schedulability validation of embedded
software model based on time automaton [J]. J4, 2013, 35(3): 121-127.

[1]	白先平, 姚袭欣, 陈香兰, 刘翀, 李曦. 基于时间自动机的AADL端到端流规约验证方法[J]. 计算机工程与科学, 2023, 45(05): 810-819.
[2]	马燕燕1，杨志斌1,2，江国华1. 一种SysML模型到AADL模型的自动转换方法[J]. 计算机工程与科学, 2020, 42(03): 456-466.
[3]	胡军,张维珺,李宛倩. 面向需求的安全关键系统形式化建模与验证方法研究[J]. 计算机工程与科学, 2019, 41(08): 1426-1433.
[4]	吴格格，庄雷，张坤丽，王国卿. 移动支付协议PCMS的形式化分析和验证[J]. 计算机工程与科学, 2017, 39(01): 67-73.
[5]	程亦涵，黄志球，阚双龙. 一种结合AADL和IMC的系统可靠性建模方法[J]. J4, 2015, 37(08): 1517-1524.
[6]	张君华1,黄志球2,肖芳雄3. 基于抽取-精化的概率系统假设-保证验证[J]. J4, 2013, 35(3): 128-133.
[7]	朱梅霞. MARTE顺序图到CCSL模型的转换[J]. J4, 2013, 35(10): 172-180.
[8]	曾一，王健，洪媛，周欣，蔡森虎. 一种支持MDA的UML类图到RDB模型的转换方法[J]. J4, 2010, 32(4): 67-70.
[9]	刘哲,吴健. 基于本体规则的模型转换的研究[J]. J4, 2010, 32(4): 75-78.
[10]	曾一, 王艳丽, 洪媛, 王健, 刘引. 一种B语言描述的需求模型到PIM的转换方法[J]. J4, 2010, 32(3): 85-88.
[11]	刘传会[1] 戎玫[2] 张广泉[1]. UML2．0顺序图的一种有穷自动机模型[J]. J4, 2008, 30(12): 118-121.
[12]	赵旭辉庄雷. 一种基于优先级扩展的时间自动机模型中DBM减法算法的改进[J]. J4, 2008, 30(11): 56-59.
[13]	张松年庄雷杜娟. 时间自动机可达性分析算法的改进[J]. J4, 2007, 29(10): 44-46.
[14]	马怀磊[1] 郭华[2] 庄雷[1]. 基于模型检测的不可靠环境下电子商务协议分析[J]. J4, 2007, 29(10): 82-84.
[15]	陈冰周祖德陈幼平谢经明艾武. 基于时间自动机的CAN网络可调度性分析[J]. J4, 2006, 28(9): 25-27.