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: A framework for verifying adaptive embedded systems
Mälardalen University, School of Innovation, Design and Engineering. (IS)ORCID iD: 0000-0003-0073-1674
Mälardalen University, School of Innovation, Design and Engineering. (IS)ORCID iD: 0000-0003-4040-3480
Mälardalen University, School of Innovation, Design and Engineering. (IS)ORCID iD: 0000-0003-2870-2680
2012 (English)In: Lecture Notes in Computer Science, vol. 7212, Springer, 2012, p. 115-129Chapter 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. p. 115-129
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7212
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:mdh:diva-17227DOI: 10.1007/978-3-642-28872-2_9ISI: 000343044000009Scopus ID: 2-s2.0-84859124356ISBN: 9783642288715 (print)OAI: oai:DiVA.org:mdh-17227DiVA, id: diva2:579558
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: 2018-08-08Bibliographically 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
Keywords
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 in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Hatvani, LeoPettersson, PaulSeceleanu, Cristina

Search in DiVA

By author/editor
Hatvani, LeoPettersson, PaulSeceleanu, Cristina
By organisation
School of Innovation, Design and Engineering
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 64 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