mdh.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Formal semantics of the ProCom real-time component model
Mälardalens högskola, Akademin för innovation, design och teknik. (Industrial Software Engineering)ORCID-id: 0000-0003-2383-7981
Mälardalens högskola, Akademin för innovation, design och teknik. (Real-Time Systems Modelling and Analysis)
Mälardalens högskola, Akademin för innovation, design och teknik. (Industrial Software Engineering)ORCID-id: 0000-0002-8461-0230
Mälardalens högskola, Akademin för innovation, design och teknik. (Real-Time Systems Modelling and Analysis)ORCID-id: 0000-0003-2870-2680
Visa övriga samt affilieringar
2009 (Engelska)Ingår i: Proceedings of the 35th Euromicro Conference on Software Engineering and Advanced Applications 2009. SEAA 09, 2009, s. 478-485Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
2009. s. 478-485
Nyckelord [en]
real-time systems; embedded systems; component model, finite state machines; timed automata
Forskningsämne
datavetenskap
Identifikatorer
URN: urn:nbn:se:mdh:diva-6553DOI: 10.1109/SEAA.2009.53ISI: 000275857500069Scopus ID: 2-s2.0-74549208521ISBN: 978-076953784-9 (tryckt)OAI: oai:DiVA.org:mdh-6553DiVA, id: diva2:227047
Konferens
EUROMICRO2009 - 35th EUROMICRO Conference on Software Engineering and Advanced Applications, SEAA 2009; Patras; 27 August 2009 through 29 August 2009
Projekt
PROGRESSTillgänglig från: 2009-07-08 Skapad: 2009-07-08 Senast uppdaterad: 2013-12-19Bibliografiskt granskad
Ingår i avhandling
1. A Resource-Aware Component Model for Embedded Systems
Öppna denna publikation i ny flik eller fönster >>A Resource-Aware Component Model for Embedded Systems
2009 (Engelska)Licentiatavhandling, sammanläggning (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Västerås: Mälardalens högskola, 2009
Serie
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 108
Nyckelord
component based software engineering, formal modeling, embedded systems, resources, analysis, behavior, component model
Nationell ämneskategori
Datavetenskap (datalogi)
Forskningsämne
Datavetenskap
Identifikatorer
urn:nbn:se:mdh:diva-6681 (URN)978-91-86135-37-9 (ISBN)
Presentation
2009-09-17, Zeta, Västerås, 14:15 (Engelska)
Opponent
Handledare
Projekt
PROGRESS
Tillgänglig från: 2009-08-25 Skapad: 2009-08-25 Senast uppdaterad: 2018-01-13Bibliografiskt granskad
2. Design and Analysis Support for Abstract Models of Component-based Embedded Systems
Öppna denna publikation i ny flik eller fönster >>Design and Analysis Support for Abstract Models of Component-based Embedded Systems
2011 (Engelska)Licentiatavhandling, sammanläggning (Övrigt vetenskapligt)
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.

 

Ort, förlag, år, upplaga, sidor
Västerås: Mälardalen University, 2011
Serie
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 132
Forskningsämne
datavetenskap
Identifikatorer
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
Handledare
Projekt
PROGRESSARROWS
Forskningsfinansiär
Vetenskapsrådet
Tillgänglig från: 2011-05-13 Skapad: 2011-05-12 Senast uppdaterad: 2011-06-03Bibliografiskt granskad
3. Model Based Development of Embedded Systems using Logical Clock Constraints and Timed Automata
Öppna denna publikation i ny flik eller fönster >>Model Based Development of Embedded Systems using Logical Clock Constraints and Timed Automata
2013 (Engelska)Doktorsavhandling, sammanläggning (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Västerås: Mälardalen University, 2013
Serie
Mälardalen University Press Dissertations, ISSN 1651-4238 ; 146
Nyckelord
Embedded Systems, Model-based development, Model-Checking, Architectural Modeling, CCSL, Timed Automata
Nationell ämneskategori
Inbäddad systemteknik
Identifikatorer
urn:nbn:se:mdh:diva-22328 (URN)978-91-7485-123-6 (ISBN)
Disputation
2013-12-09, Kappa, Mälardalen University, Västerås, 13:15 (Engelska)
Opponent
Handledare
Projekt
ARROWS
Forskningsfinansiär
Vetenskapsrådet, 2270 430 16243
Tillgänglig från: 2013-11-01 Skapad: 2013-11-01 Senast uppdaterad: 2013-11-18Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Personposter BETA

Vulgarakis, AnetaCarlson, JanSeceleanu, CristinaPettersson, Paul

Sök vidare i DiVA

Av författaren/redaktören
Vulgarakis, AnetaSuryadevara, JagadishCarlson, JanSeceleanu, CristinaPettersson, Paul
Av organisationen
Akademin för innovation, design och teknik

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

doi
isbn
urn-nbn
Totalt: 148 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf