×

zbMATH — the first resource for mathematics

Theorem proving based on proof scores for rewrite theory specifications of OTSs. (English) Zbl 1407.68298
Iida, Shusaku (ed.) et al., Specification, algebra, and software. Essays dedicated to Kokichi Futatsugi. Berlin: Springer. Lect. Notes Comput. Sci. 8373, 630-656 (2014).
Summary: We have intensively used proof scores to theorem prove that equational theory specifications of observational transition systems (OTSs) have properties. The paper describes a way to theorem prove that rewrite theory specifications of OTSs have invariant properties by proof score writing. The method may achieve a more faithfully seamless integration of model checking and theorem proving because no translation is needed for system specifications. The Lowe’s modification (NSLPK) of NSPK authentication protocol is used to describe the method.
For the entire collection see [Zbl 1283.68036].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
CafeOBJ; CIRC; CITP; Maude; OBJ3; TRAM; UNITY
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ogata, K., Kurihara, S., Inari, M., Doi, N.: The design and implementation of HoME. In: PLDI 1992, pp. 44–54 (1992) · doi:10.1145/143095.143117
[2] Ogata, K., Doi, N.: Object allocation and dynamic compilation in MultithreadSmalltalk. In: 9th SAC, pp. 452–456 (1994) · doi:10.1145/326619.326808
[3] Ogata, K., Ohhara, K., Futatsugi, K.: TRAM: An abstract machine for order-sorted conditional term rewriting systems. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 335–338. Springer, Heidelberg (1997) · Zbl 06808117 · doi:10.1007/3-540-62950-5_84
[4] Ogata, K., Kondo, M., Ioroi, S., Futatsugi, K.: Design and implementation of Parallel TRAM. In: Lengauer, C., Griebl, M., Gorlatch, S. (eds.) Euro-Par 1997. LNCS, vol. 1300, pp. 1209–1216. Springer, Heidelberg (1997) · Zbl 0996.68654 · doi:10.1007/BFb0002874
[5] Ogata, K., Hirata, H., Ioroi, S., Futatsugi, K.: Experimental implementation of Parallel TRAM on massively parallel computer. In: Pritchard, D., Reeve, J. (eds.) Euro-Par 1998. LNCS, vol. 1470, pp. 846–851. Springer, Heidelberg (1998) · doi:10.1007/BFb0057939
[6] Ogata, K., Futatsugi, K.: Specification and verification of some classical mutual exclusion algorithms with CafeOBJ. In: OBJ/CafeOBJ/Maude Workshop at FM 1999, pp. 159–177 (1999)
[7] 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) · Zbl 1253.68249 · doi:10.1007/978-3-540-39958-2_12
[8] Ogata, K., Futatsugi, K.: Some tips on writing proof scores in the OTS/CafeOBJ method. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Goguen Festschrift. LNCS, vol. 4060, pp. 596–615. Springer, Heidelberg (2006) · Zbl 1132.68489 · doi:10.1007/11780274_31
[9] Goguen, J., Malcolm, G.: A hidden agenda. TCS 245, 55–101 (2000) · Zbl 0946.68070 · doi:10.1016/S0304-3975(99)00275-3
[10] Diaconescu, R., Futatsugi, K.: Behavioural coherence in object-oriented algebraic specification. J. UCS 6, 74–95 (2000) · Zbl 0963.68104
[11] Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley (1988) · Zbl 0717.68034
[12] Diaconescu, R., Futatsugi, K.: CafeOBJ report. AMAST Series in Computing 6. World Scientific (1998) · Zbl 0962.68115
[13] Ogata, K., Futatsugi, K.: Formal verification of the MCS list-based queuing lock. In: Thiagarajan, P.S., Yap, R. (eds.) ASIAN 1999. LNCS, vol. 1742, pp. 281–293. Springer, Heidelberg (1999) · Zbl 0959.68505 · doi:10.1007/3-540-46674-6_24
[14] Ogata, K., Futatsugi, K.: Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm. In: Jacobs, B., Rensink, A. (eds.) Formal Methods for Open Object-Based Distributed Systems V. IFIP, vol. 81, pp. 181–195. Springer, Heildelberg (2002) · Zbl 1056.68162 · doi:10.1007/978-0-387-35496-5_13
[15] Xiang, J., Ogata, K., Futatsugi, K.: Formal fault tree analysis of state transition systems. In: 5th QSIC, pp. 124–131 (2005)
[16] Kong, W., Ogata, K., Futatsugi, K.: Specification and verification of workflows with RBAC mechanism and SoD constraints. IJSEKE 17, 3–32 (2007)
[17] Ogata, K., Futatsugi, K.: Formal analysis of the bakery protocol with consideration of nonatomic reads and writes. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 187–206. Springer, Heidelberg (2008) · Zbl 05362216 · doi:10.1007/978-3-540-88194-0_13
[18] Kong, W., Ogata, K., Futatsugi, K.: Towards reliable e-government systems with the OTS/CafeOBJ method. IEICE Transactions E93-D, 974–984 (2010) · doi:10.1587/transinf.E93.D.974
[19] Ogata, K., Futatsugi, K.: Proof score approach to analysis of electronic commerce protocols. IJSEKE 20, 253–287 (2010)
[20] Zhang, M., Ogata, K., Futatsugi, K.: Formalization and verification of behavioral correctness of dynamic software updates. In: 2nd VSSE. ENTCS, vol. 294, pp. 12–23 (2013)
[21] Futatsugi, K., Goguen, J., Ogata, K.: Verifying design with proof scores. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 277–290. Springer, Heidelberg (2008) · Zbl 05295165 · doi:10.1007/978-3-540-69149-5_30
[22] Futatsugi, K., Găină, D., Ogata, K.: Principles of proof scores in CafeOBJ. TCS 464, 90–112 (2012) · Zbl 1253.68220 · doi:10.1016/j.tcs.2012.07.041
[23] Ogata, K., Futatsugi, K.: Proof score approach to verification of liveness properties. IEICE Transactions E91-D, 2804–2817 (2008) · doi:10.1093/ietisy/e91-d.12.2804
[24] Ogata, K., Futatsugi, K.: Modeling and verification of real-time systems based on equations. SCP 66, 162–180 (2007) · Zbl 1116.68054
[25] Ouranos, I., Ogata, K., Stefaneas, P.: Formal analysis of TESLA protocol in the Timed OTS/CafeOBJ method. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 126–142. Springer, Heidelberg (2012) · Zbl 06246820 · doi:10.1007/978-3-642-34032-1_15
[26] Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Creme: An automatic invariant prover of behavioral specifications. IJSEKE 17, 783–804 (2007)
[27] Găină, D., Futatsugi, K., Ogata, K.: Constructor-based logics. J. UCS 18, 90–112 (2012) · Zbl 1362.68193
[28] Găină, D., Zhang, M., Chiba, Y., Arimoto, Y.: Constructor-based inductive theorem prover. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 328–333. Springer, Heidelberg (2013) · Zbl 1396.68112 · doi:10.1007/978-3-642-40206-7_26
[29] Ogata, K., Nakano, M., Kong, W., Futatsugi, K.: Induction-guided falsification. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 114–131. Springer, Heidelberg (2006) · doi:10.1007/11901433_7
[30] Ogata, K., Futatsugi, K.: A combination of forward & backward reachability analysis methods. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 501–517. Springer, Heidelberg (2010) · Zbl 05854667 · doi:10.1007/978-3-642-16901-4_33
[31] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007) · Zbl 1115.68046
[32] Kong, W., Ogata, K., Futatsugi, K.: Model-checking observational transition system with Maudea. In: 20th ITC-CSCC, pp. 5–6 (2005)
[33] Ogata, K., Kong, W., Futatsugi, K.: Falsification of OTSs by searches of bounded reachable state spaces. In: 18th SEKE, pp. 440–445 (2006)
[34] Kong, W., Ogata, K., Seino, T., Futatsugi, K.: A lightweight integration of theorem proving and model checking for system verification. In: 12th APSEC, pp. 59–66 (2005) · doi:10.1109/APSEC.2005.9
[35] Nakamura, M., Kong, W., Ogata, K., Futatsugi, K.: A specification translation from behavioral specifications to rewrite specifications. IEICE Transactions E91-D, 1492–1503 (2008) · doi:10.1093/ietisy/e91-d.5.1492
[36] Zhang, M., Ogata, K., Nakamura, M.: Translation of state machines from equational theories into rewrite theories with tool support. IEICE Transactions 94-D, 976–988 (2011) · doi:10.1587/transinf.E94.D.976
[37] Zhang, M., Ogata, K.: Invariant-preserved transformation of state machines from equations into rewrite rules. In: 18th APSEC, pp. 511–516 (2012) · doi:10.1109/APSEC.2012.99
[38] Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. IPL 56, 131–133 (1995) · Zbl 0875.94114 · doi:10.1016/0020-0190(95)00144-2
[39] Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. CACM 21, 993–999 (1978) · Zbl 0387.68003 · doi:10.1145/359657.359659
[40] Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE TIT IT-29, 198–208 (1983) · Zbl 0502.94005
[41] Goguen, J., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing OBJ. In: Software Engineering with OBJ: Algebraic Specification in Action. Kluwer (2000) · doi:10.1007/978-1-4757-6541-0_1
[42] Meseguer, J., Palomino, M., Martí-Oliet, N.: Equational abstractions. TCS 403, 239–264 (2008) · Zbl 1155.68050 · doi:10.1016/j.tcs.2008.04.040
[43] Rocha, C., Meseguer, J.: Proving safety properties of rewrite theories. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 314–328. Springer, Heidelberg (2011) · Zbl 1344.68142 · doi:10.1007/978-3-642-22944-2_22
[44] Jouannaud, J.P., Kirchner, C., Kirchner, H.: Incremental construction of unification algorithms in equational theories. In: Diaz, J. (ed.) 10th ICALP. LNCS, vol. 154, pp. 361–373. Springer, Heidelberg (1983) · Zbl 0516.68067
[45] Ogata, K., Futatsugi, K.: Compositionally writing proof scores of invariants in the OTS/CafeOBJ method. J. UCS 19, 771–804 (2013)
[46] Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: 24th RTA, pp. 81–96 (2013) · Zbl 1356.68140
[47] 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) · Zbl 1278.68199 · doi:10.1007/978-3-540-45069-6_2
[48] 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) · doi:10.1007/978-3-540-27813-9_45
[49] Hennicker, R.: Context induction: A proof principle for behavioural abstractions. In: Miola, A. (ed.) DISCO 1990. LNCS, vol. 429, pp. 101–110. Springer, Heidelberg (1990)
[50] Roşu, G., Lucanu, D.: Circular coinduction: A proof theoretical foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 127–144. Springer, Heidelberg (2009) · Zbl 1239.68067 · doi:10.1007/978-3-642-03741-2_10
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.