Reliable Restricted Process Theory

• Autorzy: Ghassemi Fatemeh , Fokkink Wan

Identyfikatory

DOI

10.3233/FI-2019-1775

• Języki publikacji: EN

Abstrakty

EN

Malfunctions of a mobile ad hoc network (MANET) protocol caused by a conceptual mistake in the protocol design, rather than unreliable communication, can often be detected only by considering communication among the nodes in the network to be reliable. In Restricted Broadcast Process Theory, which was developed for the specification and verification of MANET protocols, the communication operator is lossy. Replacing unreliable with reliable communication invalidates existing results for this process theory. We examine the effects of this adaptation on the semantics of the framework with regard to the non-blocking property of communication in MANETs, the notion of behavioral equivalence relation and its axiomatization. To utilize our complete axiomatization for analyzing the correctness of protocols at the syntactic level, we introduce a precongruence relation which abstracts away from a sequence of multi-hop communications, leading to an application-level action preconditioned by a multi-hop constraint over the topology. We illustrate the applicability of our framework through a simple routing protocol. To prove its correctness, we introduce a novel proof process, based on our precongruence relation.

Słowa kluczowe

EN

behavioral congruence; mobile ad hoc network; process algebra; refinement; restricted broadcast

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 165, nr 1
• Strony: 1--41
• Opis fizyczny: Bibliogr. 51 poz., tab.

Twórcy

autor

Ghassemi Fatemeh

• University of Tehran, Tehran, Iran

autor

Fokkink Wan

• Vrije Universiteit Amsterdam, Amsterdam, The Netherlands

Bibliografia

