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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
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)
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)
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)
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)
Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
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)
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)
Futatsugi, K., Gâinâ, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theoretical Computer Science 464, 90–112 (2012)
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)
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)
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)
Hendrix, J.: Decision Procedures for Equationally Based Reasoning. PhD thesis, University of Illinois at Urbana-Champaign (April 2008)
Lin, K., Goguen, J.: A hidden proof of the Alternating Bit Protocol, http://cseweb.ucsd.edu/~goguen/pps/abp.ps
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)
Meseguer, J.: Twenty years of rewriting logic. JLAP 81(7-8), 721–781 (2012)
Meseguer, J., Goguen, J.A.: Initially, induction and computability. Algebraic Methods in Semantics (1986)
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)
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)
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)
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)
Pnueli, A.: Deduction is forever (1999) Invited talk at FM 1999 avaliable online at cs.nyu.edu/pnueli/fm99.ps
Rocha, C.: Symbolic Reachability Analysis for Rewrite Theories. PhD thesis, University of Illinois at Urbana-Champaign (2012), http://hdl.handle.net/2142/42200
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)
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)
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)
Suzuki, I.: Formal analysis of the Alternating Bit Protocol by Temporal Petri Nets. IEEE Transactions on Software Engineering 16(11), 1273–1281 (1990)
Viry, P.: Equational rules for rewriting logic. TCS 285, 487–517 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Rocha, C., Meseguer, J. (2014). Mechanical Analysis of Reliable Communication in the Alternating Bit Protocol Using the Maude Invariant Analyzer Tool. In: Iida, S., Meseguer, J., Ogata, K. (eds) Specification, Algebra, and Software. Lecture Notes in Computer Science, vol 8373. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54624-2_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-54624-2_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54623-5
Online ISBN: 978-3-642-54624-2
eBook Packages: Computer ScienceComputer Science (R0)