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
Formal semantics of the ProCom real-time component model
Mälardalen University, School of Innovation, Design and Engineering. (Industrial Software Engineering)ORCID iD: 0000-0003-2383-7981
Mälardalen University, School of Innovation, Design and Engineering. (Real-Time Systems Modelling and Analysis)
Mälardalen University, School of Innovation, Design and Engineering. (Industrial Software Engineering)ORCID iD: 0000-0002-8461-0230
Mälardalen University, School of Innovation, Design and Engineering. (Real-Time Systems Modelling and Analysis)ORCID iD: 0000-0003-2870-2680
Show others and affiliations
2009 (English)In: Proceedings of the 35th Euromicro Conference on Software Engineering and Advanced Applications 2009. SEAA 09, 2009, p. 478-485Conference paper, Published paper (Refereed)
Abstract [en]

ProCom is a new component model for real-timeand embedded systems, targeting the domains of vehicularand telecommunication systems. In this paper, we describehow the architectural elements of the ProCom componentmodel have been given a formal semantics. The semantics isgiven in a small but powerful finite state machine formalism,with notions of urgency, timing, and priorities. By definingthe semantics in this way, we (i) provide a rigorous and compactdescription of the modeling elements of ProCom, (ii) setthe ground for formal analysis using other formalisms, and(iii) provide an intuitive and useful description for bothpractitioners and researchers. To illustrate the approach,we exemplify with a number of particularly interestingcases, ranging from ports and services to components andcomponent hierarchies.

Place, publisher, year, edition, pages
2009. p. 478-485
Keywords [en]
real-time systems; embedded systems; component model, finite state machines; timed automata
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-6553DOI: 10.1109/SEAA.2009.53ISI: 000275857500069Scopus ID: 2-s2.0-74549208521ISBN: 978-076953784-9 (print)OAI: oai:DiVA.org:mdh-6553DiVA, id: diva2:227047
Conference
EUROMICRO2009 - 35th EUROMICRO Conference on Software Engineering and Advanced Applications, SEAA 2009; Patras; 27 August 2009 through 29 August 2009
Projects
PROGRESSAvailable from: 2009-07-08 Created: 2009-07-08 Last updated: 2013-12-19Bibliographically approved
In thesis
1. A Resource-Aware Component Model for Embedded Systems
Open this publication in new window or tab >>A Resource-Aware Component Model for Embedded Systems
2009 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Embedded systems are microprocessor-based systems that cover a large range of computer systems from ultra small computer-based devices to large systems monitoring and controlling complex processes. The particular constraints that must be met by embedded systems, such as timeliness, resource-use efficiency, short time-to-market and low cost, coupled with the increasing complexity of embedded system software, demand technologies and processes that will tackle these issues. An attractive approach to manage the software complexity, increase productivity, reduce time to market and decrease development costs, lies in the adoption of the component based software engineering (CBSE) paradigm. The specific characteristics of embedded systems lead to important design issues that need to be addressed by a component model. Consequently, a component model for development of embedded systems needs to systematically address extra-functional system properties. The component model should support predictable system development and as such guarantee absence or presence of certain properties. Formal methods can be a suitable solution to guarantee the correctness and reliability of software systems.

 

Following the CBSE spirit, in this thesis we introduce the ProCom component model for development of distributed embedded systems. ProCom is structured in two layers, in order to support both a high-level view of loosely coupled subsystems encapsulating complex functionality, and a low-level view of control loops with restricted functionality. These layers differ from each other in terms of execution model, communication style, synchronization etc., but also in kind of analysis which are suitable. To describe the internal behavior of a component, in a structured way, in this thesis we propose REsource Model for Embedded Systems (REMES) that describes both functional and extra-functional behavior of interacting embedded components. We also formalize the resource-wise properties of interest and show how to analyze such behavioral models against them.

Place, publisher, year, edition, pages
Västerås: Mälardalens högskola, 2009
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 108
Keywords
component based software engineering, formal modeling, embedded systems, resources, analysis, behavior, component model
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-6681 (URN)978-91-86135-37-9 (ISBN)
Presentation
2009-09-17, Zeta, Västerås, 14:15 (English)
Opponent
Supervisors
Projects
PROGRESS
Available from: 2009-08-25 Created: 2009-08-25 Last updated: 2018-01-13Bibliographically approved
2. Design and Analysis Support for Abstract Models of Component-based Embedded Systems
Open this publication in new window or tab >>Design and Analysis Support for Abstract Models of Component-based Embedded Systems
2011 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Developing industrial real-time software systems is challenging due to de- mands on system safety and reliability, through stringent system requirements in terms of functionality, timing, resource consumption etc. Due to this, the system development needs to ensure predictability before the actual imple- mentation, through reliable engineering methods. To address these challenges, model-based engineering (MBE) combined with Component-based develop- ment (CBD) has emerged as a feasible solution. MBE supports system model- ing and formal analysis through the development phases such as requirements, specification, and design. CBD supports reusability of software parts leading to faster development time, and reduced costs. However, an integrated approach needs to deal with various abstractions of the system during different phases of the development.

In this thesis, we present model-based techniques, for the development of predictable, component-based designs of embedded systems. We consider Pro- Com as the underlying component model and, as a first step, we define a for- mal semantics for its architectural elements. The given semantics provides a basis for developing analyzable embedded systems designs, associated analy- sis techniques, model transformations etc. Next, we describe some commonly- found behavioral patterns, in component-based designs. These patterns provide an abstract, and reusable specification of a real-time components functional- ity. Also, we define component-based design templates, intended to support the systematic development of component-based designs from abstract system models. Finally, we propose a formal framework to correlate statemachine- based system behavior with corresponding ProCom-based system designs. We validate our research contributions using case-studies and examples, and also by applying verification techniques, such as, model-checking.

 

Place, publisher, year, edition, pages
Västerås: Mälardalen University, 2011
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 132
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-12251 (URN)978-91-7485-016-1 (ISBN)
Presentation
2011-06-08, Lambda, Mälardalen University, Västerås, 13:30
Opponent
Supervisors
Projects
PROGRESSARROWS
Funder
Swedish Research Council
Available from: 2011-05-13 Created: 2011-05-12 Last updated: 2011-06-03Bibliographically approved
3. 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

Other links

Publisher's full textScopus

Authority records BETA

Vulgarakis, AnetaCarlson, JanSeceleanu, CristinaPettersson, Paul

Search in DiVA

By author/editor
Vulgarakis, AnetaSuryadevara, JagadishCarlson, JanSeceleanu, CristinaPettersson, Paul
By organisation
School of Innovation, Design and Engineering

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

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