[1]张辉 经小川 谢伟华 高金梁.基于Petri网的AADL模型正确性验证研究[J].计算机技术与发展,2012,(09):91-94.
　ZHANG Hui,JING Xiao-chuan,XIE Wei-hua,et al.Verification Research on Correctness of AADL Model Based on Petri Net[J].,2012,(09):91-94.
点击复制

基于Petri网的AADL模型正确性验证研究()
分享到：

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

卷:
期数:
2012年09期
页码:
91-94
栏目:
智能、算法、系统工程
出版日期:
1900-01-01

文章信息/Info

Title:
Verification Research on Correctness of AADL Model Based on Petri Net
文章编号:
1673-629X（2012）09-0091-04
作者:
张辉 经小川 谢伟华 高金梁
中国航天工程咨询中心
Author(s):
ZHANG Hui;  JING Xiao-chuan;  XIE Wei-hua;  GAO Jin-liang
China Aerospace Engineering Consultation Center
关键词:
体系结构分析和设计语言; Petri网; 运行状态; 映射; 关联矩阵
Keywords:
AADL ;  Petri net;  run state ;  mapping;  associate matrix
分类号:
TP311
文献标志码:
A
摘要:
体系结构分析和设计语言AADL能够在架构级对系统进行建模，并通过一系列验证尽早发现系统设计中的问题，在航空航天等嵌入式系统中具有广阔的应用前景。但是目前的验证集中在性能分析等方面，忽略了AADL模型本身的正确性验证。提出将AADL模型的模式和模式转换映射成Petri网模型，结合Petri网的理论对AADL模型正确性进行验证的方法，从而确保建模阶段模型的正确性，为后续各种验证分析奠定了基础，同时进一步降低了在系统实现后发现问题修改模型所带来的时间和成本。最后，通过具体实例验证了该方法的可实施性和有效性
Abstract:
Architecture analysis and design language （AADL） will be applied widely in the aviation and aerospace embedded systems, which can model the system on the architecture level and find problems in the design through a series of verification. But the focus of verification now is performance analysis, while ignoring the correctness of AADL model itself. An approach is proposed which maps modes and mode transitions of AADL model to Petfi net and verifies AADL model according to Petri net. The approach is a foundation for other verification and reduces time and cost of modifying model after finding problems by system realized. At last, an example is presented to show the enforceability and effectiveness of the approach

相似文献/References:

[1]翁辉 徐海珠 陈晓山.基于Petri网的装备战场抢修系统建模研究[J].计算机技术与发展,2010,(03):176.
　WENG Hui,XU Hai-zhu,CHEN Xiao-shan.Modeling Research on Equipment Battlefield Repair System Based on Petri Net[J].,2010,(09):176.
[2]李龙澍 胡正梁.基于Petri网的UML形式化建模应用分析[J].计算机技术与发展,2010,(04):76.
　LI Long-shu,HU Zheng-liang.Application Analysis and Formal Modeling of UML Based on Petri Net[J].,2010,(09):76.
[3]韩咚 田银花.基于赋时颜色Petri网的NSSK协议建模[J].计算机技术与发展,2010,(06):156.
　HAN Dong,TIAN Yin-hua.The Modeling of NSSK Protocols Based on Timed Colored Petri Nets[J].,2010,(09):156.
[4]徐晶明 杜宝珠.基于Petri网化简技术的工作流过程模型结构验证[J].计算机技术与发展,2009,(06):51.
　XU Jing-ming,DU Bao-zhu.Workflow Process Model Structure Verification Based on Petri Net Reduction Techniques[J].,2009,(09):51.
[5]胡文江 高永兵 樊瑞民 张健.基于Web服务的工作流执行优化方法探讨[J].计算机技术与发展,2009,(06):156.
　HU Wen-jiang,GAO Yong-bing,FAN Rui-min,et al.Research of Workflow Optimal Strategy Based on Web Services[J].,2009,(09):156.
[6]毛伟伟 于素萍.基于Petri网的Web服务动态组合[J].计算机技术与发展,2009,(11):61.
　MAO Wei-wei,YU Su-ping.Dynamic Web Service Composition Based on Petri Nets[J].,2009,(09):61.
[7]封会娟 于永利 张柳 刘文武.机动防空任务聚合级装备作战单元维修性仿真[J].计算机技术与发展,2009,(11):230.
　FENG Hui-juan,YU Yong-li,ZHANG Liu,et al.Simulation Model of Aggregated Equipment Combat Units＇ Mission Maintainability Based on Mobile Aerial Defense Mission[J].,2009,(09):230.
[8]陈伟 文东戈 王昊.层次颜色工作流Petri网建模与应用[J].计算机技术与发展,2009,(01):49.
　CHEN Wei,WEN Dong-ge,WANG Hao.Modeling and Application of Hierarchical Colored Workflow Net[J].,2009,(09):49.
[9]郭娟 许志才 方贤文.基于Petri网的Java多线程程序分析[J].计算机技术与发展,2009,(04):51.
　GUO Juan,XU Zhi-cai,FANG Xian-wen.Multi - Thread Analysis about Java Program Based on Petri Net[J].,2009,(09):51.
[10]秦凯 姜浩.一种基于Petri网的工作流模型分解方法[J].计算机技术与发展,2008,(01):97.
　QIN Kai,JIANG Hao.An Approach of Decomposition of Workflow Models Based on Petri Net[J].,2008,(09):97.

备注/Memo

备注/Memo:
国家自然科学基金（90818024）张辉（1983-），女，河北唐山人，工程师，研究方向为软件工程、高可信软件等
更新日期/Last Update: 1900-01-01