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
Software Engineering and Formal Methods
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded Systems))
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded Systems))ORCID iD: 0000-0003-2870-2680
Univ. of Nice .
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded Systems))ORCID iD: 0000-0003-4040-3480
2013 (English)In: Software Engineering and Formal Methods: 11th International Conference, SEFM 2013, Madrid, Spain, September 25-27, 2013. Proceedings, Springer, 2013, p. 1-15Chapter in book (Refereed)
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 system’s 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. On the one hand, CCSL is an expressive language that supports specification of both logical and chronometric constraints associated with MARTE models. On the other hand, semantic frameworks such as Timed Automata provide verification support for real-time systems. To tackle the challenge of verifying CCSL-based system properties, 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
Springer, 2013. p. 1-15
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8137
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:mdh:diva-21371ISI: 000335436800001ISBN: 978-3-642-40561-7 (print)ISBN: 978-3-642-40560-0 (print)OAI: oai:DiVA.org:mdh-21371DiVA, id: diva2:648948
Conference
11th International Conference on Software Engineering and Formal Methods, September 25-27. 2013, Madrid, Spain
Projects
ARROWS - Design Techniques for Adaptive Embedded SystemsAvailable from: 2013-09-17 Created: 2013-09-11 Last updated: 2015-11-13Bibliographically approved
In thesis
1. Model Based Development of Embedded Systems using Logical Clock Constraints and Timed Automata
Open this publication in new window or tab >>Model Based Development of Embedded Systems using Logical Clock Constraints and Timed Automata
2013 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

In modern times, human life is intrinsically depending on real-time embedded systems (RTES) with increasingly safety-critical and mission-critical features, for instance, in domains such as automotive and avionics. These systems are characterized by stringent functional requirements and require predictable timing behavior. However, the complexity of RTES has been ever increasing requiring systematic development methods. To address these concerns, model-based frameworks and component-based design methodologies have emerged as a feasible solution. Further, system artifacts such as requirements/specifications, architectural designs as well as behavioral models like statemachine views are integrated within the development process. However, several challenges remain to be addressed, out of which two are especially important: expressiveness, to represent the real-time and causality behavior, and analyzability, to support verification of functional and timing behavior.

As the main research contribution, this thesis presents design and verification techniques for model-based development of RTES, addressing expressiveness and analyzability for architectural and behavioral models. To begin with, we have proposed a systematic design process to support component-based development. Next, we have provided a real-time semantic basis, in order to support expressiveness and verification for structural and behavioral models. This is achieved by defining an intuitive formal semantics for real-time component models, using ProCom, a component model developed at our research centre, and also using the CCSL (Clock Constraint Specification Language), an expressive language for specification of timed causality behavior. This paves the way for formal verification of both architectural and behavioral models, using model checking, as we show in this work, by transforming the models into timed automata and performing verification using UPPAAL, a model checking tool based on timed automata. Finally, the research contributions are validated using representative examples of RTES as well as an industrial case-study.

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2013
Series
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 146
Keywords
Embedded Systems, Model-based development, Model-Checking, Architectural Modeling, CCSL, Timed Automata
National Category
Embedded Systems
Identifiers
urn:nbn:se:mdh:diva-22328 (URN)978-91-7485-123-6 (ISBN)
Public defence
2013-12-09, Kappa, Mälardalen University, Västerås, 13:15 (English)
Opponent
Supervisors
Projects
ARROWS
Funder
Swedish Research Council, 2270 430 16243
Available from: 2013-11-01 Created: 2013-11-01 Last updated: 2013-11-18Bibliographically approved

Open Access in DiVA

No full text in DiVA

Authority records BETA

Seceleanu, CristinaPettersson, Paul

Search in DiVA

By author/editor
Suryadevara, JagadishSeceleanu, CristinaPettersson, Paul
By organisation
Embedded Systems
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

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