An optimised algorithm to tackle the model explosion problem in CTL model update

Abstract

Computational Tree Logic (CTL) model update is an approach to software verification and modification, where minimal change is employed to generate updated models that represent the corrected software design. In this paper, we propose a new update principle named minimal change with maximal reachable states (II) which is a further optimisation of an existing algorithm to solve a model explosion problem during CTL model update. We provide comparison of the two methods based on Graph Theory. The algorithm of this update principle is also provided. Our experimental results show that in the case of updating the Andrew File System protocol model, the new CTL update approach significantly narrows down the committed models to fewer strong committed models.