https://www.mdu.se/

mdh.sePublikasjoner
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet 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 (engelsk)Inngår i: Electronic Communications of the EASST, E-ISSN 1863-2122, Vol. 70Artikkel i tidsskrift (Fagfellevurdert) 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.

sted, utgiver, år, opplag, sider
2014. Vol. 70
HSV kategori
Forskningsprogram
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
Konferanse
14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014), Enschede, Netherlands, September 24-26, 2014.
Prosjekter
ARROWS - Design Techniques for Adaptive Embedded SystemsTilgjengelig fra: 2014-10-20 Laget: 2014-10-20 Sist oppdatert: 2023-10-23bibliografisk kontrollert
Inngår i avhandling
1. Formal Verification of Adaptive Real-Time Systems by Extending Task Automata
Åpne denne publikasjonen i ny fane eller vindu >>Formal Verification of Adaptive Real-Time Systems by Extending Task Automata
2014 (engelsk)Licentiatavhandling, med artikler (Annet vitenskapelig)
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.

sted, utgiver, år, opplag, sider
Västerås: Mälardalen University, 2014
Serie
Mälardalen University Press Licentiate Theses, ISSN 1651-9256 ; 185
Emneord
formal verification, embedded systems, timed automata, scheduling
HSV kategori
Forskningsprogram
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 (engelsk)
Opponent
Veileder
Tilgjengelig fra: 2014-10-23 Laget: 2014-10-20 Sist oppdatert: 2014-11-20bibliografisk kontrollert

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekstScopus

Person

Hatvani, LeoSeceleanu, CristinaPettersson, Paul

Søk i DiVA

Av forfatter/redaktør
Hatvani, LeoSeceleanu, CristinaPettersson, Paul
Av organisasjonen
I samme tidsskrift
Electronic Communications of the EASST

Søk utenfor DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric

doi
urn-nbn
Totalt: 84 treff
RefereraExporteraLink to record
Permanent link

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