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 MARTE/CCSL mode behaviors using UPPAAL
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-2870-2680
Aoste Team-project INRIA/I3S, Sophia-Antipolis, France.
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0003-4040-3480
2013 (English)In: Lect. Notes Comput. Sci., 2013, 1-15 p.Conference paper, Published paper (Refereed)
Resource type
Text
Abstract [en]

In the development of safety-critical embedded systems, the ability to formally analyze system behavior models, based on timing and causality, helps the designer to get insight into the systems overall timing behavior. To support the design and analysis of real-time embedded systems, the UML modeling profile MARTE provides CCSL - a time model and a clock constraint specification language. CCSL is an expressive language that supports specification of both logical and chronometric constraints for MARTE models. On the other hand, semantic frameworks such as timed automata provide verification support for real-time systems. To address the challenge of verifying CCSL-based behavior models, in this paper, we propose a technique for transforming MARTE/CCSL mode behaviors into Timed Automata for model-checking using the UPPAAL tool. This enables verification of both logical and chronometric properties of the system, which has not been possible before. We demonstrate the proposed transformation and verification approach using two relevant examples of real-time embedded systems.

Place, publisher, year, edition, pages
2013. 1-15 p.
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8137 LNCS
Keyword [en]
CCSL, MARTE, Model-checking, Modes, UPPAAL, Verification, Design and analysis, Real-time embedded systems, Safety-critical embedded systems, Semantic framework, Embedded systems, Model checking, Real time systems, Semantics, Software engineering, Specification languages, Automata theory
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
URN: urn:nbn:se:mdh:diva-31632DOI: 10.1007/978-3-642-40561-7_1Scopus ID: 2-s2.0-84885934061ISBN: 9783642405600 (print)OAI: oai:DiVA.org:mdh-31632DiVA: diva2:930513
Conference
25 September 2013 through 27 September 2013, Madrid
Available from: 2016-05-24 Created: 2016-05-24 Last updated: 2016-05-24Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full textScopus

Authority records BETA

Seceleanu, CristinaPettersson, Paul

Search in DiVA

By author/editor
Suryadevara, JagadishSeceleanu, CristinaPettersson, Paul
By organisation
Embedded Systems
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 6 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