article

CTL model update for system modifications

Authors:

Yulin DingAuthors Info & Claims

Journal of Artificial Intelligence Research, Volume 31, Issue 1

Pages 113 - 155

Published: 01 January 2008 Publication History

Abstract

Model checking is a promising technology, which has been applied for verification of many hardware and software systems. In this paper, we introduce the concept of model update towards the development of an automatic system modification tool that extends model checking functions. We define primitive update operations on the models of Computation Tree Logic (CTL) and formalize the principle of minimal change for CTL model update. These primitive update operations, together with the underlying minimal change principle, serve as the foundation for CTL model update. Essential semantic and computational characterizations are provided for our CTL model update approach. We then describe a formal algorithm that implements this approach. We also illustrate two case studies of CTL model updates for the well-known microwave oven example and the Andrew File System 1, from which we further propose a method to optimize the update results in complex system modifications.

References

[1]

Amla, N., Du, X., Kuehlmann, A., Kurshan, R., & McMillan, K. (2005). An analysis of sat-based model checking techniques in an industrial environment. In Proceedings of Correct Hardware Design and Verification Methods - 13th IFIP WG 10.5 Advanced Research Working Conference (CHARME 2005), pp. 254-268.

Digital Library

[2]

Baral, C., & Zhang, Y. (2005). Knowledge updates: semantics and complexity issues. Artificial Intelligence, 164, 209-243.

Digital Library

[3]

Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., & Schnoebelen, P. (2001). System and Software Verification: Model-Checking Techniques and Tools. Springer-Verlag Berlin Heidelberg.

[4]

Boyer, M., & Sighireanu, M. (2003). Synthesis and verification of constraints in the pgm protocol. In Proceedings of the 12th International Symposium of Formal Methods Europe (FME'03), pp. 264-281. Springer Verlag.

[5]

Buccafurri, F., Eiter, T., Gottlob, G., & Leone, N. (1999). Enhancing model checking in verification by ai techniques. Artificial Intelligence, 112, 57-104.

Digital Library

[6]

Buccafurri, F., Eiter, T., Gottlob, G., & Leone, N. (2001). On actl formulas having linear counterexamples. Journal of Computer and System Sciences, 62, 463-515.

Digital Library

[7]

Chauhan, P., Clarke, E., Kukula, J., Sapra, S., Veith, H., & Wang, D. (2002). Automated abstraction refinement for model checking large state spaces using sat based conflict analysis. In Proceedings of Formal Methods in Computer Aided Design (FMCAD'02), pp. 33-51.

Digital Library

[8]

Cimatti, A., Clarke, E., Giunchiglia, F., & Roveri, M. (1999). Nusmv: A new symbolic model verifier. In Proceedings of the 11th International Conference on Computer Aided Verification, pp. 495-499.

Digital Library

[9]

Clarke, E., Grumberg, O., Jha, S., Liu, Y., & Veith, H. (2003). Counterexample-guided abstraction refinement for symbolic model checking. Journal of ACM, 50, 752-794.

Digital Library

[10]

Clarke, E., Grumberg, O., & Peled, D. (1999). Model Checking. MIT Press.

Digital Library

[11]

Clarke, E., Jha, S., Lu, Y., & Veith, H. (2002). Tree-like counterexamples in model checking. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), pp. 19-29.

Digital Library

[12]

Dennis, L., Monroy, R., & Nogueira, P. (2006). Proof-directed debugging and repair. In Proceedings of the 7th Symposium on Trends in Functional Programming, pp. 131-140.

[13]

Ding, Y., & Zhang, Y. (2005). A logic approach for ltl system modification. In Proceedings of the 15th International Symposium on Methodologies for Intelligent Systems (ISMIS 2005), pp. 436-444. Springer.

Digital Library

[14]

Ding, Y., & Zhang, Y. (2006). Ctl model update: Semantics, computations and implementation. In Proceedings of the 17th European Conference on Artificial Intelligence (ECAI 2006), pp. 362-366. IOS Press.

Digital Library

[15]

Eiter, T., & Gottlob, G. (1992). On the complexity of propositional knowledge base revision, updates, and counterfactuals. Artificial Intelligence, 57, 227-270.

Digital Library

[16]

Gammie, P., & van der Meyden, R. (2004). Mck-model checking the logic of knowledge. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV-2004), pp. 479-483.

[17]

Gardenfors, P. (1988). Knowledge in Flux: Modeling the Dynamics of Epistemic States. The MIT Press.

[18]

Groce, A., & Visser, W. (2003). What went wrong: Explaining counterexamples. In Proceedings of the SPIN Workshop on Model Checking of Software, pp. 121-135.

Digital Library

[19]

Harris, H., & Ryan, M. (2002). Feature integration as an operation of theory change. In Proceedings of the 15th European Conference on Artificial Intelligence (ECAI-2002), pp. 546-550.

Digital Library

[20]

Harris, H., & Ryan, M. (2003). Theoretical foundations of updating systems. In Proceedings of the 18th IEEE International Conference on Automated Software Engineering, pp. 291-298.

Digital Library

[21]

Herzig, A., & Rifi, O. (1999). Propositional belief base update and minimal change. Artificial Intelligence, 115, 107-138.

Digital Library

[22]

Holzmann, C. (2003). The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional.

Digital Library

[23]

Huth, M., & Ryan, M. (2004). Logic in Computer Science: Modelling and Reasoning about Systems. 2nd edition, Cambridge University Press.

Digital Library

[24]

