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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artificial Intelligence 112, 57–104 (1999)
Christofides, N.: Graph Theory – An Algorithmic Approach. Academic Press, London (1975)
Clarke Jr., E., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
Ding, Y., Zhang, Y.: A Study of the Model Explosion Problem in CTL Model Update. In: Proc. of the 20th International Conference on Software Engineering and Knowledge Engineering, SEKE 2008 (2008)
Ding, Y.: Model Update for System Modifications. Ph.D Thesis. School of Computing and Mathematics, University of Western Sydney (2007)
Ding, Y., Zhang, Y.: CTL model update: Semantics, computations and implementation. In: Proc. of the 17th European Conference on Artificial Intelligence, ECAI 2006 (2006)
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. University Press, Cambridge (2000)
Wing, J., Vaziri-Farahani, M.: A case study in model checking software. In: Proc. of 3rd ACM SIGSOFT Symposium on the Foundations of Software Engineering (October 1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ding, Y., Hemer, D. (2010). An Optimised Algorithm to Tackle the Model Explosion Problem in CTL Model Update. In: Zhang, BT., Orgun, M.A. (eds) PRICAI 2010: Trends in Artificial Intelligence. PRICAI 2010. Lecture Notes in Computer Science(), vol 6230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15246-7_54
Download citation
DOI: https://doi.org/10.1007/978-3-642-15246-7_54
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15245-0
Online ISBN: 978-3-642-15246-7
eBook Packages: Computer ScienceComputer Science (R0)