Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Verifying System Behaviors in EAST-ADL2 with the SPIN ModelChecker
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Embedded Systems.ORCID iD: 0000-0001-5703-5923
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Embedded Systems.ORCID iD: 0000-0001-7048-0108
Volvo Technology AB.
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Embedded Systems.ORCID iD: 0000-0002-4300-885X
2010 (English)Conference paper, Published paper (Refereed)
Abstract [en]

EAST-ADL2 is a domain-specific architecture descriptionlanguage to support the model-based developmentof automotive embedded systems. It emerged to manage thecomplexity of software and electronics in advanced automotiveapplications. The language focuses on the structural definitionfor functional specifications. Behavior is defined only on thecomponent level, in terms of functional blocks and their triggersand interfaces. The behavioral definition inside each functionalblock is not prescribed. This paper shows one approachto augment the language with precise syntax and semanticsfor behavior, and develops a procedure that transforms thecomposed behavioral model to the SPIN model for logicmodel checking. The contribution improves the modeling andverification capability of EAST-ADL2.

Place, publisher, year, edition, pages
2010.
National Category
Embedded Systems
Identifiers
URN: urn:nbn:se:kth:diva-80970DOI: 10.1109/ICMA.2010.5588261Scopus ID: 2-s2.0-78649260654OAI: oai:DiVA.org:kth-80970DiVA: diva2:496939
Conference
IEEE International Conference on Mechatronics and Automation
Projects
EAST-ADL, verification, model-checking, fomal analysis, embedded systems
Funder
EU, FP7, Seventh Framework Programme, 224442
Note
QC 20120213Available from: 2012-02-10 Created: 2012-02-10 Last updated: 2012-02-13Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Feng, LeiChen, DeJiuTörngren, Martin

Search in DiVA

By author/editor
Feng, LeiChen, DeJiuTörngren, Martin
By organisation
Embedded Systems
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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