Methods and Tool Support for Analyzing Architectural Models of Embedded Systems

↓ Direkt till sidans innehåll
↓ Direkt till sidans sekundära innehåll (sidomenyn)

Search: WFRF:(Pettersson Stefan) > (2010-2014) > Methods and Tool Su...

Details
MARC

Björnander, Stefan,1968-Mälardalens högskola,Akademin för innovation, design och teknik,Formal modeling, analysis, and verification of real-time and embedded systems (author)

Methods and Tool Support for Analyzing Architectural Models of Embedded Systems

BookEnglish2012

Publisher, publication year, extent ...

Västerås :Mälardalen University,2012
electronicrdacarrier

Numbers

LIBRIS-ID:oai:DiVA.org:mdh-14521
ISBN:9789174850710
https://urn.kb.se/resolve?urn=urn:nbn:se:mdh:diva-14521URI

Supplementary language notes

Language:English
Summary in:English

Part of subdatabase

SwePubSwePub

Classification

Subject category:vet swepub-contenttype
Subject category:lic swepub-publicationtype

Series

Mälardalen University Press Licentiate Theses,1651-9256 ;153

Notes

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.

Subject headings and genre

NATURVETENSKAP Data- och informationsvetenskap Datavetenskap hsv//swe
NATURAL SCIENCES Computer and Information Sciences Computer Sciences hsv//eng
Computer Science
datavetenskap

Added entries (persons, corporate bodies, meetings, titles ...)

Pettersson, PaulMälardalens högskola,Akademin för innovation, design och teknik (thesis advisor)
Lundqvist, KristinaMälardalens högskola,Akademin för innovation, design och teknik (thesis advisor)
Seceleanu, CristinaMälardalens högskola,Akademin för innovation, design och teknik (thesis advisor)
Sander, Ingo,docentKungliga tekniska högskolan (opponent)
Mälardalens högskolaAkademin för innovation, design och teknik (creator_code:org_t)

Internet link

Find in a library

Methods and Tool Support for Analyzing Architectural Models of Embedded Systems (Search the publication in LIBRIS)

To the university's database

Find more in SwePub

By the author/editor: Björnander, Stef ...; Pettersson, Paul; Lundqvist, Krist ...; Seceleanu, Crist ...; Sander, Ingo, do ...

About the subject

NATURAL SCIENCES: NATURAL SCIENCES; and Computer and Inf ...; and Computer Science ...

Parts in the series: Mälardalen Unive ...

By the university: Mälardalen University

Search outside SwePub

Extend your search to:: Google; Google Book Search; Google Scholar

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.

LIBRIS.kb.se