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
A Case Study on Formal Verification of Self-Adaptive Behaviors in a Decentralized System
Linnaeus University, Faculty of Science and Engineering, School of Computer Science, Physics and Mathematics. (Software Technology Labs)ORCID iD: 0000-0002-1343-5834
Linnaeus University, Faculty of Science and Engineering, School of Computer Science, Physics and Mathematics. (Software Technology Labs)ORCID iD: 0000-0002-1162-0817
2012 (English)In: Electronic Proceedings in Theoretical Computer Science / [ed] Natallia Kokash and António Ravara, 2012, Vol. 91, no 91, 45-62 p.Conference paper, Published paper (Refereed)
Abstract [en]

Self-adaptation is a promising approach to manage the complexity of modern software systems. A self-adaptive system is able to adapt autonomously to internal dynamics and changing conditions in the environment to achieve particular quality goals. Our particular interest is in decentralized selfadaptive systems, in which central control of adaptation is not an option. One important challenge in self-adaptive systems, in particular those with decentralized control of adaptation, is to provide guarantees about the intended runtime qualities. In this paper, we present a case study in which we use model checking to verify behavioral properties of a decentralized self-adaptive system. Concretely, we contribute with a formalized architecture model of a decentralized traffic monitoring system and prove a number of self-adaptation properties for flexibility and robustness. To model the main processes in the system we use timed automata, and for the specification of the required properties we use timed computation tree logic. We use the Uppaal tool to specify the system and verify the flexibility and robustness properties.

Place, publisher, year, edition, pages
2012. Vol. 91, no 91, 45-62 p.
National Category
Software Engineering
Research subject
Computer Science, Software Technology
Identifiers
URN: urn:nbn:se:lnu:diva-25920OAI: oai:DiVA.org:lnu-25920DiVA: diva2:623873
Conference
11th International Workshop on Foundations of Coordination Languages and Self Adaptation (FOCLASA 2012), Newcastle, UK, September 8, 2012
Available from: 2013-05-29 Created: 2013-05-29 Last updated: 2017-03-20Bibliographically approved

Open Access in DiVA

2012FOCLASA.pdf(1226 kB)328 downloads
File information
File name FULLTEXT01.pdfFile size 1226 kBChecksum SHA-512
6633bd68811b52def841ded361b2fd58c2e111123449cf5e6b66b4ca2f57ef926f66d1e47b5d36da1dc1d6cff3bc2df7e1c70e826fd0ab2bcc17b1dbdcc54798
Type fulltextMimetype application/pdf

Other links

FulltextArXiv

Search in DiVA

By author/editor
Iftikhar, Muhammad UsmanWeyns, Danny
By organisation
School of Computer Science, Physics and Mathematics
Software Engineering

Search outside of DiVA

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

urn-nbn

Altmetric score

urn-nbn
Total: 803 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