Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool

Rocha, Camilo; Meseguer, José

dc.contributor.author	Rocha, Camilo
dc.contributor.author	Meseguer, José
dc.date.accessioned	2021-12-01T20:41:59Z
dc.date.available	2021-12-01T20:41:59Z
dc.date.issued	2014
dc.identifier.isbn	9783642546242
dc.identifier.isbn	9783642546235
dc.identifier.uri	https://repositorio.escuelaing.edu.co/handle/001/1882
dc.description.abstract	The InvA tool supports the deductive verification of safety properties of infinite-state concurrent systems. Given a concurrent system specified as a rewrite theory and a safety formula to be verified, InvA reduces such a formula to inductive properties of the underlying equational theory by means of the application of a few inference rules. Through the combination of various techniques such as unification, narrowing, equationally-defined equality predicates, and SMT solving, InvA achieves a significant degree of automation, verifying automatically many proof obligations. Maude Inductive Theorem Prover (ITP) can be used to discharge the remaining obligations which are not automatically verified by InvA. Verification of the reliable communication ensured by the Alternating Bit Protocol (ABP) is used as a case study to explain the use of the InvA tool, and to illustrate its effectiveness and degree of automation in a concrete way.	eng
dc.description.abstract	La herramienta InvA admite la verificación deductiva de las propiedades de seguridad de los sistemas concurrentes de estado infinito. Dado un sistema concurrente especificado como una teoría de reescritura y una fórmula de seguridad a verificar, InvA reduce dicha fórmula a las propiedades inductivas de la teoría ecuacional subyacente mediante la aplicación de algunas reglas de inferencia. A través de la combinación de varias técnicas, como la unificación, el estrechamiento, los predicados de igualdad definidos por ecuaciones y la resolución SMT, InvA logra un grado significativo de automatización, verificando automáticamente muchas obligaciones de prueba. El probador del teorema inductivo de Maude (ITP) se puede utilizar para cumplir con las obligaciones restantes que InvA no verifica automáticamente. La verificación de la comunicación confiable asegurada por el Alternating Bit Protocol (ABP) se utiliza como caso de estudio para explicar el uso de la herramienta InvA, y para ilustrar su efectividad y grado de automatización de manera concreta.
dc.format.extent	27 páginas.	spa
dc.format.mimetype	application/pdf	spa
dc.language.iso	eng	spa
dc.publisher	Springer.	spa
dc.relation.ispartofseries	Lecture Notes in Computer Science;8373
dc.rights	© Springer-Verlag Berlin Heidelberg 2014	eng
dc.rights.uri	https://creativecommons.org/licenses/by/4.0/	spa
dc.title	Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool	eng
dc.type	Capítulo - Parte de Libro	spa
dc.type.version	info:eu-repo/semantics/publishedVersion	spa
oaire.accessrights	http://purl.org/coar/access_right/c_14cb	spa
oaire.version	http://purl.org/coar/version/c_970fb48d4fbd8a85	spa
dc.contributor.researchgroup	Informática	spa
dc.relation.citationendpage	629	spa
dc.relation.citationstartpage	603	spa
dc.relation.indexed	N/A	spa
dc.relation.ispartofbook	Specification, Algebra, and Software	eng
dc.relation.references	Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) 24th International Conference on Rewriting Techniques and Applications, RTA 2013, Eindhoven, The Netherlands, June 24-26. LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)	spa
dc.relation.references	Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commununications of the ACM 12(5), 260–261 (1969)	spa
dc.relation.references	Bergstra, J., Klop, J.: Verification of an Alternating Bit Protocol by means of process algebra protocol. In: Bibel, W., Jantke, K. (eds.) Mathematical Methods of Specification and Synthesis of Software Systems 1985. LNCS, vol. 215, pp. 9–23. Springer, Heidelberg (1986)	spa
dc.relation.references	Bezem, M., Groote, J.F.: Invariants in process algebra with data. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 401–416. Springer, Heidelberg (1994)	spa
dc.relation.references	Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)	spa
dc.relation.references	Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)	spa
dc.relation.references	Clavel, M., Egea, M.: ITP/OCL: A rewriting-based validation tool for UML+OCL static class diagrams. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 368–373. Springer, Heidelberg (2006)	spa
dc.relation.references	Durán, F., Meseguer, J.: A Church-Rosser checker tool for conditional order-sorted equational maude specifications. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 69–85. Springer, Heidelberg (2010)	spa
dc.relation.references	Futatsugi, K., Gâinâ, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theoretical Computer Science 464, 90–112 (2012)	spa
dc.relation.references	Găină, D., Zhang, M., Chiba, Y., Arimoto, Y.: Constructor-based inductive theorem prover. In: Heckel, R. (ed.) CALCO 2013. LNCS, vol. 8089, pp. 328–333. Springer, Heidelberg (2013)	spa
dc.relation.references	Giménez, E.: An application of co-inductive types in Coq: Verification of the Alternating Bit Protocol. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 135–152. Springer, Heidelberg (1996)	spa
dc.relation.references	Gutiérrez, R., Meseguer, J., Rocha, C.: Order-sorted equality enrichments modulo axioms. In: Durán, F. (ed.) WRLA 2012. LNCS, vol. 7571, pp. 162–181. Springer, Heidelberg (2012)	spa
dc.relation.references	Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign (April 2008)	spa
dc.relation.references	Lin, K., Goguen, J.: A hidden proof of the Alternating Bit Protocol,	spa
dc.relation.references	Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)	spa
dc.relation.references	Meseguer, J.: Twenty years of rewriting logic. JLAP 81(7-8), 721–781 (2012)	spa
dc.relation.references	Meseguer, J., Goguen, J.A.: Initially, induction and computability. Algebraic Methods in Semantics (1986)	spa
dc.relation.references	Nakano, M., Ogata, K., Nakamura, M., Futatsugi, K.: Crème: an automatic invariant prover of behavioral specifications. International Journal of Software Engineering and Knowledge Engineering 17(6), 783–804 (2007)	spa
dc.relation.references	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)	spa
dc.relation.references	Ogata, K., Futatsugi, K.: Simulation-based verification for invariant properties in the OTS/CafeOBJ method. Electronic Notes in Theorethical Computer Science 201, 127–154 (2008)	spa
dc.relation.references	Ogata, K., Futatsugi, K.: Proof score approach to analysis of electronic commerce protocols. International Journal of Software Engineering and Knowledge Engineering 20(2), 253–287 (2010)\|	spa
dc.relation.references	Pnueli, A.: Deduction is forever (1999) Invited talk at FM 1999 avaliable online at cs.nyu.edu/pnueli/fm99.ps	spa
dc.relation.references	Rocha, C.: Symbolic Reachability Analysis for Rewrite Theories. PhD thesis, University of Illinois at Urbana-Champaign (2012), http://hdl.handle.net/2142/42200	spa
dc.relation.references	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)	spa
dc.relation.references	Roşu, G., Ştefănescu, A.: Matching Logic: A New Program Verification Approach (NIER Track). In: ICSE 211: Proceedings of the 30th International Conference on Software Engineering, pp. 868–871. ACM (2011)	spa
dc.relation.references	Steggles, L., Kosiuczenko, P.: A timed rewriting logic semantics for SDL: A case study of the Alternating Bit Protocol. Electronic Notes in Theoretical Computer Science 15, 83–104 (1998)	spa
dc.relation.references	Suzuki, I.: Formal analysis of the Alternating Bit Protocol by Temporal Petri Nets. IEEE Transactions on Software Engineering 16(11), 1273–1281 (1990)	spa
dc.relation.references	Viry, P.: Equational rules for rewriting logic. TCS 285, 487–517 (2002)	spa
dc.rights.accessrights	info:eu-repo/semantics/closedAccess	spa
dc.rights.creativecommons	Atribución 4.0 Internacional (CC BY 4.0)	spa
dc.subject.armarc	Comprobación del modelo	SPA
dc.subject.armarc	Regla de inferencia	SPA
dc.subject.armarc	Propiedad de seguridad	SPA
dc.subject.armarc	Flujo de entrada	SPA
dc.subject.armarc	Obligación de prueba	SPA
dc.subject.proposal	Model Check	eng
dc.subject.proposal	Inference Rule	eng
dc.subject.proposal	Safety Property	eng
dc.subject.proposal	Input Stream	eng
dc.subject.proposal	Proof Obligation	eng
dc.type.coar	http://purl.org/coar/resource_type/c_3248	spa
dc.type.content	Text	spa
dc.type.driver	info:eu-repo/semantics/bookPart	spa
dc.type.redcol	http://purl.org/redcol/resource_type/ART	spa