• [1] Baeten J, Bravetti M. A ground-complete axiomatization of finite state processes in process algebra, Proc. 16th Conference on Concurrency Theory, 3653, Springer, 2005, ISBN 3-540-28309-9.
• [2] Basten T. Branching bisimilarity is an equivalence indeed!, Information Processing Letters, 1996; 58(3):141-147. URL https://doi.org/10.1016/0020-0190(96)00034-8.
• [3] Bengtson J, Johansson M, Parrow J, Victor B. Psi-calculi: Mobile processes, nominal data, and logic, Proc. 24th Annual IEEE Symposium on Logic in Computer Science, IEEE, 2009, ISBN 978-0-7695-3746-7.
• [4] Bergstra J, Klop JW. Process algebra for synchronous communication, Information and Control, 1984;60(1-3):109-137. URL https://doi.org/10.1016/S0019-9958(84)80025-X.
• [5] Bezem M, Groote JF. Invariants in process algebra with data, Proc. 5th Conference of Concurrency Theory, 836, Springer, 1994, ISBN 3-540-58329-7.
• [6] Bhargavan K, Obradovid D, Gunter CA. Formal verification of standards for distance vector routing protocols, Journal of the ACM, 2002;49(4):538-576. doi:10.1145/581771.581775.
• [7] Borgström J, Huang S, Johansson M, Raabjerg P, Victor B, Pohjola J Å , Parrow J. Broadcast psicalculi with an application to wireless protocols, Software and System Modeling, 2015;14(1):201-216. doi:10.1007/s10270-013-0375-z.
• [8] Bourke T, van Glabbeek RJ, Höfner P. A mechanized proof of loop freedom of the (untimed) AODV routing protocol, Proc. 12th Symposium on Automated Technology for Verification and Analysis, 8837, Springer, 2014, ISBN 978-3-319-11935-9.
• [9] Bourke T, van Glabbeek RJ, Höfner P. Showing invariance compositionally for a process algebra for network protocols, Proc. 5th Conference on Interactive Theorem Proving, 8558, Springer, 2014, ISBN 978-3-319-08969-0.
• [10] Bres, E., van Glabbeek, R. J., Höfner, P.: A timed process algebra for wireless networks with an application in routing (extended abstract), Proc. 25th European Symposium on Programming, 9632, Springer, 2016, ISBN 978-3-662-49497-4.
• [11] Chiyangwa S, Kwiatkowska M. A timing analysis of AODV, Proc. 7th IFIP Conference on Formal Methods for Open Object-based Distributed Systems, 3535, Springer, 2005, ISBN 3-540-26181-8.
• [12] Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching-time temporal logic, Proc. Workshop on Logic of Programs, 131, Springer, 1981, ISBN 3-540-11212-X.
• [13] Ehrich H, Loeckx J, Wolf M. Specification of Abstract Data Types, John Wiley, 1996, ISBN 978-0-471-95067-7.
• [14] Fall KR, Stevens WR. TCP/IP Illustrated, vol. 1, Addison-Wesley, 2011, ISBN 0-13-280818-8.
• [15] Fehnker A, van Glabbeek RJ, Höfner P, McIver A, Portmann, M, Tan WL. Automated analysis of AODV using UPPAAL, Proc. 18th Conference on Tools and Algorithms for the Construction and Analysis of Systems, 7214, Springer, 2012, ISBN 978-3-642-28755-8.
• [16] Fehnker A, van Glabbeek RJ, Höfner P, McIver A, Portmann M, Tan WL. A process algebra for wireless mesh networks, Proc. 21st European Symposium on Programming, 7211, Springer, 2012, ISBN 978-3-642-28868-5.
• [17] Fokkink WJ, Pang J, van de Pol JC. Cones and foci: A mechanical framework for protocol verification, Formal Methods in System Design, 2006;29(1):1-31. doi:10.1007/s10703-006-0004-3.
• [18] Ghassemi F, Fokkink WJ. Model checking mobile ad hoc networks, Formal Methods in System Design, 2016;48(1-2):159-189. doi:10.1007/s10703-016-0254-7.
• [19] Ghassemi F, Fokkink WJ, Movaghar A. Restricted broadcast process theory, Proc. 6th Conference on Software Engineering and Formal Methods, IEEE, 2008, ISBN 978-0-7695-3437-4.
• [20] Ghassemi F, Fokkink WJ, Movaghar A. Equational reasoning on ad hoc networks, Proc. 3rd Conference on Fundamentals of Software Engineering, 5961, Springer, 2009, ISBN 978-3-642-11622-3.
• [21] Ghassemi F, Fokkink WJ, Movaghar A. Equational reasoning on mobile ad hoc networks, Fundamenta Informaticae, 2010;105(4):375-415.
• [22] Ghassemi F, Fokkink WJ, Movaghar A. Verification of mobile ad hoc networks: An algebraic approach, Theoretical Computer Science, 2011;412(28):3262-3282. URL https://doi.org/10.1016/j.tcs.2011.03.017.
• [23] van Glabbeek RJ, Höfner P, Portmann M, Tan WL. Modelling and verifying the AODV routing protocol, Distributed Computing, 2016;29(4):279-315. doi:10.1007/s00446-015-0262-7.
• [24] Godskesen J. A calculus for mobile ad hoc networks, Proc. 9th Conference on Coordination Models and Languages, 4467, Springer, 2007, ISBN 978-3-540-72793-4.
• [25] Godskesen J. A calculus for mobile ad-hoc networks with static location binding, Proc. 15th Workshop on Expressiveness in Concurrency, 2009;242(1):161-183. doi:10.1016/j.entcs.2009.06.018.
• [26] Godskesen J, Gryn O. Modeling and verification of security protocols for ad hoc networks using UPPAAL, Proc. 18-th Nordic Workshop on Programming Theory, 2006.
• [27] Godskesen J, Nanz S. Mobility models and behavioural equivalence for wireless networks, Proc. 11th Conference on Coordination Models and Languages, 5521, Springer, 2009, ISBN 978-3-642-02052-0.
• [28] Groote JF, Mathijssen A, Reniers M, Usenko Y, van Weerdenburg M. The formal specification language mCRL2, Methods for Modelling Software Systems, 06351, Schloss Dagstuhl, 2006, ISSN 1862-4405.
• [29] Groote JF, Ponse A. μCRL: A base for analysing processes with data, Proc. 3rd Workshop on Concurrency and Compositionality, GMD-Studien Nr. 191, 1991.
• [30] Groote JF, Ponse A. Syntax and semantics of μCRL, Proc. Workshop on Algebra of Communicating Processes, Workshops in Computing, Springer, 1995, ISBN 978-3-540-19909-0.
• [31] Groote JF, Springintveld J. Focus points and convergent process operators: A proof strategy for protocol verification, Journal of Logic and Algebraic Programming, 2001;49(1-2):31-60. URL https://doi.org/10.1016/S1567-8326(01)00010-8.
• [32] Groote JF, van Wamel J. The parallel composition of uniform processes with data, Theoretical Computer Science, 2001;266(1-2):631-652. URL https://doi.org/10.1016/S0304-3975(00)00324-8.
• [33] Höfner P, van Glabbeek RJ, Tan WL, Portmann M, McIver A, Fehnker A. A rigorous analysis of AODV and its variants, The 15th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems, ACM, 2012, ISBN 978-1-4503-1628-6.
• [34] Kouzapas D, Philippou A. A process calculus for dynamic networks, Proc. Conference on Formal Techniques for Distributed Systems, 6722, Springer, 2011, ISBN 978-3-642-21460-8.
• [35] Luttik B. https://doi.org/10.1016/S0304-3975(00)00324-8, Ph.D. Thesis, University of Amsterdam, 2002.
• [36] McIver A, Fehnker A. Formal techniques for analysis of wireless networks, Proc. 2nd Symposium on Leveraging Applications of Formal Methods, IEEE, 2006, ISBN 978-0-7695-3071-0.
• [37] Merro M. An observational theory for mobile ad hoc networks, Information and Computation, 2009;207(2):194-208. URL https://doi.org/10.1016/j.ic.2007.11.010.
• [38] Merro M, Ballardin F, Sibilio EA. A timed calculus for wireless systems, Theoretical Computer Science, 2011;412(47):6585-6611. URL https://doi.org/10.1016/j.tcs.2011.07.016.
• [39] Mezzetti N, Sangiorgi D. Towards a calculus for wireless systems, Proc. 22nd Conference on Mathematical Foundations of Programming Semantics, 2006;158:331-353. URL https://doi.org/10.1016/j.entcs.2006.04.017.
• [40] Namjoshi KS, Trefler RJ. Loop freedom in AODVv2, Proc. 35th IFIP Conference on Formal Techniques for Distributed Objects, Components, and Systems, 9039, 2015, ISBN 978-3-319-19194-2.
• [41] Nanz S, Hankin C. A framework for security analysis of mobile wireless networks, Theoretical Computer Science, 2006;367(1-2):203-227. URL Aframeworkforsecurityanalysisofmobilewirelessnetworks,.
• [42] Nanz S, Nielson F, Nielson H. Static analysis of topology-dependent broadcast networks, Information and Computation, 2010;208(2):117-139. doi:10.1016/j.ic.2009.10.003.
• [43] Perkins CE, Belding-Royer EM. Ad-hoc on-demand distance vector routing, Proc. 2nd Workshop on Mobile Computing Systems and Applications, IEEE, 1999, ISBN 0-7695-0025-0.
• [44] Plotkin GD. A structural approach to operational semantics, Journal of Logic and Algebraic Programming, 2004;60-61:17-139. doi:10.1016/j.jlap.2004.05.001.
• [45] Prasad KVS. A calculus of broadcasting systems, Science of Computer Programming, 1995;25(2-3):285-327. URL https://doi.org/10.1016/0167-6423(95)00017-8.
• [46] de Renesse R, Aghvami AH. Formal verification of ad-hoc routing protocols using SPIN model checker, Proc. 12th Mediterranean Electrotechnical Conference, IEEE, 2004, ISBN 0-7803-8271-4.
• [47] Singh A, Ramakrishnan CR, Smolka SA. A process calculus for mobile ad hoc networks, Science of Computer Programming, 2010;75(6):440-469. URL https://doi.org/10.1016/j.scico.2009.07. 008.
• [48] Usenko Y. Linearization in μCRL, Ph.D. Thesis, Eindhoven University of Technology, 2002.
• [49] Wibling O, Parrow J, Pears A. Automatized verification of ad hoc routing protocols, Proc. 24th IFIP Conference on Formal Techniques for Networked and Distributed Systems, 3235, Springer, 2004. doi:10.1007/978-3-540-30232-2_22.
• [50] Wibling O, Parrow J, Pears A. Ad hoc routing protocol verification through broadcast abstraction, Proc. 25th IFIP Conference on Formal Techniques for Networked and Distributed Systems, 3731, Springer, 2005, ISBN 3-540-29189-X.
• [51] Yousefi B, Ghassemi F, Khosravi R. Modeling and efficient verification of wireless ad hoc networks, Formal Aspect of Computing, 2017;29(6):1051-1086. doi:10.1007/s00165-017-0429-z.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).