Advertisement

Induction-Guided Falsification

  • Kazuhiro Ogata
  • Masahiro Nakano
  • Weiqiang Kong
  • Kokichi Futatsugi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4260)

Abstract

The induction-guided falsification searches a bounded reachable state space of a transition system for a counterexample that the system satisfies an invariant property. If no counterexamples are found, it tries to verify that the system satisfies the property by mathematical induction on the structure of the reachable state space of the system, from which some other invariant properties may be obtained as lemmas. The verification and falsification process is repeated for each of the properties until a counterexample is found or the verification is completed. The NSPK authentication protocol is used as an example to demonstrate the induction-guided falsification.

Keywords

CafeOBJ counterexample induction invariant Maude observational transition system (OTS) 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Ogata, K., Futatsugi, K.: Proof scores in the OTS/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  2. 2.
    Diaconescu, R., Futatsugi, K.: CafeOBJ Report. AMAST Series in Computing, vol. 6. World Scientific, Singapore (1998)zbMATHGoogle Scholar
  3. 3.
    Ogata, K., Futatsugi, K.: Formally modeling and verifying Ricart&Agrawala distributed mutual exclusion algorithm. In: 2nd APAQS, pp. 357–366. IEEE CS Press, Los Alamitos (2001)Google Scholar
  4. 4.
    Ogata, K., Futatsugi, K.: Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm. In: 5th FMOODS, pp. 181–195. Kluwer, Dordrecht (2002)Google Scholar
  5. 5.
    Ogata, K., Futatsugi, K.: Rewriting-based verification of authentication protocols. In: 4th WRLA 2002. ENTCS 71. Elsevier, Amsterdam (2002)Google Scholar
  6. 6.
    Ogata, K., Futatsugi, K.: Formal analysis of the iKP electronic payment protocols. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 441–460. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Ogata, K., Futatsugi, K.: Formal verification of the Horn-Preneel micropayment protocol. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 238–252. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Ogata, K., Futatsugi, K.: Equational approach to formal verification of SET. In: 4th QSIC, pp. 50–59. IEEE CS Press, Los Alamitos (2004)Google Scholar
  9. 9.
    Ogata, K., Futatsugi, K.: Formal analysis of the NetBill electronic commerce protocol. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 45–64. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  10. 10.
    Ogata, K., Futatsugi, K.: Equational approach to formal analysis of TLS. In: 25th ICDCS, pp. 795–804. IEEE CS Press, Los Alamitos (2005)Google Scholar
  11. 11.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Quesada, J.: Maude: Spesification and programming language in rewriting logic. TCS 285, 187–243 (2002)zbMATHCrossRefGoogle Scholar
  12. 12.
    Ogata, K., Kong, W., Futatsugi, K.: Falsification of OTSs by searches of bounded reachable state spaces. In: 18th SEKE, pp. 440–445 (2006)Google Scholar
  13. 13.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Advances in Computers, vol. 58. Academic Press, London (2003)Google Scholar
  14. 14.
    Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. CACM 21, 993–999 (1978)zbMATHGoogle Scholar
  15. 15.
    Kong, W., Ogata, K., Futatsugi, K.: Model-checking observational transition system with Maude. In: 20th ITC-CSCC, pp. 5–6 (2005)Google Scholar
  16. 16.
    Hsiang, J., Dershowitz, N.: Rewrite methods for clausal and nonclausal theorem proving. In: Díaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 331–346. Springer, Heidelberg (1983)CrossRefGoogle Scholar
  17. 17.
    Ogata, K., Futatsugi, K.: Some tips on writing proof scores in the OTS/CafeOBJ method. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 596–615. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    Edmund, M., Clarke, J., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2001)Google Scholar
  19. 19.
    Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: WRLA 2002. ENTCS 71, pp. 143–168. Elsevier, Amsterdam (2002)Google Scholar
  20. 20.
    Wang, B.Y.: Specification of an infinite-state local model checker in rewriting logic. In: 17th SEKE, pp. 442–447 (2005)Google Scholar
  21. 21.
    Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM TOPLAS 16, 1512–1542 (1994)CrossRefGoogle Scholar
  22. 22.
    de Moura, L., Rueß, H., Sorea, M.: Bounded model checking and induction: From refutation to verification. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 14–26. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  23. 23.
    de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N., Sorea, M., Tiwari, A.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496–500. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  24. 24.
    Kong, W., Ogata, K., Seino, T., Futatsugi, K.: Lightweight integration of theorem proving and model checking for system verification. In: 12th APSEC, pp. 59–66. IEEE CS Press, Los Alamitos (2005)Google Scholar
  25. 25.
    Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Automatic verification of the STS authentication protocol with Crème. In: 20th ITC-CSCC, pp. 15–16 (2005)Google Scholar
  26. 26.
    Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Automating invariant verification of behavioral specifications. In: 6th QSIC. IEEE CS Press, Los Alamitos (2006)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Kazuhiro Ogata
    • 1
  • Masahiro Nakano
    • 1
  • Weiqiang Kong
    • 1
  • Kokichi Futatsugi
    • 1
  1. 1.School of Information ScienceJapan Advanced Institute of Science and Technology (JAIST) 

Personalised recommendations