mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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 Verification of Adaptive Real-Time Systems by Extending Task Automata
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded Systems))ORCID iD: 0000-0003-0073-1674
2014 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Recently, we have seen an increase in the deployment of safety critical embedded systems in rapidly changing environments, as well as requirement for on-site customizations and rapid adaptation. To address the extended range of requirements, adaptation mechanism are added to the systems to handle large number of situations appropriately. Although necessary, adaptations can cause inconsistent and unstable configurations that must be prevented for the embedded system to remain dependable and safe. Therefore, verifying the behavior of adaptive embedded systems during the design phase of the production process is highly desirable.

A hard real time embedded system and its environment can be modeled using timed automata. Such model can describe the system at various levels of abstraction. In this thesis, we model the adaptive responses of a system in terms of tasks that are executed to handle changes in the environmental or internal parameters.

Schedulability, a property that all tasks complete execution within their respective deadlines, is a key element in designing hard real-time embedded systems. A system that is unschedulable immediately compromises safety and hard real-time requirements and can cause fatal failure. Given specifications of all tasks in the system, we can model the system, an abstraction of the environment, and adaptive strategies to investigate whether the system retains safety properties, including schedulability, regardless of the changes in the environment and adaptations to those changes.

Place, publisher, year, edition, pages
Västerås: Mälardalen University , 2014.
Series
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 185
Keyword [en]
formal verification, embedded systems, timed automata, scheduling
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:mdh:diva-26129ISBN: 978-91-7485-172-4 (print)OAI: oai:DiVA.org:mdh-26129DiVA: diva2:756834
Presentation
2014-11-28, Kappa, Västerås, 13:15 (English)
Opponent
Supervisors
Available from: 2014-10-23 Created: 2014-10-20 Last updated: 2014-11-20Bibliographically approved
List of papers
1. Adaptive task automata: A framework for verifying adaptive embedded systems
Open this publication in new window or tab >>Adaptive task automata: A framework for verifying adaptive embedded systems
2012 (English)In: Lecture Notes in Computer Science, vol. 7212, Springer, 2012, 115-129 p.Chapter in book (Refereed)
Abstract [en]

We present a framework for modeling and analysis of adaptive embedded systems, based on the model of timed automata with tasks. The model is extended with primitives allowing modeling of adaptivity, by testing the potential schedulability of a given task, in the context of the set of currently enqueued tasks. This makes it possible to describe adaptive embedded systems, in which decisions to admit further tasks or take other measures of adaptivity is based on available CPU resources, external, or internal events. We show that this model can be encoded in the framework of timed automata, and hence that the problem is decidable. We also validate the framework, by using the Uppaal tool.

Place, publisher, year, edition, pages
Springer, 2012
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7212
National Category
Engineering and Technology
Identifiers
urn:nbn:se:mdh:diva-17227 (URN)10.1007/978-3-642-28872-2_9 (DOI)2-s2.0-84859124356 (Scopus ID)978-364228871-5 (ISBN)
Note

15th International Conference on Fundamental Approaches to Software Engineering, FASE 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012; Tallinn; 24 March 2012 through 1 April 2012

Available from: 2012-12-20 Created: 2012-12-20 Last updated: 2016-05-17Bibliographically approved
2. Modeling and Analysis of Adaptive Embedded Systems using Adaptive Task Automata
Open this publication in new window or tab >>Modeling and Analysis of Adaptive Embedded Systems using Adaptive Task Automata
2013 (English)In: SIGBED Rev., ISSN 1551-3688, Vol. 10, no 1, 43-47 p.Article in journal (Refereed) Published
Abstract [en]

Most embedded systems need to continually function in unpredictable environments. One way to achieve high dependability is to make the system adaptive to changes, if possible, without sacrificing maintainability. To be able to reason about adaptivity, one needs a modeling and analysis framework suitable for adaptive systems. Recently, we have introduced Adaptive Task Automata, to meet this goal. In this paper, we overview the current functionality implemented in the Adaptive Task Automata framework (ATA), as well as some of the challenges encountered during the development. In the end, we enumerate possible future extensions of ATA.

