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

Formal methods
Model checking
Formal specification

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
Calinescu, Radu ; Kikuchi, Shinji ; Kwiatkowska, Marta. / Formal methods for the development and verification of autonomic IT systems. Formal and practical aspects of autonomic computing and networking: specification, development, and verification. editor / Phan Cong-Vinh. IGI Global, 2011. pp. 1-37 (Premier Referecen Source).
@inbook{9c0515a733ac4defb2e5cefd4451996e,
title = "Formal methods for the development and verification of autonomic IT systems",
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.",
author = "Radu Calinescu and Shinji Kikuchi and Marta Kwiatkowska",
year = "2011",
month = "10",
doi = "10.4018/978-1-60960-845-3.ch001",
language = "English",
isbn = "978-1-6096-0845-3",
series = "Premier Referecen Source",
publisher = "IGI Global",
pages = "1--37",
editor = "Phan Cong-Vinh",
booktitle = "Formal and practical aspects of autonomic computing and networking",
address = "United States",

}

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. Premier Referecen Source, IGI Global, pp. 1-37. https://doi.org/10.4018/978-1-60960-845-3.ch001

Formal methods for the development and verification of autonomic IT systems. / Calinescu, Radu; Kikuchi, Shinji; Kwiatkowska, Marta.

Formal and practical aspects of autonomic computing and networking: specification, development, and verification. ed. / Phan Cong-Vinh. IGI Global, 2011. p. 1-37 (Premier Referecen Source).

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

TY - CHAP

T1 - Formal methods for the development and verification of autonomic IT systems

AU - Calinescu, Radu

AU - Kikuchi, Shinji

AU - Kwiatkowska, Marta

PY - 2011/10

Y1 - 2011/10

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=79959967907&partnerID=8YFLogxK

UR - http://www.igi-global.com/chapter/formal-methods-development-verification-autonomic/60442

U2 - 10.4018/978-1-60960-845-3.ch001

DO - 10.4018/978-1-60960-845-3.ch001

M3 - Chapter (peer-reviewed)

AN - SCOPUS:79959967907

SN - 978-1-6096-0845-3

T3 - Premier Referecen Source

SP - 1

EP - 37

BT - Formal and practical aspects of autonomic computing and networking

A2 - Cong-Vinh, Phan

PB - IGI Global

ER -

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