Formal methods for the development and verification of autonomic IT systems

Radu Calinescu, Shinji Kikuchi, Marta Kwiatkowska

    Research output: Chapter in Book/Published conference outputChapter (peer-reviewed)peer-review


    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
    Number of pages37
    ISBN (Electronic)978-1-6096-0846-0
    ISBN (Print)978-1-6096-0845-3
    Publication statusPublished - Oct 2011

    Publication series

    NamePremier Referecen Source
    PublisherIGI Global


    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