Advertisement

Timed Simulation of Extended AADL-Based Architecture Specifications with Timed Abstract State Machines

  • Stefan Björnander
  • Lars Grunske
  • Kristina Lundqvist
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5581)

Abstract

The Architecture Analysis and Design Language (AADL) is a popular language for architectural modeling and analysis of software intensive systems in application domains such as automotive, avionics, railway and medical systems. These systems often have stringent real-time requirements. This paper presents an extension to AADL’s behavior model using time annotations in order to improve the evaluation of timing properties in AADL. The translational semantics of this extension is based on mappings to the Timed Abstract State Machines (TASM) language. As a result, timing analysis with timed simulation or timed model checking is possible. The translation is supported by an Eclipse-based plug-in and the approach is validated with a case study of an industrial production cell system.

Keywords

AADL Behavior Annex TASM Translation 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 414–425. IEEE Computer Society Press, Los Alamitos (1990)CrossRefGoogle Scholar
  2. 2.
    Grunske, L.: Early quality prediction of component-based systems - A generic framework. Journal of Systems and Software 80, 678–686 (2007)CrossRefGoogle Scholar
  3. 3.
    Yovine, S.: Model checking timed automata. In: Rozenberg, G. (ed.) EEF School 1996. LNCS, vol. 1494, pp. 114–124. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. 4.
    Feiler, P.H., Gluch, D.P., Hudak, J.J.: The Architecture Analysis and Design Language (AADL): An Introduction. Technical Report CMU/SEI-2006-TN-011, Society of Automotive Engineers (2006)Google Scholar
  5. 5.
    Feiler, P., Lewis, B.: SAE Architecture Analysis and Design Language (AADL) Annex Volume 1. Technical Report AS5506/1, Society of Automobile Engineers (2006)Google Scholar
  6. 6.
    Ouimet, M., Lundqvist, K.: The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 126–130. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Lynch, N.: Modeling and verification of automated transit systems, using timed automata, invariants, and simulations. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 449–459. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  8. 8.
    Lewerentz, C., Lindner, T.: Formal development of reactive systems, case study production cell. In: Lewerentz, C., Lindner, T. (eds.) Formal Development of Reactive Systems. LNCS, vol. 891, pp. 21–54. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  9. 9.
    Ouimet, M., Lundqvist, K.: Modeling the Production Cell System in the TASM Language. Technical Report ESL-TIK-00209, Embedded Systems Laboratory, Massachusetts Institute of Technology, Cambridge, MA, 02139, USA (2007)Google Scholar
  10. 10.
    Vestal, S.: Formal verification of the metaH executive using linear hybrid automata. In: Proceedings of the Sixth IEEE Real-Time Technology and Applications Symposium (RTAS 2000), pp. 134–144. IEEE, Washington (2000)CrossRefGoogle Scholar
  11. 11.
    Miles, R., Hamilton, K.: Learning UML 2.0. O’Reilly Media, Sebastopol (2006)Google Scholar
  12. 12.
    Pilone, D., Pitman, N.: UML 2.0 in a Nutshell, 2nd edn. O’Reilly Media, Sebastopol (2005)Google Scholar
  13. 13.
    Ouimet, M., Lundqvist, K.: The TASM Language and the Hi-Five Framework: Specification, Validation, and Verification of Embedded Real-Time Systems. In: Asia-Pacific Software Engineering Conference (2007)Google Scholar
  14. 14.
    Ouimet, M., Lundqvist, K.: The TASM Language Reference Manual, Version 1.1, Massachusetts Institute of Technology, Cambridge, MA, 02139, USA (2006)Google Scholar
  15. 15.
    França, R.B., Bodeveix, J.P., Filali, M., Rolland, J.F., Chemouil, D., Thomas, D.: The AADL behaviour annex - experiments and roadmap. In: ICECCS, pp. 377–382. IEEE Computer Society, Los Alamitos (2007)Google Scholar
  16. 16.
    Börger, E., Stärk, R.: Abstract State Machines - A Method for High-level System Design and Analysis. Springer, Heidelberg (2003)CrossRefzbMATHGoogle Scholar
  17. 17.
    Behrmann, G., David, A., Larsen, K.G.: A Tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  18. 18.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Bengtsson, J., Wang, Y.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. 20.
    Winkowski, J.: Processes of Timed Petri Nets. TCS: Theoretical Computer Science 243 (2000)Google Scholar
  21. 21.
    Colvin, R., Grunske, L., Winter, K.: Probabilistic timed behavior trees. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 156–175. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  22. 22.
    Colvin, R., Grunske, L., Winter, K.: Timed behavior trees for failure mode and effects analysis of time-critical systems. Journal of Systems and Software 81, 2163–2182 (2008)CrossRefGoogle Scholar
  23. 23.
    Grunske, L., Winter, K., Colvin, R.: Timed Behavior Trees and their Application to Verifying Real-time Systems. In: Proceedings of the 18th Australian Conference on Software Engineering (ASWEC 2007), pp. 211–220. IEEE Computer Society, Los Alamitos (2007)CrossRefGoogle Scholar
  24. 24.
    Dong, J.S., Hao, P., Qin, S.C., Sun, J., Wang, Y.: Timed patterns: Tcoz to timed automata. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 483–498. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  25. 25.
    Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The Tool KRONOS. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 208–219. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  26. 26.
    Ouimet, M., Lundqvist, K.: A Mapping between the Timed Abstract State Machine Language and UPPAAL’s Timed Automata. Technical Report ESL-TIK-00212, Embedded Systems Laboratory, Massachusetts Institute of Technology, Cambridge, MA, 02139, USA (2007)Google Scholar
  27. 27.
    Schneider, S.: An operational semantics for timed CSP. Information and Computation 116, 193–213 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Dong, J.S., Duke, R., Hao, P.: Integrating object-z with timed automata. In: Int. Conference on Engineering of Complex Computer Systems (ICECCS 2005), pp. 488–497. IEEE Computer Society, Los Alamitos (2005)Google Scholar
  29. 29.
    Smith, G., Hayes, I.: An introduction to real-time object-z. Formal Aspects of Computing 13, 128–141 (2002)CrossRefzbMATHGoogle Scholar
  30. 30.
    Feiler, P.H., Gluch, D.P., Hudak, J.J., Lewis, B.A.: Embedded Systems Architecture Analysis Using SAE AADL. Technical report, CMU/SEI-2004-TN-005 (2004)Google Scholar
  31. 31.
    Singhoff, F., Legrand, J., Nana, L., Marcé, L.: Scheduling and memory requirements analysis with AADL. ACM SIGADA Ada Letters 25, 1–10 (2005)CrossRefGoogle Scholar
  32. 32.
    Feiler, P., Rugina, A.: Dependability modeling with the architecture analysis and design language (AADL). Technical Report CMU/SEI-2007-TN-043, Carnegie Mellon University (2007)Google Scholar
  33. 33.
    Grunske, L., Han, J.: A Comparative Study into Architecture-Based Safety Evaluation Methodologies Using AADL’s Error Annex and Failure Propagation Models. In: 11th IEEE High Assurance Systems Engineering Symposium, HASE 2008, pp. 283–292. IEEE Computer Society, Los Alamitos (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Stefan Björnander
    • 1
  • Lars Grunske
    • 2
  • Kristina Lundqvist
    • 1
  1. 1.School of IDEMälardalen UniversityVästeråsSweden
  2. 2.Faculty of ICTSwinburne University of TechnologyHawthornAustralia

Personalised recommendations