[1]孙健,徐敏. 基于AADL的嵌入式系统可调度性验证[J].计算机技术与发展,2016,26(03):23-26.
　SUN Jian,XU Min. Schedulability Verification of Embedded System Based on AADL[J].,2016,26(03):23-26.
点击复制

 基于AADL的嵌入式系统可调度性验证()
分享到：

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
26
期数:
2016年03期
页码:
23-26
栏目:
智能、算法、系统工程
出版日期:
2016-03-10

文章信息/Info

Title:
 Schedulability Verification of Embedded System Based on AADL
文章编号:
1673-629X（2016)03-0023-04
作者:
 孙健; 徐敏
 南京航空航天大学 计算机科学与技术学院
Author(s):
 SUN Jian; XU Min
关键词:
 ; 嵌入式系统; 体系结构分析设计语言; 时间自动机; 模型转换; UPPAAL; 实时性
Keywords:
 ; embedded system; AADL; timed automata; model transformation; UPPAAL; real-time
分类号:
TP302
文献标志码:
A
摘要:
 AADL近年来在嵌入式实时系统领域得到了广泛的应用，相对于其他语言能够更好地描述系统的非功能属性，同时支持系统软硬件建模，在基于模型驱动的开发方法下对系统进行建模和分析，用形式化的方法对系统的相关属性进行验证，从而可以在设计阶段发现错误，对保证系统的安全运行和开发效率的提高有着重要意义。对于验证AADL模型可调度性的问题，文中利用时间自动机理论，根据AADL调度模型和时间自动机模型的语义相似性，将AADL模型转换成时间自动机模型，并设计转换插件，通过Eclipse插件开发技术将其集成到AADL建模与分析工具OSATE中。最后在UP-PAAL工具中对转换后的时间自动机模型进行模拟和验证，利用相关性质验证语句等价地对原模型的可调度性进行验证。
Abstract:
 AADL has been widely used in embedded real-time system in recent years. Compared with other languages,it can better de-scribe the system non functional attributes,and also support the software and hardware modeling of the system. AADL can model and ana-lyze the system based on the model driven development method,and verify relevant properties using formal method. Error can be found in the design phase,and it has great significance to ensure the safe operation of the system and improve the efficiency of development. For verifying AADL model schedulability problem, according to the semantics similarity of AADL scheduling model and timed automata model,the theory of timed automata is used to convert AADL model to timed automata model,and integrate conversion plug-in into the AADL modeling and analysis tool OSATE through the development of Eclipse plug-in technology. Finally,the converted timed automa-ton model in the UPPAAL tool is simulated and verified,using the related verification statement to verify the schedulability of the original model.

相似文献/References:

