Abstract
This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Bengtson, J., Parrow, J.: Psi-calculi in Isabelle. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2009). LNCS, vol. 5674, pp. 99–114. Springer, Berlin (2009)
Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations. In: Principles of Programming Languages (POPL’06), pp. 55–66. ACM (2006)
Blanchette, J.C., Böhme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) Conference on Automated Deduction (CADE-23). LNCS, vol. 6803, pp. 116–130. Springer, Berlin (2011)
Bourke, T.: Mechanization of the Algebra for Wireless Networks (AWN). Archive of Formal Proofs (2014). http://afp.sf.net/entries/AWN.shtml
Bourke, T., van Glabbeek, R.J., Höfner, P.: A mechanized proof of loop freedom of the (untimed) AODV routing protocol. In: Cassez, F., Raskin, J.F. (eds.) Automated Technology for Verification and Analysis (ATVA’14). LNCS, vol. 8837, pp. 47–63. Springer, Berlin (2014)
Bourke, T., van Glabbeek, R.J., Höfner, P.: Showing invariance compositionally for a process algebra for network protocols. In: Klein, G., Gamboa, R. (eds.) Interactive Theorem Proving (ITP’14). LNCS, vol. 8558, pp. 144–159. Springer, Berlin (2014)
Bourke, T., Höfner, P.: Loop Freedom of the (Untimed) Aodv Routing Protocol. Archive of Formal Proofs (2014). http://afp.sf.net/entries/AODV.shtml
Chandy K.M., Misra J.: Parallel Program Design: A Foundation. Addison Wesley, Boston (1988)
Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the TLA+ proof system. In: Giesl, J., Hähnle, R. (eds.) International Joint Conference on Automated Reasoning (IJCAR’10). LNCS, vol. 6173, pp. 142–148. Springer, Berlin (2010)
Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks. In: Seidl, H. (ed.) European Symposium on Programming (ESOP ’12). LNCS, vol. 7211, pp. 295–315. Springer, Berlin (2012)
Fehnker, A., van Glabbeek, R.J., Höfner, P., McIver, A.K., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical Report 5513, NICTA (2013). http://arxiv.org/abs/1312.7645
Feliachi, A., Gaudel, M.C., Wolff, B.: Isabelle/Circus: A process specification and verification environment. In: Joshi, R., Müller, P., Podelski, A. (eds.) Verified Software: Theories, Tools, and Experiments (VSTTE’12) LNCS, vol. 7152, pp. 243–260. Springer, Berlin (2012)
Floyd R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19–32 (1967)
Fokkink W., Groote J.F., Reniers M.: Process algebra needs proof methodology. EATCS Bull. 82, 109–125 (2004)
Ghassemi, F., Fokkink, W., Movaghar, A.: Restricted broadcast process theory. In: Cerone, A., Gruner, S. (eds.) Software Engineering and Formal Methods (SEFM ’08), pp. 345–354. IEEE Computer Society (2008)
Godskesen, J.C.: A calculus for mobile ad hoc networks. In: Murphy, A.L., Vitek, J. (eds.) Coordination Models and Languages (COORDINATION ’07) LNCS, vol. 4467, pp. 132–150. Springer, Berlin (2007)
Göthel T., Glesner S.: An approach for machine-assisted verification of timed CSP specifications. Innov. Syst. Softw. Eng. 6(3), 181–193 (2010)
Heyd, B., Crégut, P.: A modular coding of UNITY in COQ. In: Goos, G., Hartmanis, J., Leeuwen, J., Wright, J., Grundy, J., Harrison, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 1996) LNCS, vol. 1125, pp. 251–266. Springer, Berlin (1996)
Hirschkoff, D.: A full formalisation of π-calculus theory in the calculus of constructions. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2007). LNCS, vol. 4732, pp. 153–169. Springer, Berlin (2007)
Kammüller, F., Wenzel, M., Paulson, L.C.: Locales: A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 1999). LNCS, vol. 1690, pp. 149–165. Springer, Berlin (1999)
Lamport L.: Specifying Systems: The TLA + Language and Tools for Hardware and Software Engineers. Addison Wesley, Boston (2002)
Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Q. 2(3), 219–246 (1989). http://theory.lcs.mit.edu/tds/papers/Lynch/CWI89.html
Manna Z., Pnueli A.: Temporal Verification of Reactive Systems: Safety. Springer, Berlin (1995)
Merro M.: An observational theory for mobile ad hoc networks (full version). Inf. Comput. 207(2), 194–208 (2009)
Mezzetti N., Sangiorgi D.: Towards a calculus for wireless systems. Electron. Notes Theor. Comput. Sci. (ENTCS) 158, 331–353 (2006)
Milner, R.: Operational and algebraic semantics of concurrent processes. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, chap. 19, pp. 1201–1242. Elsevier Science Publishers B.V. (North-Holland) (1990). Alternatively see Communication and Concurrency, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems. LNCS 92, Springer, 1980
Müller, O.: A Verification Environment for I/O Automata Based on Formalized Meta-theory. Ph.D. Thesis, TU München (1998)
Nanz S., Hankin C.: A framework for security analysis of mobile wireless networks. Theor. Comput. Sci. 367, 203–227 (2006)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Berlin (2002)
Paulson L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6(1–2), 85–128 (1998)
Perkins, C.E., Belding-Royer, E.M., Das, S.R.: Ad hoc On-Demand Distance Vector (AODV) Routing. RFC 3561 (Experimental), Network Working Group (2003)
Plotkin, G.: A structural approach to operational semantics. J. Log. Algebr. Program. 60–61, 17–139 (2004). Originally appeared in 1981
de Roever, W.P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science 54. CUP (2001)
Singh A., Ramakrishnan C.R., Smolka S.A.: A process calculus for mobile ad hoc networks. Sci. Comput. Program. 75, 440–469 (2010)
Sutcliffe G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337–362 (2009)
Tej, H., Wolff, B.: A corrected failure divergence model for CSP in Isabelle/HOL. In: Fitzgerald, J.S., Jones, C.B., Lucas, P. (eds.) Industrial Applications and Strengthened Foundations of Formal Methods (FME’97). LNCS, vol. 1313, pp. 318–337. Springer, Berlin (1997)
Wenzel, M.: Isabelle/jEdit—a prover IDE within the PIDE framework. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) Intelligent Computer Mathematics. LNCS, vol. 7362, pp. 468–471. Springer, Berlin (2012)
Wenzel, M.: Shared-memory multiprocessing for interactive theorem proving. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving (ITP’13). LNCS, vol. 7998, pp. 418–434. Springer, Berlin (2013)
Zhou, M., Yang, H., Zhang, X., Wang, J.: The proof of AODV loop freedom. In: International Conference on Wireless Communications and Signal Processing (WCSP’09). IEEE (2009)
Author information
Authors and Affiliations
Corresponding author
Additional information
NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program.
Rights and permissions
About this article
Cite this article
Bourke, T., van Glabbeek, R.J. & Höfner, P. Mechanizing a Process Algebra for Network Protocols. J Autom Reasoning 56, 309–341 (2016). https://doi.org/10.1007/s10817-015-9358-9
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-015-9358-9