lnu.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Assuring the Correctness of Large-scale Adaptive Systems
TU Braunschweig, Germany.ORCID iD: 0000-0002-0377-5595
Tarbiat Modares University, Iran.
Reykjavik University, Iceland.
2011 (English)Report (Other academic)
Abstract [en]

The next generation of software systems includes systems composed of a large number of distributed, decentralized, autonomous, interacting, cooperating, organically grown, heterogeneous, and continually evolving subsystems, which we call IT Ecosystems. Clearly, we need novel models and approaches to design and develop such systems which can tackle the long-term evolution and complexity problems. In this paper, our framework to model IT-Ecosystems is a combination of top-down (centralized control) and bottom-up (self-organizing) approach. We use a flexible formal model, hierarchical PobSAM, that supports both behavioral and structural adaptation/evolution. We use a detailed, close to real-life, case study of a smart airport to show how we can use hierarchical PobSAM in modeling, analyzing and developing an IT Ecosystem. We provide an executable formal specification of the model in Maude, and use LTL model checking and bounded state space search provided by Maude to analyze the model. We develop a prototype of our case study designed by hierarchical PobSAM using Java and Ponder2. Due to the complexity of model, we can not check all properties at design time using Maude. We propose a new approach for run-time verification of our case study, and check different types of properties which we could not verify using model checking. As our model uses dynamic policies to control the behavior of system which can be modified at runtime, it provides us a suitable capability to react to the property violation by modification of policies.

Place, publisher, year, edition, pages
TU Braunschweig , 2011. , 36 p.
National Category
Computer Science
Identifiers
URN: urn:nbn:se:lnu:diva-42333OAI: oai:DiVA.org:lnu-42333DiVA: diva2:805200
Available from: 2015-04-14 Created: 2015-04-14 Last updated: 2015-04-30Bibliographically approved

Open Access in DiVA

No full text

Other links

Fulltext

Search in DiVA

By author/editor
Khakpour, Narges
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

Total: 38 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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