Computer Science ›› 2016, Vol. 43 ›› Issue (1): 211-217.doi: 10.11896/j.issn.1002-137X.2016.01.047

Previous Articles     Next Articles

Transformation and Verification Method of AADL Data Flows for Real-time System Using Uppaal

SHEN Ning-min, LI Jing, BAI Hai-yang and ZHUANG Yi   

  • Online:2018-12-01 Published:2018-12-01

Abstract: Architecture analysis and design language (AADL) is a modeling language for formalization and graphics,which can support integrated modeling and multi-analysis.We used timed automata formal checking method to transform and verif y data flow in AADL models.Considering the difference between single data flow and mixed data flows,we designed corresponding transformation rules from AADL models to timed automata,and analyzed and verified the data flow comprehensively by establishing timed automata network.An automated model conversion Eclipse plug-in was designed and integrated into the AADL modeling tool OSATE.Finally,timed automata modeling and Uppaal were used to simulate and verify the transformed timed automata while verifying whether the AADL model equivalently satisfies the real-time requirement of system.Experimental results show that the model transformation method is valid and flow latency qualities can be verified effectively with Uppaal.

Key words: AADL,Timed automata,Data flow latency,Uppaal,Software verification

[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].Mlardalen 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] Bjrnander 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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!