Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
ViTAL : A Verification Tool for EAST-ADL Models using UPPAAL PORT
Mälardalen University. (MRTC)ORCID iD: 0000-0003-2416-4205
Mälardalen University, School of Innovation, Design and Engineering. (IS)ORCID iD: 0000-0002-7663-5497
Mälardalen University, School of Innovation, Design and Engineering. (IS)ORCID iD: 0000-0003-2870-2680
Mälardalen University, School of Innovation, Design and Engineering. (IS)ORCID iD: 0000-0003-4040-3480
2012 (English)In: Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, Paris, France, 2012, 328-337 p.Conference paper, Published paper (Refereed)
Abstract [en]

A system’s architecture influence on the functions and other properties of embedded systems makes its high level analysis and verification very desirable. EAST-ADL is an architecture description language dedicated to automotive embedded system design with focus on structural and functional modeling. The behavioral description is not integrated within the execution semantics, which makes it harder to transform, analyze, and verify EAST-ADL models. Model-based techniques help address this issue by enabling automated transformation between different design models, and providing means for simulation and verification. We present a verification tool, called ViTAL, which provides the possibility to express the functional EAST-ADL behavior as timed automata models, which have precise semantics and can be formally verified. The ViTAL tool enables the transformation of EAST-ADL functional models to the UPPAAL PORT tool for model checking. This method improves the verification of functional and timing requirements in EAST-ADL, and makes it possible to identify dependencies and potential conflicts between different vehicle functions before the actual AUTOSAR implementation.

Place, publisher, year, edition, pages
Paris, France, 2012. 328-337 p.
Keyword [en]
UPPAAL PORT, EAST ADL, functional modeling, behavioral description, model checking
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-14603DOI: 10.1109/ICECCS.2012.42ISI: 000315026500034Scopus ID: 2-s2.0-84867971602ISBN: 978-295418100-4 (print)OAI: oai:DiVA.org:mdh-14603DiVA: diva2:526561
Conference
2012 IEEE 17th International Conference on Engineering of Complex Computer Systems, ICECCS 2012; Paris; 18 July 2012 through 20 July 2012
Projects
ATAC, MBAT
Available from: 2012-05-18 Created: 2012-05-14 Last updated: 2016-05-11Bibliographically approved

Open Access in DiVA

fulltext(1057 kB)914 downloads
File information
File name FULLTEXT01.pdfFile size 1057 kBChecksum SHA-512
2cac8a46bc699d7ab1ac55b8cb421a3cf6a3fbb2884e73a3490144c894c3faac105303d5171c11452a5bac8d18bcb26b88edc51560cefdae0baddb238d8d0380
Type fulltextMimetype application/pdf

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Enoiu, Eduard PaulMarinescu, RalucaSeceleanu, CristinaPaul, Pettersson
By organisation
Mälardalen UniversitySchool of Innovation, Design and Engineering
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 914 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 64 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf