Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Introduction: Modeling, Analysis and Synthesis of Embedded Software and Systems Read chapter Read first chapter

2014 | OriginalPaper | Chapter

5. On Integrating EAST-ADL and UPPAAL for Embedded System Architecture Verification

Authors : Tahir Naseer Qureshi, De-Jiu Chen, Magnus Persson, Martin Törngren

Published in: Embedded Systems Development

Publisher: Springer New York

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Model-based development (MBD) is a common approach adopted in many engineering disciplines for handling complexity. For distributed microprocessor based systems MBD approaches include the use of architecture description languages (ADL’s), modeling and simulation tools and tools for formal verification. To increase their combined effectiveness, the various MBD methods, tools and languages are required to be integrated with each other. This chapter addresses the connection between ADL’s and formal verification in the context of automotive embedded systems. A template-based mapping scheme providing formal interpretation of EAST-ADL, an automotive specific ADL with timed automata (TA) is the main contribution providing a possibility of automated analysis of timing constraints specified for the execution behavior and events of a system. One benefit of using TA is the fact that it can also be used for generating test cases for their usage during late development phases.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
previous chapter Model-Driven Design of Software Defined Radio Applications Based on UML
next chapter Schedulability Analysis at Early Design Stages with MARTE
Footnotes
Literature
1.
Törngren, M., Chen, D., Malvius, D., Axelsson, J.: Automotive embedded systems handbook. In: Model-Based Development of Automotive Embedded Systems. CRC Press, Boca Raton, FL (2009)
2.
Lönn, H., Freund, U.: Automotive embedded systems handbook. In: Automotive Architecture Description Languages, CRC Press, Boca Raton, FL (2009)
3.
Broy, M., Feilkas, M., Herrmannsdoerfer, M., Merenda, S., Ratiu, D.: Seamless model-based development: from isolated tools to integrated model engineering environments. Proc. IEEE 98(4), 526–545 (2010)CrossRef
4.
5.
Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Lectures on Concurrency and Petri Nets, LNCS, vol. 3098, pp. 87–124. Springer, Berlin (2004)
6.
Hendriks, M., Verhoef, M.: Timed automata based analysis of embedded system architectures. In: Parallel and Distributed Processing Symposium, 2006. IPDPS 2006. 20th, International, p. 8 (2006)
7.
Ponsard, C., Massonet, P., Molderez, J.F., Rifaut, A., Lamsweerde, A.V., Van, H.T.: Early verification and validation of mission critical systems. Form. Methods Syst. Des. 30(3), 233–247 (2007)MATHCrossRef
8.
Montag, P., Nowotka, D., Levi, P.: Verification in the design process of large real-time systems: a case study. In: Automotive Safety and Security 2006, Stuttgart (Germany), October 12–13, 2006, pp. 1–13 (2006)
9.
Qureshi, T.N., Chen, D.J., Persson, M., Törngren, M.: Towards the integration of UPPAAL for formal verification of EAST-ADL timing constraint specification. In: Workshop on Time Analysis and Model-Based Design, from Functional Models to Distributed Deployments (2011)
10.
Qureshi, T.N., Chen, D.J., Törngren, M.: A timed automata-based method to analyze EAST-ADL timing constraint specifications. In: Modelling Foundations and Applications, Lecture Notes in Computer Science, vol. 7349, pp. 303–318. Springer, Berlin (2012)
11.
Feng, L., Chen, D.J., Lönn, H., Törngren, M.: Verifying system behaviors in EAST-ADL2 with the SPIN model checker. In: Mechatronics and Automation (ICMA), 2010 International Conference on, pp. 144–149 (2010)
12.
Kang, E.Y., Schobbens, P.Y., Pettersson, P.: Verifying functional behaviors of automotive products in EAST-ADL2 Using UPPAAL-PORT. In: Computer Safety, Reliability, and Security, LNCS, vol. 6894, pp. 243–256. Springer, Berlin (2011)
13.
Enoiu, E.P., Marinescu, R., Seceleanu, C., Pettersson, P.: ViTAL : A verification tool for EAST-ADL models using UPPAAL PORT. In: Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems. IEEE Computer Society Press (2012)
14.
Qureshi, T.N.: Enhancing model-based development of embedded systems: modeling, simulation and model-transformation in an automotive context. Trita-mmk, issn 1400–1179; 2012:16, isbn 978-91-7501-465-4, Department of Machine Design, KTH - The Royal Institute of Technology, Sweden (2012)
15.
Stappert, F., Jonsson, J., Mottok, J., Johansson, R.: A design framework for End-To-End timing constrained automotive applications. Embedded Real-Time Software and Systems (ERTS’10) (2010)
16.
17.
Zhao, Y.: On the design of concurrent, distributed real-time systems. Ph.D. thesis, EECS Department, University of California, Berkeley (2009)
18.
19.
Anssi, S., Tucci-Pergiovanni, S., Mraidha, C., Albinet, A., Terrier, F., Gerard, S.: Completing EAST-ADL2 with MARTE for Enabling Scheduling Analysis for Automotive Applications. Conference ERTS, In (2010)
20.
Cuenot, P., Frey, P., Johansson, R., Lönn, H., Reiser, M.O., Servat, D., Tavakoli Kolagari, R., Chen, D.: Developing automotive products using the EAST-ADL2, an AUTOSAR compliant architecture description language. In: Proceedings of the 4th European Congress ERTS (Embedded Real Time Software) (2008)
21.
Qureshi, T.N., Chen, D., Lönn, H., Törngren, M.: From EAST-ADL to AUTOSAR. Tech. Rep. TRITA-MMK 2011:12, ISSN 1400–1179, ISRN/KTH/MMK/R-11/12-SE, Mechatronics Lab, Department of Machine Design, KTH, Stockholm, Sweden (2011)
Metadata
Title
On Integrating EAST-ADL and UPPAAL for Embedded System Architecture Verification
Authors
Tahir Naseer Qureshi
De-Jiu Chen
Magnus Persson
Martin Törngren
Copyright Year
2014
Publisher
Springer New York
Book
Embedded Systems Development

Print ISBN: 978-1-4614-3878-6

Electronic ISBN: 978-1-4614-3879-3

Copyright Year: 2014

DOI
https://doi.org/10.1007/978-1-4614-3879-3_5