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

TY - GEN

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

AU - Calinescu, Radu

AU - Kikuchi, Shinji

AU - Johnson, Kenneth

PY - 2012/11/9

Y1 - 2012/11/9

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

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

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

U2 - 10.1007/978-3-642-34059-8_16

DO - 10.1007/978-3-642-34059-8_16

M3 - Conference contribution

AN - SCOPUS:84868341735

SN - 9783642340581

VL - 7539 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 303

EP - 329

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

T2 - 17th Monterey Workshop on Large-Scale Complex IT Systems, LSCITS 2012

Y2 - 19 March 2012 through 21 March 2012

ER -