Compositional reverification of probabilistic safety properties for large-scale complex IT systems

Radu Calinescu*, Shinji Kikuchi, Kenneth Johnson

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Compositional verification has long been regarded as an effective technique for extending the use of symbolic model checking to large, component-based systems. This paper explores the effectiveness of the technique for large-scale complex IT systems (LSCITS). In particular, we investigate how compositional verification can be used to reverify LSCITS safety properties efficiently after the frequent changes that characterise these systems. We identify several LSCITS change patterns-including component failure, join and choice-and propose an approach that uses assume-guarantee compositional verification to reverify probabilistic safety properties compositionally in scenarios associated with these patterns. The application of this approach is illustrated using a case study from the area of cloud computing.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages303-329
Number of pages27
Volume7539 LNCS
DOIs
Publication statusPublished - 9 Nov 2012
Event17th Monterey Workshop on Large-Scale Complex IT Systems, LSCITS 2012 - Oxford, United Kingdom
Duration: 19 Mar 201221 Mar 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7539 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference17th Monterey Workshop on Large-Scale Complex IT Systems, LSCITS 2012
Country/TerritoryUnited Kingdom
CityOxford
Period19/03/1221/03/12

Cite this