Abstract
The recent development of model update aims to enhance model checking functions and provides computer aided modifications in system development. On the other hand, constraints have been playing an essential role in describing rational system behaviours. In previous model update approaches, constraints are usually not considered in the update process. In this paper, we present an ACTL - a widely used fragment of Computation Tree Logic (CTL), local model update approach where constraints have been explicitly taken into account. This approach handles constraints effectively by integrating constraint automata into the underlying model update. We demonstrate the effectiveness of our approach through the case study of the correction of the well known mutual exclusion program.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Berard, B., et al.: System and Software Verification: Model-Checking techniques and tools. Springer, Heidelberg (2001)
Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: On ACTL formulas having linear counterexamples. Journal of Computer and System Sciences 62, 463–515 (2001)
Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artificial Intelligence 112, 57–104 (1999)
Clarke Jr., E., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 19–29 (2002)
Clarke Jr., E., Grumberg, O., Jha, S., Liu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of ACM 50, 752–794 (2003)
Fraser, G., Wotawa, F.: Nondeterministic testing with linear model-checking counterexamples. In: Proceedings of the 7th Intel. Conf on Quality Software, QSIC 2007 (2007)
Harris, H., Ryan, M.: Theoretical foundations of updating systems. In: Proceedings 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, 2nd edn. Cambridge University Press, Cambridge (2004)
Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. Journal of Computer and System Sciences (2010) (to appear)
Kelly, M., Zhang, Y., Zhou, Y.: Local model update with an application to sliding window protocol (2010) (under review)
Zhang, Y., Ding, Y.: CTL model update for system modifications. Journal of Artificial Intelligence Research 31, 113–155 (2008)
Zhang, Y., Kelly, M., Zhou, Y.: Foundations of tree-like local model updates (2010) (under review)
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
Kelly, M., Pu, F., Zhang, Y., Zhou, Y. (2010). ACTL Local Model Update with Constraints. In: Setchi, R., Jordanov, I., Howlett, R.J., Jain, L.C. (eds) Knowledge-Based and Intelligent Information and Engineering Systems. KES 2010. Lecture Notes in Computer Science(), vol 6279. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15384-6_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-15384-6_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15383-9
Online ISBN: 978-3-642-15384-6
eBook Packages: Computer ScienceComputer Science (R0)