mdh.sePublications
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
Verifying functional behaviors of automotive products in EAST-ADL2 using UPPAAL-PORT
Mälardalen University, School of Innovation, Design and Engineering. University of Namur, Belgium.
University of Namur, Belgium.
Mälardalen University, School of Innovation, Design and Engineering.ORCID iD: 0000-0003-4040-3480
2011 (English)In: Computer Safety, Reliability, and Security: 30th International Conference,SAFECOMP 2011, Naples, Italy, September 19-22, 2011. Proceedings, 2011, 243-256 p.Conference paper, Published paper (Refereed)
Abstract [en]

We study the use of formal modeling and verification techniques at an early stage in the development of safety-critical automotive products which are originally described in the domain specific architectural language EAST-ADL2. This architectural language only focuses on the structural definition of functional blocks. However, the behavior inside each functional block is not specified and that limits formal modeling and analysis of systems behaviors as well as efficient verification of safety properties. In this paper, we tackle this problem by proposing one modeling approach, which formally captures the behavioral execution inside each functional block and their interactions, and helps to improve the formal modeling and verification capability of EAST-ADL2: the behavior of each elementary function of EAST-ADL2 is specified in UPPAAL Timed Automata. The formal syntax and semantics are defined in order to specify the behavior model inside EAST-ADL2 and their interactions. A composition of the functional behaviors is considered a network of Timed Automata that enables us to verify behaviors of the entire system using the UPPAAL model checker. The method has been demonstrated by verifying the safety of the Brake-by-wire system design.

Place, publisher, year, edition, pages
2011. 243-256 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6894
National Category
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-13658DOI: 10.1007/978-3-642-24270-0_18Scopus ID: 2-s2.0-80052983092ISBN: 978-3-642-24269-4 (print)OAI: oai:DiVA.org:mdh-13658DiVA: diva2:466202
Conference
30th International Conference,SAFECOMP 2011, Naples, Italy, September 19-22, 2011
Available from: 2011-12-15 Created: 2011-12-15 Last updated: 2015-09-15Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Search in DiVA

By author/editor
Pettersson, Paul
By organisation
School of Innovation, Design and Engineering
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 23 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