You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at http://www.ieee.org/web/publications/rights/copyrightpolicy.html)
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at http://www.acm.org/pubs/copyright_policy/)
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact webmaster@ide.mdh.se

Methods and Tool Support for Analyzing Architectural Models of Embedded Systems

Publication Type:

Licentiate Thesis

Publisher:

Mälardalen University


Abstract

Embedded systems are ubiquitous in the modern world. They are microcomputers most often included in complete devices consisting of software and hardware. Embedded systems range from small devices to large systems monitoring and controlling complex processes. The 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 safety-critical, meaning that some system failures may cause severe damage in human life or large financial losses.One way to ensure that a system works in accordance with its specification is to define the system in an Architecture Description Language (ADL) and apply formal verification methods on the architectural model, well in advance of the system implementation. The Architecture Analysis and Design Language (AADL) of the Society of Automotive Engineers (SAE) has become popular in, e.g., the avionic and automobile industry. The AADL specification holds several annexes, including the Behavior Annex that is considered in this thesis. Parts of AADL lack a formal semantics, which prevents formal analysis of AADL models, e.g., model checking. Moreover, AADL does not support time annotations, which makes modeling of real-time systems harder.In this thesis, we address the above-mentioned shortcomings by presenting a formal analysis framework including a denotational semantics for a subset of AADL and its Behavior Annex, which allows for checking properties defined in Computation Tree Logic (CTL) by model checking. Model checking is a formal verification method that has proved to be powerful as well as effective in uncovering design errors prior to system implementation. Our AADL-semantics is supported by a model-checker, called ABV, which implements the semantics in Standard ML and is encapsulated in an Eclipse plug-in. We also present a time annotation extension of AADL, implemented in a tool that translates the latter and its Behavior Annex into the Timed Abstract State Machine (TASM) language for simulation of real-time features.Effective component distribution, in particular achieving optimal component distribution, against a set of constraints (e.g. frequency and bandwidth) is a problem tightly connected to architectural modeling. In order to address this problem, we have developed a tool that performs near-optional component distribution with respect to a series of parameters.The research results, which have been illustrated on relevant case studies, provide to the system engineer means for proving that the architectural system model meets its specification with respect to both function and timing. The research has been conducted in the context of the PROGRESS research center, for predictable embedded software systems.

Bibtex

@misc{Bjornander3097,
author = {Stefan Bj{\"o}rnander},
title = {Methods and Tool Support for Analyzing Architectural Models of Embedded Systems},
number = {153},
month = {December},
year = {2012},
publisher = {M{\~A}¤lardalen University},
url = {http://www.es.mdu.se/publications/3097-}
}