×

A Maude environment for CafeOBJ. (English) Zbl 1358.68195

Summary: We present in this paper an interpreter implemented in Maude for non-behavioral CafeOBJ specifications. This alternative implementation poses a number of advantages: (1) it allows Maude tools to be used with CafeOBJ specifications, (2) it improves the performance of some CafeOBJ commands, such as search, (3) it enriches CafeOBJ syntax with Maude syntax, and (4) it makes CafeOBJ easily extensible, since new commands and tools can be included and tested and, once they are sufficiently mature, can be considered for inclusion in the Lisp implementation of CafeOBJ. The current tool presents a number of improvements over the tool presented in previous papers: it supports principal sorts, all kinds of CafeOBJ views, and all the search predicates recently implemented in the system. These improvements have allowed us to run the most recent CafeOBJ specifications, hence proving the robustness of the tool. Moreover, we present case studies illustrating the power of the tool, focusing on the falsification and verification of the NSPK and QLOCK protocols, respectively.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N20 Theory of compilers and interpreters
68Q42 Grammars and rewriting systems
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Bae K, Escobar S, Meseguer J (2013) Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. In: Raamsdonk F (ed) 24th International Conference on Rewriting Techniques and Applications, RTA 2013, vol 21 of Leibniz International Proceedings in Informatics, Dagstuhl, Germany, pp 81-96. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik · Zbl 1356.68140
[2] Bouhoula, A; Jouannaud, J-P; Meseguer, J, Specification and proof in membership equational logic, Theor Comput Sci, 236, 35-132, (2000) · Zbl 0938.68057
[3] Bidoit M, Mosses PD (2004) Casl user manual, volume 2900 of Lecture Notes in Computer Science. Springer
[4] Bogdanas D, Rosu G (2015) K-java: a complete semantics of java. In: Rajamani SK, Walker D (eds) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015. ACM, pp 445-456 · Zbl 1346.68046
[5] Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott C (2007) All about Maude: a high-performance logical framework, volume 4350 of Lecture Notes in Computer Science. Springer · Zbl 1115.68046
[6] Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott C (2011) Maude manual (version 2.6). http://maude.cs.uiuc.edu/maude2-manual · Zbl 1362.68193
[7] Codescu M, Horozal F, Kohlhase M, Mossakowski T, Rabe F, Sojakova K (2012) Towards logical frameworks in the heterogeneous tool set hets. In: Mossakowski T, Kreowski HJ (eds) Proceedings of the 20th International Workshop on Recent Trends in Algebraic Development Techniques, WADT 2010, Revised Selected Papers, volume 7137 of Lecture Notes in Computer Science. Springer, pp 139-159 · Zbl 1278.68286
[8] Clavel, M; Meseguer, J; Palomino, M, Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic, Theor Comput Sci, 373, 70-91, (2007) · Zbl 1111.03034
[9] Codescu M, Mossakowski T, Riesco A, Maeder C (2011) Integrating Maude into Hets. In: Johnson M, Pavlovic D (eds) Proceedings of the 13th International Conference on Algebraic Methodology and Software Technology, AMAST 2010, volume 6486 of Lecture Notes in Computer Science. Springer, pp 60-75 · Zbl 1308.68075
[10] Şerbanuţă T-F, Roşu G (2010) K-Maude: a rewriting based tool for semantics of programming languages. In: Proceedings of the 8th International Workshop on Rewriting Logic and its Applications, WRLA 2010, volume 6381 of Lecture Notes in Computer Science. Springer, pp 104-122 · Zbl 1111.03034
[11] Diaconescu, R; Futatsugi, K, Behavioural coherence in object-oriented algebraic specification, J Univ Comput Sci, 6, 74-95, (2000) · Zbl 0963.68104
[12] Durán F, Ölveczky PC (2009) A guide to extending Full Maude illustrated with the implementation of Real-Time Maude. In: Roşu G (ed) Proceedings of the 7th International Workshop on Rewriting Logic and its Applications, WRLA 2008, Electronic Notes in Theoretical Computer Science, vol 238(3). Elsevier, pp 83-102 · Zbl 1356.68125
[13] Durán F, Rocha C, Álvarez JM (2011) Towards a Maude formal environment. In: Agha G, Meseguer J, Danvy O (eds) Formal modeling: actors, open systems, biological systems, volume 7000 of Lecture Notes in Computer Science. Springer, pp 329-351
[14] Dolev D, Yao AC (1983) On the security of public key protocols. IEEE TIT. IT-29:198-208 · Zbl 0502.94005
[15] Eker S, Martí-Oliet N, Meseguer J, Verdejo A (2007) Deduction, strategies, and rewriting. In: Archer M, Boy de la Tour T, Munoz CA (eds) Proceedings of the 6th International Workshop on Strategies in Automated Deduction, STRATEGIES 2006. Electronic Notes in Theoretical Computer Science, vol 174(11). Elsevier, pp 3-25 · Zbl 1277.68241
[16] Ellison C, Roşu G (2012) An executable formal semantics of C with applications. In: Proceedings of the 39th Symposium on Principles of Programming Languages, POPL 2012. ACM, pp 533-544
[17] Futatsugi K, Diaconescu R (1998) CafeOBJ Report. World Scientific, AMAST Series · Zbl 0962.68115
[18] Futatsugi, K; Gâinâ, D; Ogata, K, Principles of proof scores in cafeobj, Theor Comput Sci, 464, 90-112, (2012) · Zbl 1253.68220
[19] Futatsugi K. 12th lecture of the course i613 algebraic formal methods. http://www.jaist.ac.jp/ kokichi/class/i613-1312
[20] Futatsugi K (2015) Generate and check method for verifying transition systems in cafeobj. In: De Nicola R, Hennicker R (eds) Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, volume 8950 of Lecture Notes in Computer Science. Springer, pp 171-192
[21] Găină, D; Futatsugi, K; Ogata, K, Constructor-based logics, J Univ Comput Sci, 18, 90-112, (2012) · Zbl 1362.68193
[22] CoFI Tools Task Group. CoFI, the common framework initiative for algebraic specification and development. http://www.cofi.info · Zbl 1049.68091
[23] Goguen J, Winkler T, Meseguer J, Futatsugi K, Jouannaud J-P (2000) Introducing OBJ. In: Software engineering with OBJ: algebraic specification in action. Kluwer · Zbl 1088.68095
[24] Gâinâ D, Zhang M, Chiba Y, Arimoto Y (2013) Constructor-based inductive theorem prover. In: Heckel R, Milius S (eds) Proceedings of the 5th International Conference in Algebra and Coalgebra in Computer Science, CALCO 2013, volume 8089 of Lecture Notes in Computer Science. Springer, pp 328-333. http://www.jaist.ac.jp/ danielmg/citp.html · Zbl 1396.68112
[25] Harper, R; Honsell, F; Plotkin, GD, A framework for defining logics, J ACM, 40, 143-184, (1993) · Zbl 0778.03004
[26] Kirchner H (2013) A rewriting point of view on strategies. In: Mogavero F, Murano A, Vardi MY (eds) Proceedings 1st International Workshop on Strategic Reasoning, SR 2013, Rome, Italy, March 16-17, volume 112 of EPTCS, pp 99-105
[27] Kirchner H (2015) Rewriting strategies and strategic rewrite programs. In: Martí-Oliet N, Ölveczky PC, Talcott C (eds) Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, volume 9200 of Lecture Notes in Computer Science. Springer, pp 380-403 · Zbl 1321.68331
[28] Kreowski H-J, Bernd K-B (eds) (1999) Algebraic Foundations of Systems Specification, 1st edn. Springer, Secaucus, NJ, USA · Zbl 0922.00008
[29] Kirchner C, Kirchner H, Nahon F (2013) Narrowing based inductive proof search. In: Voronkov A, Weidenbach C (eds) Programming logics—essays in memory of Harald Ganzinger, volume 7797 of Lecture Notes in Computer Science. Springer, pp 216-238 · Zbl 1383.03019
[30] Kohlhase M, Mossakowski T (2012) Final project report—latin: Logic atlas and integrator. https://svn.omdoc.org/repos/latin/public/latin_report.pdf · Zbl 1278.68285
[31] Lucanu D, Goriac E-I, Caltais G, Rosu G (2009) CIRC: A behavioral verification tool based on circular coinduction. In: Kurz A, Lenisa M, Tarlecki A (eds) Proceedings of the 3rd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2009, volume 5728 of Lecture Notes in Computer Science. Springer, pp 433-442 · Zbl 1239.68066
[32] Lucanu D, Rosu G (2007) CIRC: a circular coinductive prover. In: Mossakowski T, Montanari U, Haveraaen M (eds) Proceedings of the 2nd International Conference on Algebra and Coalgebra in Computer Science, CALCO 2007, volume 4624 of Lecture Notes in Computer Science, pages. Springer, pp 372-378 · Zbl 1214.68336
[33] Meseguer, J, Conditional rewriting logic as a unified model of concurrency, Theor Comput Sci, 96, 73-155, (1992) · Zbl 0758.68043
[34] Mossakowski T, Maeder C, Codescu M (2014) Hets user guide—version 0.99. Technical report, DFKI GmbH, Formal Methods for Software Development
[35] Mossakowski T, Maeder C, Lüttich K (2007) The Heterogeneous Tool Set. In: Grumberg O, Huth M (eds) Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007, volume 4424 of Lecture Notes in Computer Science. Springer-Verlag Heidelberg, pp 519-522
[36] Mosses P (2004) (ed) Casl reference manual, volume 2960 of Lecture Notes in Computer Science. Springer
[37] Meseguer, J; Roşu, G, The rewriting logic semantics project, Theor Comput Sci, 373, 213-237, (2007) · Zbl 1111.68068
[38] Nakamura M, Kong W, Ogata K, Futatsugi K (2008) A specification translation from behavioral specifications to rewrite specifications. IEICE Trans 91-D(5):1492-1503 · Zbl 0938.68057
[39] Needham, RM; Schroeder, MD, Using encryption for authentication in large networks of computers, Commun ACM, 21, 993-999, (1978) · Zbl 0387.68003
[40] Nakagawa AT, Sawada T, Futatsugi K (2010) CafeOBJ user’s manual (version 1.4.8). http://www.comp.dit.ie/pbrowne/compfund2/manual.pdf
[41] Ogata K, Futatsugi K (2003) Proof scores in the OTS/CafeOBJ method. In: Najm E, Nestmann U, Stevens P (eds) Proceedings of the 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems, FMOODS 2003, volume 2884 of Lecture Notes in Computer Science. pp 170-184 · Zbl 1253.68249
[42] Ogata K, Futatsugi K (2014) Theorem proving based on proof scores for rewrite theory specifications of OTSs. In: Iida S, Meseguer J, Ogata K (eds) Specification, algebra and software: essays Dedicated to Kokichi Futatsugi, volume 8373 of Lecture Notes in Computer Science, pp 630-656 · Zbl 1407.68298
[43] Ölveczky PC, Meseguer J (2007) Semantics and pragmatics of Real-Time Maude. Higher-Order Symb Comput 20: 161-196 · Zbl 1115.68095
[44] Ouranos I, Ogata K, Stefaneas PS (2012) Formal analysis of TESLA protocol in the Timed OTS/CafeOBJ method. In: Margaria T, Steffen B (eds) ISoLA (2), volume 7610 of Lecture Notes in Computer Science. Springer, pp 126-142
[45] Pfenning F (1994) Elf: a meta-language for deductive systems (system descrition). In: Bundy A (ed) Proceedings of the 12th International Conference on Automated Deduction, CADE-12, volume 814 of Lecture Notes in Computer Science. Springer, pp 811-815 · Zbl 1279.68220
[46] Pfenning F (1996) The practice of logical frameworks. In: Kirchner H (ed) Proceedings Of The 21St International Colloquium On Trees In Algebra And Programming, CAAP 1996, volume 1059 of Lecture Notes in Computer Science. Springer, pp 119-134
[47] Pfenning F (2002) Proof and system-reliability, chapter logical frameworks—a brief introduction. Springer, pp 137-166 · Zbl 1097.68541
[48] Riesco A (2014) An integration of CafeOBJ into full Maude. In: Escobar S (ed) Proceedings of the 10th International Workshop on Rewriting Logic and Its Applications, WRLA 2014, Revised Selected Papers, volume 8663 of Lecture Notes in Computer Science. Springer, pp 230-246 · Zbl 0387.68003
[49] Rusu, V; Lucanu, D; Serbanuta, T-F; Arusoaie, A; Stefanescu, A; Rosu, G, Language definitions as rewrite theories, J Logic Algebraic Methods Programm, 85, 98-120, (2016) · Zbl 1356.68125
[50] Rocha C, Meseguer J, Muñoz CA (2014) Rewriting modulo SMT and open system analysis. In: Escobar S (ed) Proceedings of the 10th International Workshop on Rewriting Logic and Its Applications, WRLA 2014, volume 8663 of Lecture Notes in Computer Science. Springer, pp 247-262 · Zbl 1367.68151
[51] Riesco A, Ogata K, Futatsugi K (2016) CafeInMaude: a CafeOBJ interpreter in maude. In: Stevens P, Wasowski A (eds) Proceedings of the 19th International Conference on Fundamental Approaches to Software Engineering, FASE 2016, volume 9633 of Lecture Notes in Computer Science. Springer. Springer, pp 377-380
[52] Riesco, A; Verdejo, A; Martí-Oliet, N; Caballero, R, Declarative debugging of rewriting logic specifications, J Logic Algebraic Program, 81, 851-897, (2012) · Zbl 1279.68220
[53] Sawada T, Futatsugi K, Preining N (2015) CafeOBJ reference manual (version 1.5.3) · Zbl 0758.68043
[54] Verdejo, A; Martí-Oliet, N, Executable structural operational semantics in maude, J Logic Algebraic Program, 67, 226-293, (2006) · Zbl 1088.68095
[55] Zhang M, Ogata K (2009) Modular implementation of a translator from behavioral specifications to rewrite theory specifications. In: Choi B (ed) Proceedings of the 9th International Conference on Quality Software, QSIC 2009. IEEE Computer Society, pp 406-411
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.