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

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • 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
A Case Study on Formal Verification of Self-Adaptive Behaviors in a Decentralized System
Linnéuniversitetet, Fakultetsnämnden för naturvetenskap och teknik, Institutionen för datavetenskap, fysik och matematik, DFM. (Software Technology Labs)ORCID-id: 0000-0002-1343-5834
Linnéuniversitetet, Fakultetsnämnden för naturvetenskap och teknik, Institutionen för datavetenskap, fysik och matematik, DFM. (Software Technology Labs)ORCID-id: 0000-0002-1162-0817
2012 (Engelska)Ingår i: Electronic Proceedings in Theoretical Computer Science / [ed] Natallia Kokash and António Ravara, 2012, Vol. 91, nr 91, s. 45-62Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
2012. Vol. 91, nr 91, s. 45-62
Nationell ämneskategori
Programvaruteknik
Forskningsämne
Datavetenskap, Programvaruteknik
Identifikatorer
URN: urn:nbn:se:lnu:diva-25920OAI: oai:DiVA.org:lnu-25920DiVA, id: diva2:623873
Konferens
11th International Workshop on Foundations of Coordination Languages and Self Adaptation (FOCLASA 2012), Newcastle, UK, September 8, 2012
Tillgänglig från: 2013-05-29 Skapad: 2013-05-29 Senast uppdaterad: 2018-01-11Bibliografiskt granskad

Open Access i DiVA

2012FOCLASA.pdf(1226 kB)400 nedladdningar
Filinformation
Filnamn FULLTEXT01.pdfFilstorlek 1226 kBChecksumma SHA-512
6633bd68811b52def841ded361b2fd58c2e111123449cf5e6b66b4ca2f57ef926f66d1e47b5d36da1dc1d6cff3bc2df7e1c70e826fd0ab2bcc17b1dbdcc54798
Typ fulltextMimetyp application/pdf

Övriga länkar

FulltextArXiv

Personposter BETA

Iftikhar, Muhammad UsmanWeyns, Danny

Sök vidare i DiVA

Av författaren/redaktören
Iftikhar, Muhammad UsmanWeyns, Danny
Av organisationen
Institutionen för datavetenskap, fysik och matematik, DFM
Programvaruteknik

Sök vidare utanför DiVA

GoogleGoogle Scholar
Totalt: 400 nedladdningar
Antalet nedladdningar är summan av nedladdningar för alla fulltexter. Det kan inkludera t.ex tidigare versioner som nu inte längre är tillgängliga.

urn-nbn

Altmetricpoäng

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

Direktlänk
Referera
Referensformat
  • apa
  • harvard1
  • 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