Place, publisher, year, edition, pages
New York, NY, USA: Association for Computing Machinery (ACM), 2013
Keyword
adaptive embedded systems, adaptive task automata, schedulability verification, task automata
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-25871 (URN)10.1145/2492385.2492393 (DOI)
Projects
ARROWS - Design Techniques for Adaptive Embedded Systems
Available from: 2014-09-05 Created: 2014-09-05 Last updated: 2015-02-06Bibliographically approved
3. Adaptive Task Automata with Earliest-Deadline-First Scheduling
Open this publication in new window or tab >>Adaptive Task Automata with Earliest-Deadline-First Scheduling
(English)In: Electronic Communications of the EASST, ISSN 1863-2122, Vol. 070Article in journal (Refereed) Accepted
Abstract [en]

Adjusting to resource changes, dynamic environmental conditions, or new usage modes are some of the reasons why real-time embedded systems need to be adaptive. This requires a rigorous framework for designing such systems, to ensure that the adaptivity does not result in invalidating the system's real-time constraints.

To address this need, we have recently introduced adaptive task automata, a framework for modeling, verification, and schedulability analysis in adaptive, hard real-time embedded systems, assuming a fixed-priority scheduler.

In this work, we extend the adaptive task automata framework to incorporate the earliest-deadline-first scheduling policy, as well as enable implementation of any other dynamic scheduling policy. To prove the decidability of our model, and at the same time maintain a manageable degree of conciseness, we show an encoding of our model as a network of timed automata with clock updates. To support this, we also show that reachability in our class of timed automata with updates is decidable. Our contribution helps to streamline the process of designing safety critical adaptive embedded systems.

National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-26126 (URN)
Conference
14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014), Enschede, Netherlands, September 24-26, 2014.
Projects
ARROWS - Design Techniques for Adaptive Embedded Systems
Available from: 2014-10-20 Created: 2014-10-20 Last updated: 2014-11-11Bibliographically approved
4. Adaptive Task Automata with Earliest-Deadline-First Scheduling
Open this publication in new window or tab >>Adaptive Task Automata with Earliest-Deadline-First Scheduling
2014 (English)Report (Other (popular science, discussion, etc.))
Abstract [en]

Adjusting to resource changes, dynamic environmental conditions, or new usage modes are some of the reasons why real-time embedded systems need to be adaptive. This requires a rigorous framework for designing such systems, to ensure that the adaptivity does not result in invalidating the system's real-time constraints.

To address this need, we have recently introduced adaptive task automata, a framework for modeling, verification, and schedulability analysis in adaptive, hard real-time embedded systems, assuming a fixed-priority scheduler.

In this work, we extend the adaptive task automata framework to incorporate the earliest-deadline-first scheduling policy, as well as enable implementation of any other dynamic scheduling policy. To prove the decidability of our model, and at the same time maintain a manageable degree of conciseness, we show an encoding of our model as a network of timed automata with clock updates. To support this, we also show that reachability in our class of timed automata with updates is decidable. Our contribution helps to streamline the process of designing safety critical adaptive embedded systems.

Place, publisher, year, edition, pages
Sweden: , 2014. 18 p.
Series
MRTC Reports, ISSN 1404-3041
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-25965 (URN)MDH-MRTC-287/2014-1-SE (ISRN)
Projects
ARROWS - Design Techniques for Adaptive Embedded Systems
Available from: 2014-09-17 Created: 2014-09-17 Last updated: 2014-11-11Bibliographically approved

Open Access in DiVA

fulltext(608 kB)174 downloads
File information
File name FULLTEXT02.pdfFile size 608 kBChecksum SHA-512
ad0e4dd1ffb58de923930c0ad925c8f725463210849fded8ee5e7aac994465b33a612b12e2cec7fdc0630f259e7f8f1e920cd33c52a42265945cb6d219f43cb9
Type fulltextMimetype application/pdf

Search in DiVA

By author/editor
Hatvani, Leo
By organisation
Embedded Systems
Embedded Systems

Search outside of DiVA

GoogleGoogle Scholar
Total: 174 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

Total: 753 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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