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
Methods and Tool Support for Analyzing Architectural Models of Embedded Systems
Mälardalen University, School of Innovation, Design and Engineering. (Formal modeling, analysis, and verification of real-time and embedded systems)ORCID iD: 0000-0003-1119-611X
2012 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Embedded systems are ubiquitous in the modern world. They are microcomputers most often included incomplete devices consisting of software and hardware. Embedded systems range from small devices to large systems monitoring and controlling complex processes. Design and development of such systems is a complex task, since embedded systems often need to fulfill extra-functional requirements, on top of functional ones, within constrained amounts of platform resources. Some embedded systems are mission critical; hence, they are not allowed to fail during the mission. One way to ensure that a system works in accordance to its specification is to define the system in an Architecture Description Language (ADL) and apply formal verification methods. The Architecture Design and Analysis Language (AADL) has become popular in the avionic and automobile industry, and is equipped with several annexes, among them the Behavior Annex. However, AADL still misses a formal semantics, which prevents the possibility to prove correctness of architecture features by performing model checking on AADL models. Moreover, AADL does not support time annotations, which prevents modeling of real-time systems in AADL.

In this thesis, we address these issues by presenting a formal analysis framework including a denotationalsemantics for a subset of the AADL and its Behavior Annex, which evaluates properties defined in Computation Tree Logic (CTL) by providing model checking. Model checking is a formal verification method that has proved to be powerful as well as effective. Our AADL-semantics is supported by a tool with an implementation of the semantics in Standard ML, which in turn is encapsulated in an Eclipse plugin.We also present a time annotation extension of AADL, implemented in a tool translating time annotated AADL and its Behavior Annex into the Timed Abstract State Machine (TASM) for simulation of real-time features. Another closely related problem is how to achieve optimal component distribution; in order to address this issue we have developed a tool that perform near-optional component distribution in regard to a series of parameters.

The research results, which have been validated thought case studies, provides the possibility for a system engineer to model a system and prove its correctness. The research has been conducted in the context of the PROGRESS research center, for predictable embedded software systems.

Place, publisher, year, edition, pages
Västerås: Mälardalen University , 2012.
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 153
National Category
Computer Science
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-14521ISBN: 978-91-7485-071-0 (print)OAI: oai:DiVA.org:mdh-14521DiVA: diva2:517420
Presentation
2012-12-14, Lambda, Mälardalens högskola, Västerås, 10:00 (English)
Opponent
Supervisors
Available from: 2012-05-10 Created: 2012-04-23 Last updated: 2013-12-03Bibliographically approved
List of papers
1. ArcheOpterix: An Extendable Tool for Architecture Optimization of AADL Models
Open this publication in new window or tab >>ArcheOpterix: An Extendable Tool for Architecture Optimization of AADL Models
2009 (English)In: Proceedings of the 2009 ICSE Workshop on Model-Based Methodologies for Pervasive and Embedded Software, MOMPES 2009, 2009, 61-71 p.Conference paper, Oral presentation only (Refereed)
National Category
Computer Science
Identifiers
urn:nbn:se:mdh:diva-14515 (URN)10.1109/MOMPES.2009.5069138 (DOI)2-s2.0-70349898605 (Scopus ID)978-142443721-4 (ISBN)
Conference
Model-Based Methodologies for Pervasive and Embedded Model-Based Methodologies for Pervasive and Embedded Software (MOMPES) at ICSE '09: Proceedings of the 31st International Conference on Software Engineering
Note
(c) 2009 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other users, including reprinting/ republishing this material for advertising or promotional purposes, creating new collective works for resale or redistribution to servers or lists, or reuse of any copyrighted components of this work in other worksAvailable from: 2012-04-27 Created: 2012-04-23 Last updated: 2013-12-03Bibliographically approved
2. Timed Simulation of Extended AADL-Based Architecture Specifications with Timed Abstract State Machines
Open this publication in new window or tab >>Timed Simulation of Extended AADL-Based Architecture Specifications with Timed Abstract State Machines
2009 (English)In: Architectures for Adaptive Software Systems: 5th International Conference on the Quality of Software Architectures, QoSA 2009, East Stroudsburg, PA, USA, June 24-26, 2009 Proceedings, Berlin: Springer, 2009, 101-115 p.Chapter in book (Refereed)
Abstract [en]