[1]侯战胜 姚放吾.基于i.MX21的AdHoc网络终端的设计与实现[J].计算机技术与发展,2010,(01):4.
　HOU Zhan-sheng,YAO Fang-wu.Design and Realization of AdHoc Network Terminal Based on i.MX21[J].,2010,(03):4.
[2]宋亮 原亮 满梦华.军用嵌入式系统中PCB设计与测试规范研究[J].计算机技术与发展,2010,(01):232.
　SONG Liang,YUAN Liang,MAN Meng-hua.Study of PCB Design and Testing Standards in Embedded Systems for Military Usage[J].,2010,(03):232.
[3]张军 尚敏 卢宁 吴晓阳.嵌入式机电设备典型系统平台研究[J].计算机技术与发展,2010,(04):228.
　ZHANG Jun,SHANG Min,LU Ning,et al.Research of Electro- Mechanical Equipment Typical System Platform Based on Embedded Technology[J].,2010,(03):228.
[4]杨杰 刘锋 张义超 王天生.基于工程化流程的一种嵌入式系统开发方法[J].计算机技术与发展,2009,(12):105.
　YANG J ie,LIU Feng,ZHANG Yi-chao,et al.Embedded System Development Method Based on Engineering Conception[J].,2009,(03):105.
[5]何振兴 熊健民 刘幺和 宋庭新.基于WSN的实时监控系统的研究[J].计算机技术与发展,2009,(12):229.
　HE Zhen-xing,XIONG Jian-min,LIU Yao-he,et al.Research of Remote Real - Time Monitoring System Based on WSN[J].,2009,(03):229.
[6]刘军 马文丽 姚文娟 郑文岭.基于嵌入式Web服务器病人监护系统设计[J].计算机技术与发展,2009,(01):187.
　LIU Jun,MA Wen-li,YAO Wen-juan,et al.Design of Remote Care System Based on Embedded Web Server[J].,2009,(03):187.
[7]刘金祥 王京仁.μCLinux在实时监控系统中的应用研究[J].计算机技术与发展,2009,(03):220.
　LIU Jin-xiang,WANG Jing-ren.Research on μCLinux Applied in Real Time Monitoring System[J].,2009,(03):220.
[8]张炯 吕紫旭 刘栋 金惠华.实时操作系统ThreadX剖析[J].计算机技术与发展,2008,(01):22.
　ZHANG Jiong,LU Zi-xu,LIU Dong,et al.Analysis of Real Time Operating System： ThreadX[J].,2008,(03):22.
[9]鲁艳 马旭东 问治国 黄艳.基于Linux—MiniGUI嵌入式系统监控管理软件开发[J].计算机技术与发展,2008,(06):179.
　LU Yan,MA Xu-dong,WEN Zhi-guo,et al.Development of Embedded System Management Software Based on Linux- MiniGUI[J].,2008,(03):179.
[10]王恒 李勇 王泉 赵双.基于IEEE 802．11b和CDMA网的多路监控系统的设计与实现[J].计算机技术与发展,2008,(06):192.
　WANG Heng,LI Yong,WANG Quan,et al.Design and Implementation of a Multi- Channel Monitoring System Based on IEEE 802. 11b and CDMA Networks[J].,2008,(03):192.
[11]勇[],郭兵[],沈艳[],等. 烟叶定级系统的Zigbee通信的设计和实现[J].计算机技术与发展,2014,24(07):188.
　HUANG Yong[],GUO Bing[],SHEN Yan[],et al. Design and Implementation of Zigbee Communication in Tobacco Grading Embedded System[J].,2014,24(03):188.
[12]高翔,刘秀鹏,冯天天,等. 基于无线体域网的康复监测系统设计[J].计算机技术与发展,2014,24(09):234.
　GAO Xiang,LIU Xiu-peng,FENG Tian-tian,et al. Monitoring System Design for Rehabilitating Training Based on Wireless Body Area Network[J].,2014,24(03):234.
[13]王涛,吴蒙. 基于OMAP的视频监控系统关键技术研究[J].计算机技术与发展,2014,24(11):230.
　WANG Tao,WU Meng.Research on Key Techniques of Video Monitoring System Based on OMAP[J].,2014,24(03):230.
[14]张磊,王亚刚. 基于MiniGUI的嵌入式图形界面的研究与实现[J].计算机技术与发展,2015,25(02):194.
　ZHANG Lei,WANG Ya-gang. Research and Implementation of Embedded GUI Based on MiniGUI[J].,2015,25(03):194.
[15]杨莉[][],李楠[],席隆[]. 基于AADL的嵌入式系统可靠性建模方法的探讨[J].计算机技术与发展,2015,25(08):234.
　YANG Li[][],LI Nan[],XI Long[]. Discussion on Reliability Modeling for Embedded System Based on AADL[J].,2015,25(03):234.
[16]朱耀麟,刘慧琳. 基于Qt的电脑横机上位机系统[J].计算机技术与发展,2017,27(04):200.
　ZHU Yao-lin,LIU Hui-lin. Host System of Computer Flat Knitting Machine with Qt[J].,2017,27(03):200.
[17]王凯. 基于Qt/Embedded的嵌入式GUI显示架构实现[J].计算机技术与发展,2017,27(05):144.
　WANG Kai. Implementation of Embedded GUI Display Architecture Based on Qt/Embedded[J].,2017,27(03):144.
[18]马铮,黄连丽,陶冰冰,等. 一种结合AADL和TPN的系统能耗建模方法[J].计算机技术与发展,2017,27(06):151.
　MA Zheng,HUANG Lian-li,TAO Bing-bing,et al. An Embedded System Energy Consumption Modeling Method Using AADL and TPN[J].,2017,27(03):151.

更新日期/Last Update: 2016-05-24