mdh.sePublikationer
Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Adaptive Task Automata with Earliest-Deadline-First Scheduling
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. (IS (Embedded Systems))ORCID-id: 0000-0003-0073-1674
Aalborg University, Danmark. (Department of Computer Science)
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. (IS (Embedded Systems))ORCID-id: 0000-0003-2870-2680
Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. (IS (Embedded Systems))ORCID-id: 0000-0003-4040-3480
2014 (Engelska)Ingår i: Electronic Communications of the EASST, ISSN 1863-2122, E-ISSN 1863-2122, Vol. 70Artikel i tidskrift (Refereegranskat) Published
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.

Ort, förlag, år, upplaga, sidor
2014. Vol. 70
Nationell ämneskategori
Elektroteknik och elektronik
Forskningsämne
datavetenskap
Identifikatorer
URN: urn:nbn:se:mdh:diva-26126DOI: 10.14279/tuj.eceasst.70.975Scopus ID: 2-s2.0-85042925051OAI: oai:DiVA.org:mdh-26126DiVA, id: diva2:756829
Konferens
14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014), Enschede, Netherlands, September 24-26, 2014.
Projekt
ARROWS - Design Techniques for Adaptive Embedded SystemsTillgänglig från: 2014-10-20 Skapad: 2014-10-20 Senast uppdaterad: 2018-03-15Bibliografiskt granskad
Ingår i avhandling
1. Formal Verification of Adaptive Real-Time Systems by Extending Task Automata
Öppna denna publikation i ny flik eller fönster >>Formal Verification of Adaptive Real-Time Systems by Extending Task Automata
2014 (Engelska)Licentiatavhandling, sammanläggning (Övrigt vetenskapligt)
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.

Ort, förlag, år, upplaga, sidor
Västerås: Mälardalen University, 2014
Serie
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 185
Nyckelord
formal verification, embedded systems, timed automata, scheduling
Nationell ämneskategori
Inbäddad systemteknik
Forskningsämne
datavetenskap
Identifikatorer
urn:nbn:se:mdh:diva-26129 (URN)978-91-7485-172-4 (ISBN)
Presentation
2014-11-28, Kappa, Västerås, 13:15 (Engelska)
Opponent
Handledare
Tillgänglig från: 2014-10-23 Skapad: 2014-10-20 Senast uppdaterad: 2014-11-20Bibliografiskt granskad

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltextScopus

Personposter BETA

Hatvani, LeoSeceleanu, CristinaPettersson, Paul

Sök vidare i DiVA

Av författaren/redaktören
Hatvani, LeoSeceleanu, CristinaPettersson, Paul
Av organisationen
Inbyggda system
I samma tidskrift
Electronic Communications of the EASST
Elektroteknik och elektronik

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetricpoäng

doi
urn-nbn
Totalt: 50 träffar
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf