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. © Springer-Verlag 2010.
CITATION STYLE
Kelly, M., Pu, F., Zhang, Y., & Zhou, Y. (2010). ACTL local model update with constraints. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6279 LNAI, pp. 135–144). https://doi.org/10.1007/978-3-642-15384-6_15
Mendeley helps you to discover research relevant for your work.