Abstract
Computational Tree Logic (CTL) model update is a new system modification method for software verification. In this paper, a case study is described to show how a prototype model updater is implemented based on the authors’ previous work of model update theoretical results [4]. The prototype is coded in Linux C and contains model checking, model update and parsing functions. The prototype is applied to the well known microwave oven example. This case study also illustrates some key features of our CTL model update approach such as the five primitive CTL model update operations and the associated minimal change semantics. This case study can be viewed as the first step towards the integration of model checking and model update for practical system modifications.
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.
References
Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artificial Intelligence 112(1999), 57–104 (1999)
Clarke Jr., E., et al.: Model Checking, p. 314. The MIT press, Cambridge (1999)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Ding, Y., Zhang, Y.: Model updating CTL systems. In: Zhang, S., Jarvis, R. (eds.) AI 2005. LNCS, vol. 3809, pp. 1–12. Springer, Heidelberg (2005)
Gammie, P., van der Meyden, R.: MCK: Model Checking the Logic of Knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)
Harris, H., Ryan, M.: Theoretical foundations of updating systems. In: The Proceeding of the 18th IEEE International Conference on Automated Software Engineering, pp. 291–298 (2003)
Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. University Press, Cambridge (2000)
Holzmann, G.: The SPIN Model Checking: Primer and Reference Manual, p. 596. Addison-Wesley Professional, Reading (2003)
McMillan, K., Amla, N.: Automatic abstraction without counterexamples. Cadence Berkeley Labs, Cadence Design Systems (2002)
McMillan, K.: The SMV System (1992), http://www.cs.cmu.edu/~modelcheck/smv.html
Wing, J., Vaziri-Farahani, M.: A case study in model checking software. In: Proceedings 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
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ding, Y., Zhang, Y. (2006). A Case Study for CTL Model Update. In: Lang, J., Lin, F., Wang, J. (eds) Knowledge Science, Engineering and Management. KSEM 2006. Lecture Notes in Computer Science(), vol 4092. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11811220_9
Download citation
DOI: https://doi.org/10.1007/11811220_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37033-8
Online ISBN: 978-3-540-37035-2
eBook Packages: Computer ScienceComputer Science (R0)