The Architecture Analysis and Design Language (AADL) is a popular language for architectural modeling and analysis of software intensive systems in application domains such as automotive, avionics, railway and medical systems. These systems often have stringent real-time requirements. This paper presents an extension to AADL's behavior model using time annotations in order to improve the evaluation of timing properties in AADL. The translational semantics of this extension is based on mappings to the Timed Abstract State Machines (TASM) language. As a result, timing analysis with timed simulation or timed model checking is possible. The translation is supported by art Eclipse-based plug-in and the approach is validated with a case study of an industrial production cell system.

Place, publisher, year, edition, pages
Berlin: Springer, 2009
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 5581
National Category
Computer Science
Identifiers
urn:nbn:se:mdh:diva-14517 (URN)10.1007/978-3-642-02351-4_7 (DOI)000270318900007 ()2-s2.0-70350675939 (Scopus ID)978-364202350-7 (ISBN)
Conference
Proceedings of the Fifth International Conference on the Quality of Software Architectures
Available from: 2012-04-27 Created: 2012-04-23 Last updated: 2014-06-22Bibliographically approved
3. ABV: A Verifier for the Architecture Analysis and Description Language (AADL)
Open this publication in new window or tab >>ABV: A Verifier for the Architecture Analysis and Description Language (AADL)
2011 (English)In: 16th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), 2011, 2011, 355-360 p.Conference paper, Oral presentation only (Refereed)
National Category
Computer Science
Identifiers
urn:nbn:se:mdh:diva-14519 (URN)10.1109/ICECCS.2011.43 (DOI)000298664200036 ()2-s2.0-79960524242 (Scopus ID)978-0-7695-4381-9 (ISBN)978-1-61284-853-2 (ISBN)
Conference
Proceedings of the Sixth IEEE International workshop on UML and AADL
Note
(c) 2011 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other users, including reprinting/ republishing this material for advertising or promotional purposes, creating new collective works for resale or redistribution to servers or lists, or reuse of any copyrighted components of this work in other worksAvailable from: 2012-04-27 Created: 2012-04-23 Last updated: 2013-12-03Bibliographically approved
4. A Formal Analysis Framework for AADL
Open this publication in new window or tab >>A Formal Analysis Framework for AADL
2011 (English)In: The Journal of Science and Technology, ISSN 0866-708X, Vol. 49, no 5Article in journal (Refereed) Submitted
Abstract [en]

As system failure of mission-critical embedded systems may result in serious consequences, the development process should include verification techniques already at the architectural design stage, in order to provide evidence that the architecture fulfils its requirements. The Architecture Analysis and Design Language (AADL) is a language designed for modeling embedded systems, and its Behavior Annex defines the behavior of the system. However, even though it is an internationally used industry standard, AADL still lacks a formal semantics and is not executable, which limits the possibility to perform formal verification. In this paper, we introduce a formal analysis framework for a subset of AADL and its Behavior Annex, which includes the following: a denotational semantics, its implementation in Standard ML, and a graphical Eclipse-based tool encapsulating the implementation. We also show how to perform model checking of AADL properties defined in the Computation Tree Logic (CTL).

Place, publisher, year, edition, pages
Vietnam Academy of Science and Technology, 2011
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-13500 (URN)
Available from: 2011-12-15 Created: 2011-12-15 Last updated: 2013-12-03Bibliographically approved

Open Access in DiVA

kappa(184 kB)367 downloads
File information
File name FULLTEXT03.pdfFile size 184 kBChecksum SHA-512
e76d169edaf64f99185e37e6c7027b8810b1db820ea39676576dc4cb83bf3403acb8f0630845d2bf9bb844e8adec241612bbf5989708243f17c9315f6b252a91
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Björnander, Stefan
By organisation
School of Innovation, Design and Engineering
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 367 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

isbn
urn-nbn

Altmetric score

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