计算机科学 ›› 2016, Vol. 43 ›› Issue (1): 211-217.doi: 10.11896/j.issn.1002-137X.2016.01.047
沈宁敏,李静,白海洋,庄毅
SHEN Ning-min, LI Jing, BAI Hai-yang and ZHUANG Yi
摘要： 体系结构分析设计语言AADL是一种可支持软硬件一体化建模及同一模型多元分析的形式化与图形化建模语言。采用时间自动机形式化模型检验方法对AADL模型中的数据流进行转换和验证。考虑到单一数据流与混合数据流的差异性,分别设计了数据流到时间自动机模型的转换规则,并通过时间自动机网络实现数据流的综合分析。设计开发了自动化模型转换的插件AADLToUppaal Plug-in,将其嵌入到OSTATE工具中,使用时间自动机建模与验证工具Uppaal对转换得到的时间自动机进行模拟和验证,等价地验证所设计的AADL模型数据流时延是否满足系统实时性要求。仿真实验结果表明,所设计的数据流模型转换方法能有效地将AADL模型转换到时间自动机模型,并能在Uppaal中正确地分析原模型的数据流时延特性。
| [1] Krishna C M.Real-Time Systems[M].John Wiley & Sons,Inc.,1999 [2] Kleppe A G,Warmer J B,Bast W.MDA explained,the model driven architecture:Practice and promise[M].Addison-Wesley Professional,2003 [3] Feiler P H,Gluch D P,Hudak J J.The architecture analysis & design language (AADL):An introduction[R].Carnegie-Mellon Univ Pittsburgh PA Software Engineering Inst,2006 [4] Feiler P H,Lewis B A,Vestal S.The SAE Architecture Analysis & Design Language (AADL) a standard for engineering performance critical systems[C]∥ IEEE International Symposium on Computer Aided Control System Design.Washington:IEEE Computer Society Press,2006:1206-1211 [5] Feiler P H,Hansson J.Flow latency analysis with the architecture analysis and design language (aadl): Technical Note CMU/SEI-2007-IN-010[R].Software Engineering,Institute,2007 [6] Lee S Y,Mallet F,De Simone R.Dealing with AADL End-to-end Flow Latency with UML MARTE[C]∥13th IEEE International Conference on Engineering of Complex Computer Systems,2008(ICECCS 2008).IEEE,2008:228-233 [7] Jiao Ting-ting,Wang Le,Ye Guo-dong.Software ReliabilityVerification based on AADL[J].Journal of Computer Application,2012,32(A02):92-95 [8] Peled D.Software reliability methods[M].Springer,2001 [9] Amnell T,Fersman E,Mokrushin L,et al.TIMES:a tool for schedulability analysis and code generation of real-time systems[M].Springer Berlin Heidelberg,2004 [10] Fersman E,Mokrushin L,Pettersson P,et al.Schedulabilityanalysis of fixed-priority systems using timed automata[J].Theo-retical Computer Science,2006,354(2):301-317 [11] Zhang Y,Dong Y,Zhang Y,et al.A study of the AADL mode based on timed automata[C]∥2011 IEEE 2nd International Conference on Software Engineering and Service Science (ICSESS).IEEE,2011:224-227 [12] Wei L,Shuyu L.Research on the Formalization of AADL Model[C]∥2013 Fifth International Conference on Computational and Information Sciences (ICCIS).IEEE,2013:72-75 [13] Alur R,Dill D.The theory of timed automata[C]∥Real-Time:Theory in Practice.Springer Berlin Heidelberg,1992:45-73 [14] Johnsen A.Architecture-Based Verification of Dependable Embedded Systems[D].Mlardalen University,2013 [15] Yovine S.Model checking timed automata[M].Springer Berlin Heidelberg,1998 [16] Alur R.Timed automata[M]∥Verification of Digital and Hybrid Systems.Springer Berlin Heidelberg,2000:233-264 [17] Bjrnander S,Seceleanu C,Lundqvist K,et al.A Formal Analysis Framework for AADL[J].The Journal of Science and Technology,2011,49(5):105-118 [18] Alur R,Dill D L.A theory of timed automata[J].Theoretical Computer Science,1994,126(2):183-235 [19] Alur R.Timed automata[M]∥Computer Aided Verification.Springer Berlin Heidelberg,1999:8-22 [20] Gui S,Luo L,Li Y,et al.Formal schedulability analysis and si-mulation for AADL[C]∥International Conference on Embedded Software and Systems,2008(ICESS’08).IEEE,2008:429-435 [21] Abdeddaim Y,Maler O.Job-Shop Scheduling Using Timed Automata?[M]∥Computer Aided Verification.Springer Berlin Heidelberg,2001:478-492 [22] Abdoul T,Champeau J,Dhaussy P T,et al.AADL execution semantics transformation for formal verification[C]∥13th IEEE International Conference on Engineering of Complex Computer Systems,2008(ICECCS 2008).IEEE,2008:263-268 |
| No related articles found! |
|
||
首页