Efficient model checking of IT change operations

Sebastian Hagen, Weverton Luis Da Costa Cordeiro, Luciano Paschoal Gaspary, Lisandro Zambenedetti Granville, Alfons Kemper

Research output: Contribution to journalArticlepeer-review

1 Scopus citations


The success of businesses in modern organizations heavily depends on the high availability of information technology (IT) infrastructures. To prevent business disruption, IT operators have worked hard to ensure that any changes to this infrastructure are properly and efficiently deployed. Change management-a discipline of the Information Technology Infrastructure Library (ITIL)-provides important guidance to help achieve this end. As IT infrastructures grow larger, however, ensuring that changes are harmless to business continuity becomes increasingly complex. In fact, previous research has shown that existing approaches for verifying changes suffer from severe scalability issues. This problem can become a serious threat to most organizations, as it can lead for example to customer dissatisfaction due to missed deadlines in service change deployment. To bridge this gap, we propose a partial-order reduction model checking paradigm and algorithm for efficiently detecting harmful change operations. Our model improves the complexity of verifying a set of concurrent change activities against safety constraints by reducing-without losing effectiveness-the verification scope. To prove concept and technical feasibility, we carried out an extensive performance evaluation of our algorithm considering a variety of change activities, safety constraints, and configuration scenarios. The results obtained from 32 benchmarks have shown that our algorithm significantly outperformed state-of-the-art, general purpose model checkers, improving the runtime complexity frompolynomial/exponential to linear. In summary, the results evidenced that change verification finally became feasible and efficient for larger IT infrastructures.

Original languageEnglish
Article number6873326
Pages (from-to)292-306
Number of pages15
JournalIEEE Transactions on Network and Service Management
Issue number3
StatePublished - 1 Sep 2014
Externally publishedYes


  • Change management
  • Model checker
  • Partial order reduction
  • Verification


Dive into the research topics of 'Efficient model checking of IT change operations'. Together they form a unique fingerprint.

Cite this