Katsuno, H., & Mendelzon, A. (1991). On the difference between updating a knowledge base and revising it. In Proceedings of International Conference on the Principles of Knowledge Representation and Reasoning (KR'91), pp. 387-394.

[25]

McMillan, K., & Amla, N. (2002). A logic of implicit and explicit belief. In Automatic Abstraction without Counterexamples. Cadence Berkeley Labs, Cadence Design Systems.

[26]

Pettie, S., & Ramachandran, V. (2002). An optimal minimum spanning tree algorithm. Journal of ACM, 49, 16-34.

Digital Library

[27]

Rustan, K., Leino, M., Millstein, T., & Saxe, J. (2005). Generating error traces from verification-condition counterexamples. Science of Computer Programming, 55, 209- 226.

Digital Library

[28]

Stumptner, M., & Wotawa, F. (1996). A model-based approach to software debugging. In Proceedings of the 7th International Workshop on Principles of Diagnosis.

[29]

Wing, J., & Vaziri-Farahani, M. (1995). A case study in model checking software. In Proceedings of the 3rd ACM SIGSOFT Symposium on the Foundations of Software Engineering.

Digital Library

[30]

Winslett, M. (1988). Reasoning about action using a possible models approach. In Proceedings of AAAI-88, pp. 89-93.

[31]

Winslett, M. (1990). Updating Logical Databases. Cambridge University Press.

Digital Library

Cited By

Ribeiro JNayak AWassermann R(2019)Belief update without compactness in non-finitary languagesProceedings of the 28th International Joint Conference on Artificial Intelligence10.5555/3367243.3367296(1858-1864)Online publication date: 10-Aug-2019
https://dl.acm.org/doi/10.5555/3367243.3367296
Monperrus M(2018)Automatic Software RepairACM Computing Surveys10.1145/310590651:1(1-24)Online publication date: 23-Jan-2018
https://dl.acm.org/doi/10.1145/3105906
Attie PBab KSakr M(2017)Model and Program Repair via SAT SolvingACM Transactions on Embedded Computing Systems10.1145/314742617:2(1-25)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3147426
Show More Cited By

CTL model update for system modifications
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

A case study for CTL model update
KSEM'06: Proceedings of the First international conference on Knowledge Science, Engineering and Management

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 ...
Model Checking CTL*[DC]
TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

We define a logic called CTL*[DC] which extends CTL* with ability to specify past-time and quantitative timing properties using the formulae of Quantified Discrete-time Duration Calculus (QDDC). Alternately, we can consider CTL*[DC] as extending logic ...
CTL Model Update: Semantics, Computations and Implementation
Proceedings of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy

Minimal change is a fundamental principle for modeling system dynamics. In this paper, we study the issue of minimal change for Computational Tree Logic (CTL) model update. We first propose five primitive operations which capture the basic update of the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Artificial Intelligence Research

Journal of Artificial Intelligence Research Volume 31, Issue 1

January 2008

651 pages

ISSN:1076-9757

Issue’s Table of Contents

Publisher

AI Access Foundation

El Segundo, CA, United States

Publication History

Published: 01 January 2008

Received: 01 August 2007

Published in JAIR Volume 31, Issue 1

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ribeiro JNayak AWassermann R(2019)Belief update without compactness in non-finitary languagesProceedings of the 28th International Joint Conference on Artificial Intelligence10.5555/3367243.3367296(1858-1864)Online publication date: 10-Aug-2019
https://dl.acm.org/doi/10.5555/3367243.3367296
Monperrus M(2018)Automatic Software RepairACM Computing Surveys10.1145/310590651:1(1-24)Online publication date: 23-Jan-2018
https://dl.acm.org/doi/10.1145/3105906
Attie PBab KSakr M(2017)Model and Program Repair via SAT SolvingACM Transactions on Embedded Computing Systems10.1145/314742617:2(1-25)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3147426
Gómez SGoron AGroza ALetia I(2016)Assuring safety in air traffic control systems with argumentation and model checkingExpert Systems with Applications: An International Journal10.1016/j.eswa.2015.09.02744:C(367-385)Online publication date: 1-Feb-2016
https://dl.acm.org/doi/10.1016/j.eswa.2015.09.027
Beck HDao-Tran MEiter T(2015)Answer update for rule-based stream reasoningProceedings of the 24th International Conference on Artificial Intelligence10.5555/2832581.2832632(2741-2747)Online publication date: 25-Jul-2015
https://dl.acm.org/doi/10.5555/2832581.2832632
(2015)Model and program repair via SAT solvingProceedings of the 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2015.7340481(148-157)Online publication date: 1-Sep-2015
https://dl.acm.org/doi/10.1109/MEMCOD.2015.7340481
Gerasimou STamburrelli GCalinescu RCohen MGrunske LWhalen M(2015)Search-based synthesis of probabilistic models for quality-of-service software engineeringProceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2015.22(319-330)Online publication date: 9-Nov-2015
https://dl.acm.org/doi/10.1109/ASE.2015.22
Carrillo MRosenblueth D(2014)CTL update of Kripke models through protectionsArtificial Intelligence10.1016/j.artint.2014.02.005211:1(51-74)Online publication date: 1-Jun-2014
https://dl.acm.org/doi/10.1016/j.artint.2014.02.005
Bonakdarpour BKulkarni S(2012)Automated model repair for distributed programsACM SIGACT News10.1145/2261417.226143743:2(85-107)Online publication date: 11-Jun-2012
https://dl.acm.org/doi/10.1145/2261417.2261437
Guerra PWassermann R(2011)Belief revision on computation tree logicProceedings of the Twenty-Second international joint conference on Artificial Intelligence - Volume Volume Three10.5555/2283696.2283872(2810-2811)Online publication date: 16-Jul-2011
https://dl.acm.org/doi/10.5555/2283696.2283872
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents