@article{1519,
  author = {Muhammad Nauman, Nadeem Akhtar},
  title = {Contribution of the Formal Verification of Self-adaptive Distributed Systems: A Case Study},
  journal = {Journal of Information Technology Review},
  year = {2014},
  volume = {5},
  number = {2},
  doi = {},
  url = {http://www.dline.info/jitr/fulltext/v5n2/1.pdf},
  abstract = {Self-adaptive systems have been proposed as an effective approach to tackle the challenges associated with the engineering and management of modern-day complex distributed software systems. There has been a substantial enhancement in the approaches to build such systems that are designed, organized, deployed and formally verified for previous decade; there is still disagreement among the researchers on some of the essential fundamental concepts. In this paper, we present a case study in which we use model checking to verify behavioural properties of a decentralized self-adaptive system. Concretely, we contribute with a formalized architecture model of a Distributed Internet Marketing System and prove a number of selfadaptation 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 safety property.},
}