Formal methods for the development and verification of autonomic IT systems

Radu Calinescu, Shinji Kikuchi, Marta Kwiatkowska

Research output: Chapter in Book/Report/Conference proceedingChapter (peer-reviewed)

Abstract

This chapter explores ways in which rigorous mathematical techniques, termed formal methods, can be employed to improve the predictability and dependability of autonomic computing. Model checking, formal specification, and quantitative verification are presented in the contexts of conflict detection in autonomic computing policies, and of implementation of goal and utility-function policies in autonomic IT systems, respectively. Each of these techniques is illustrated using a detailed case study, and analysed to establish its merits and limitations. The analysis is then used as a basis for discussing the challenges and opportunities of this endeavour to transition the development of autonomic IT systems from the current practice of using ad-hoc methods and heuristic towards a more principled approach.

Original languageEnglish
Title of host publicationFormal and practical aspects of autonomic computing and networking
Subtitle of host publicationspecification, development, and verification
EditorsPhan Cong-Vinh
PublisherIGI Global
Pages1-37
Number of pages37
ISBN (Electronic)978-1-6096-0846-0
ISBN (Print)978-1-6096-0845-3
DOIs
Publication statusPublished - Oct 2011

Publication series

NamePremier Referecen Source
PublisherIGI Global

Fingerprint Dive into the research topics of 'Formal methods for the development and verification of autonomic IT systems'. Together they form a unique fingerprint.

  • Cite this

    Calinescu, R., Kikuchi, S., & Kwiatkowska, M. (2011). Formal methods for the development and verification of autonomic IT systems. In P. Cong-Vinh (Ed.), Formal and practical aspects of autonomic computing and networking: specification, development, and verification (pp. 1-37). (Premier Referecen Source). IGI Global. https://doi.org/10.4018/978-1-60960-845-3.ch001