Formal design and verification of self-adaptive systems with decentralized control
Result description
Feedback control loops that monitor and adapt managed parts of a software system are considered crucial for realizing self-adaptation in software systems. The MAPE-K (Monitor-Analyze-Plan-Execute over a shared Knowledge) autonomic control loop is the most influential reference control model for self-adaptive systems. The design of complex distributed self-adaptive systems having decentralized adaptation control by multiple interacting MAPE components is among the major challenges. In particular, formal methods for designing and assuring the functional correctness of the decentralized adaptation logic are highly demanded. This article presents a framework for formal modeling and analyzing self-adaptive systems. We contribute with a formalism, called self-adaptive Abstract State Machines, that exploits the concept of multiagent Abstract State Machines to specify distributed and decentralized adaptation control in terms of MAPE-K control loops, also possible instances of MAPE patterns. We support validation and verification techniques for discovering unexpected interfering MAPE-K loops, and for assuring correctness of MAPE components interaction when performing adaptation.
Keywords
functional requirements assuranceformal modeling and analysisAbstract State MachinesMAPE patternMAPE-K loopSelf-adaptation
The result's identifiers
Result code in IS VaVaI
Result on the web
DOI - Digital Object Identifier
Alternative languages
Result language
angličtina
Original language name
Formal design and verification of self-adaptive systems with decentralized control
Original language description
Feedback control loops that monitor and adapt managed parts of a software system are considered crucial for realizing self-adaptation in software systems. The MAPE-K (Monitor-Analyze-Plan-Execute over a shared Knowledge) autonomic control loop is the most influential reference control model for self-adaptive systems. The design of complex distributed self-adaptive systems having decentralized adaptation control by multiple interacting MAPE components is among the major challenges. In particular, formal methods for designing and assuring the functional correctness of the decentralized adaptation logic are highly demanded. This article presents a framework for formal modeling and analyzing self-adaptive systems. We contribute with a formalism, called self-adaptive Abstract State Machines, that exploits the concept of multiagent Abstract State Machines to specify distributed and decentralized adaptation control in terms of MAPE-K control loops, also possible instances of MAPE patterns. We support validation and verification techniques for discovering unexpected interfering MAPE-K loops, and for assuring correctness of MAPE components interaction when performing adaptation.
Czech name
—
Czech description
—
Classification
Type
Jimp - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
GA17-12465S: Verification and Bug Hunting for Advanced Software
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2017
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
ACM Transactions on Autonomous and Adaptive Systems
ISSN
1556-4665
e-ISSN
—
Volume of the periodical
11
Issue of the periodical within the volume
4
Country of publishing house
US - UNITED STATES
Number of pages
35
Pages from-to
1-35
UT code for WoS article
000395848000006
EID of the result in the Scopus database
2-s2.0-85009236676
Basic information
Result type
Jimp - Article in a specialist periodical, which is included in the Web of Science database
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Year of implementation
2017