System Design Modification with Actions

  • Maria Viviane de Menezes
  • Silvio do Lago Pereira
  • Leliane Nunes de Barros
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6404)


System designers are expected to use error-detecting and correcting techniques. Although, model checking approaches have been used for verification of errors in large complex systems, they can only detect the error. the task of correcting the system design (called model update) is completely left to the system designer. Recent works on model update can suggest changes in the system model which do not consider domain contingencies and constraints. In this paper, we present a model update approach that can be used to automatically suggest modifications in a system based on the actions that are behind state transitions and a set of domain constraints. We claim that with this approach we can develop more realistic system error-correcting tools.


Model Checking Model Update Temporal Logic Reasoning about action Automated design 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. J. Artif. Intell. 112, 57–104 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  3. 3.
    Harris, H., Ryan, M.: Theoretical foundations of updating systems. In: 18th IEEE International Conference on Automated Software Engineering, pp. 291–294 (2003)Google Scholar
  4. 4.
    Katsuno, H., Mendelzon, A.O.: On the difference between updating a knowledge base and revising it. In: 2nd International Conference on the Principles of Knowledge Representation and Reasoning, pp. 387–394 (1991)Google Scholar
  5. 5.
    Kripke, S.: Semantical Considerations on Modal Logic. J. Acta Philosophica Fennica 16, 83–94 (1963)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Müller-Olm, M., Schmidt, D., Steffen, B.: Model-Checking: A Tutorial Introduction. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 330–354. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Pereira, S.L., Barros, L.N.: A logic-based agent that plans for extended reachability goals. Journal Autonomous Agents and Multi-Agent Systems 16, 327–344 (2008)CrossRefGoogle Scholar
  8. 8.
    Pnueli, A.: The temporal logic of programs. In: 18th Symposium Foundations of Computer Science, pp. 46–57 (1977)Google Scholar
  9. 9.
    Winslett, M.: Reasoning about action using a possible models approach. In: 7th American Association for Artificial Intelligence, pp. 89–93 (1988)Google Scholar
  10. 10.
    Zhang, Y., Ding, Y.: CTL Model Update for System Modifications. J. Artif. Int. Res. 31, 113–155 (2008)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Maria Viviane de Menezes
    • 1
  • Silvio do Lago Pereira
    • 2
  • Leliane Nunes de Barros
    • 1
  1. 1.Department of Computer ScienceIME-USPBrazil
  2. 2.Department of Information TechnologyFATEC-SP\CEETEPSBrazil

Personalised recommendations