mdh.sePublications
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
Adaptive Task Automata with Earliest-Deadline-First Scheduling
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded Systems))ORCID iD: 0000-0003-0073-1674
Aalborg University, Danmark. (Department of Computer Science)
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded Systems))ORCID iD: 0000-0003-2870-2680
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems. (IS (Embedded Systems))ORCID iD: 0000-0003-4040-3480
(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: urn:nbn:se:mdh:diva-26126OAI: oai:DiVA.org:mdh-26126DiVA: diva2:756829
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
In thesis
1. Formal Verification of Adaptive Real-Time Systems by Extending Task Automata
Open this publication in new window or tab >>Formal Verification of Adaptive Real-Time Systems by Extending Task Automata
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
formal verification, embedded systems, timed automata, scheduling
National Category
Embedded Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:mdh:diva-26129 (URN)978-91-7485-172-4 (ISBN)
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

Open Access in DiVA

No full text

Search in DiVA

By author/editor
Hatvani, LeoSeceleanu, CristinaPettersson, Paul
By organisation
Embedded Systems
In the same journal
Electronic Communications of the EASST
Electrical Engineering, Electronic Engineering, Information Engineering

Search outside of DiVA

GoogleGoogle Scholar

Total: 33 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