@inproceedings(Ahrenholz08, author = {J. Ahrenholz and C. Danilov and T. Henderson and J. Kim}, year = {2008}, title = {{CORE:} A Real-Time Network Emulator}, doi = {10.1109/MILCOM.2008.4753614}, ) @incollection(uppaal04, author = {G. Behrmann and A. David and K. G. Larsen}, year = {2004}, title = {{A Tutorial on \textsc{Uppaal}}}, editor = {Marco Bernardo and Flavio Corradini}, booktitle = {Formal Methods for the Design of Real-Time Systems}, series = {Lecture Notes in Computer Science}, volume = {3185}, publisher = {Springer}, pages = {200--236}, doi = {10.1007/978-3-540-30080-9\_7}, ) @article(Bellman58, author = {R. Bellman}, year = {1958}, title = {On a Routing Problem}, journal = {Quarterly of Applied Mathematics}, volume = {16}, pages = {87--90}, doi = {10.1090/qam/102435}, ) @incollection(BK86, author = {J. A. Bergstra and J. W. Klop}, year = {1986}, title = {Algebra of Communicating Processes}, editor = {{de Bakker}, J. W. and M. Hazewinkel and J. K. Lenstra}, booktitle = {Mathematics and Computer Science}, series = {CWI Monograph 1}, publisher = {North-Holland}, pages = {89--138}, ) @inproceedings(BHJRVPP11, author = {J. Borgstr{\"o}m and S. Huang and M. Johansson and P. Raabjerg and B. Victor and J. {\r A} Pohjola and J. Parrow}, year = {2011}, title = {Broadcast Psi-calculi with an Application to Wireless Protocols}, editor = {G. Barthe and A. Pardo and G. Schneider}, booktitle = {Software Engineering and Formal Methods {(SEFM'11)}}, series = {Lecture Notes in Computer Science}, volume = {7041}, publisher = {Springer}, pages = {74--89}, doi = {10.1007/978-3-642-24690-6\_7}, ) @inproceedings(ESOP16, author = {E. Bres and R. van Glabbeek and P. H\"{o}fner}, year = {2016}, title = {A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract)}, editor = {P. Thiemann}, booktitle = {Programming Languages and Systems (ESOP'16)}, series = {Lecture Notes in Computer Science}, volume = {9632}, publisher = {Springer}, pages = {95--122}, doi = {10.1007/978-3-662-49498-1\_5}, ) @article(tawn_tr, author = {E. Bres and R. van Glabbeek and R. H{\"{o}}fner}, year = {2016}, title = {A Timed Process Algebra for Wireless Networks}, journal = {CoRR}, volume = {abs/1606.03663}, url = {http://arxiv.org/abs/1606.03663}, ) @inproceedings(CBMC, author = {E. Clarke and D. Kroening and F. Lerda}, year = {2004}, title = {A Tool for Checking {ANSI-C} Programs}, editor = {K. Jensen and A. Podelski}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04)}, series = {Lecture Notes in Computer Science}, volume = {2988}, publisher = {Springer}, pages = {168--176}, doi = {10.1007/978-3-540-24730-2\_15}, ) @misc(rfc5340, author = {R. Coltun and D. Ferguson and J. Moj and A. Lindem}, year = {2008}, title = {{OSPF for IPv6}}, howpublished = {RFC 5340, Network Working Group}, url = {http://www.ietf.org/rfc/rfc5340.txt}, ) @inproceedings(Z3, author = {De Moura, L. and Bj{\o}rner, N.}, year = {2008}, title = {{Z3:} An Efficient {SMT} Solver}, editor = {C. R. Ramakrishnan and J. Rehof}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08)}, series = {Lecture Notes in Computer Science}, volume = {4963}, publisher = {Springer}, pages = {337--340}, doi = {10.1007/978-3-540-78800-3\_24}, ) @article(Dijkstra59, author = {E. W. Dijkstra}, year = {1959}, title = {A Note on Two Problems in Connexion with Graphs}, journal = {Numerische Mathematik}, volume = {1}, number = {1}, pages = {269--271}, doi = {10.1007/BF01386390}, ) @inproceedings(bpi, author = {C. Ene and T. Muntean}, year = {2001}, title = {A Broadcast-based Calculus for Communicating Systems}, booktitle = {Parallel {\&} Distributed Processing Symposium {(IPDPS '01)}}, publisher = {IEEE Computer Society}, pages = {1516--1525}, doi = {10.1109/IPDPS.2001.925136}, ) @conference(TACAS12, author = {A. Fehnker and R. J. van Glabbeek and P H{\"o}fner and A. K. McIver and M. Portmann and W. L. Tan}, year = {2012}, title = {Automated Analysis of {AODV} using {UPPAAL}}, editor = {C. Flanagan and B. K{\"onig}}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems {(TACAS '12)}}, series = {Lecture Notes in Computer Science}, volume = {7214}, publisher = {Springer}, pages = {173--187}, doi = {10.1007/978-3-642-28756-5\_13}, ) @inproceedings(ESOP12, author = {A. Fehnker and R. J. van Glabbeek and P. H{\"o}fner and A. K. McIver and M. Portmann and W. L. Tan}, year = {2012}, title = {A Process Algebra for Wireless Mesh Networks}, editor = {H. Seidl}, booktitle = {European Symposium on Programming {\rm (ESOP '12)}}, series = {Lecture Notes in Computer Science}, volume = {7211}, publisher = {Springer}, pages = {295--315}, doi = {10.1007/978-3-642-28869-2\_15}, ) @misc(TR13, author = {A. Fehnker and R. J. van Glabbeek and P. H\"{o}fner and A. K. McIver and M. Portmann and W. L. Tan}, year = {2013}, title = {A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing {AODV}}, url = {http://arxiv.org/abs/1312.7645}, ) @techreport(Ford56, author = {Ford Jr., L. R.}, year = {1956}, title = {Network Flow Theory}, type = {Technical Report}, number = {Paper P-923}, institution = {The RAND Corporation}, ) @inproceedings(RBPT, author = {F. Ghassemi and W. Fokkink and A. Movaghar}, year = {2008}, title = {Restricted Broadcast Process Theory}, editor = {A. Cerone and S. Gruner}, booktitle = {Software Engineering and Formal Methods {(SEFM '08)}}, publisher = {IEEE Computer Society}, pages = {345--354}, doi = {10.1109/SEFM.2008.25}, ) @inproceedings(MARS17, author = {R. J. van Glabbeek and P. H\"ofner}, year = {2017}, title = {Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack}, editor = {H. Hermanns and P. H\"ofner}, booktitle = {Models for Formal Analysis of Real Systems (MARS'17)}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {244}, publisher = {Open Publishing Association}, pages = {14--52}, doi = {10.4204/EPTCS.244.2}, ) @inproceedings(MSWIM13, author = {R. J. van Glabbeek and P. H{\"o}fner and W. L. Tan and M. Portmann}, year = {2013}, title = {Sequence Numbers Do Not Guarantee Loop Freedom ---{AODV} Can Yield Routing Loops---}, booktitle = {Modeling, Analysis and Simulation of Wireless and Mobile Systems {(MSWiM '13)}}, publisher = {ACM}, pages = {91--100}, doi = {10.1145/2507924.2507943}, ) @article(DIST16, author = {R. J. van Glabbeek and P. H{\"o}fner and M. Portmann and W.L. Tan}, year = {2016}, title = {Modelling and Verifying the {AODV} Routing Protocol}, journal = {Distributed Computing}, volume = {29}, number = {4}, pages = {279--315}, doi = {10.1007/s00446-015-0262-7}, ) @inproceedings(CMAN, author = {J. C. Godskesen}, year = {2007}, title = {A Calculus for Mobile Ad Hoc Networks}, editor = {A. L. Murphy and J. Vitek}, booktitle = {Coordination Models and Languages {(COORDINATION '07)}}, series = {Lecture Notes in Computer Science}, volume = {4467}, publisher = {Springer}, pages = {132--150}, doi = {10.1007/978-3-540-72794-1\_8}, ) @inproceedings(bApi, author = {J. C. Godskesen}, year = {2010}, title = {Observables for Mobile and Wireless Broadcasting Systems}, editor = {D. Clarke and G. A. Agha}, booktitle = {Coordination Models and Languages {(COORDINATION '10)}}, series = {Lecture Notes in Computer Science}, volume = {6116}, publisher = {Springer}, pages = {1--15}, doi = {10.1007/978-3-642-13414-2\_1}, ) @book(Ho85, author = {C. A. R. Hoare}, year = {1985}, title = {Communicating Sequential Processes}, publisher = {Prentice Hall}, address = {Englewood Cliffs}, ) @misc(IEEE80211, author = {{ISO/IEC/IEEE 8802-11}}, year = {2018}, title = {Information Technology --- Telecommunications and information exchange between systems --- Local and metropolitan area networks --- Specific requirements --- Part 11: Wireless {LAN} Medium Access Control {(MAC)} and Physical Layer {(PHY)} specifications}, url = {https://www.iso.org/standard/73367.html}, ) @article(LPY97, author = {K. G. Larsen and P. Pettersson and {Wang Yi}}, year = {1997}, title = {{UPPAAL} in a Nutshell}, journal = {International Journal of Software Tools for Technology Transfer}, volume = {1}, number = {1-2}, pages = {134--152}, doi = {10.1007/s100090050010}, ) @misc(Malik, author = {S.U.R Malik and S. K. Srinivasan and S. U. Khan}, year = {2012}, title = {A Methodology for {OSPF} Routing Protocol Verification}, ) @article(CMN, author = {M. Merro}, year = {2009}, title = {An Observational Theory for Mobile Ad Hoc Networks (full version)}, journal = {Information and Computation}, volume = {207}, number = {2}, pages = {194--208}, doi = {10.1016/j.ic.2007.11.010}, ) @article(CWS, author = {N. Mezzetti and D. Sangiorgi}, year = {2006}, title = {Towards a Calculus For Wireless Systems}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {158}, pages = {331--353}, doi = {10.1016/j.entcs.2006.04.017}, ) @book(Mi80, author = {R. Milner}, year = {1980}, title = {A Calculus of Communicating Systems}, series = {Lecture Notes in Computer Science}, volume = {92}, publisher = {Springer}, doi = {10.1007/3-540-10235-3}, ) @book(Mi89, author = {R. Milner}, year = {1989}, title = {Communication and Concurrency}, publisher = {Prentice Hall}, address = {Englewood Cliffs}, ) @inproceedings(MK10, author = {S. Miskovic and E. W. Knightly}, year = {2010}, title = {Routing Primitives for Wireless Mesh Networks: Design, Analysis and Experiments}, booktitle = {INFOCOM'10}, publisher = {IEEE}, pages = {2793--2801}, doi = {10.1109/INFCOM.2010.5462111}, ) @mastersthesis(Moehring17, author = {K. M{\"o}hring}, year = {2017}, title = {Transformation of {AWN} Protocol Specifications to the {Uppaal} Model Checker}, type = {{Bachelor Thesis}}, school = {Universit{\"a}t Hamburg and Data61, CSIRO}, ) @misc(rfc2328, author = {J. Moj}, year = {1998}, title = {{OSPF Version 2}}, howpublished = {RFC 2328, Network Working Group}, url = {http://www.ietf.org/rfc/rfc2328.txt}, ) @techreport(Moore57, author = {E. F. Moore}, year = {1957}, title = {The Shortest Path Through a Maze}, type = {Technical Report}, institution = {Bell Telephone System}, ) @inproceedings(NakiblyEtAl14, author = {G. Nakibly and A. Sosnovich and E. Menahem and A. Waizel and Y. Elovici}, year = {2014}, title = {OSPF Vulnerability to Persistent Poisoning Attacks: A Systematic Analysis}, booktitle = {Computer Security Applications Conference}, series = {ACSAC '14}, publisher = {ACM}, pages = {336--345}, doi = {10.1145/2664243.2664278}, ) @article(NH06, author = {S. Nanz and C. Hankin}, year = {2006}, title = {A Framework for Security Analysis of Mobile Wireless Networks}, journal = {Theoretical Computer Science}, volume = {367}, pages = {203--227}, doi = {10.1016/j.tcs.2006.08.036}, ) @inproceedings(CBS91, author = {K. V. S. Prasad}, year = {1991}, title = {A Calculus of Broadcasting Systems}, editor = {S. Abramsky and T. S. E. Maibaum}, booktitle = {Theory and Practice of Software Development {(TAPSOFT '91)}}, series = {Lecture Notes in Computer Science}, volume = {493}, publisher = {Springer}, pages = {338--358}, doi = {10.1007/3-540-53982-4\_19}, ) @article(CBS, author = {K. V. S. Prasad}, year = {1995}, title = {A Calculus of Broadcasting Systems}, journal = {Science of Computer Programming}, volume = {25}, number = {2-3}, pages = {285--327}, doi = {10.1016/0167-6423(95)00017-8}, ) @inproceedings(Shimbel55, author = {A. Shimbel}, year = {1955}, title = {Structure in Communication Nets}, booktitle = {Symposium on Information Networks}, publisher = {Polytechnic Press of the Polytechnic Institute of Brooklyn}, pages = {199--203}, ) @article(SRS10, author = {A. Singh and C. R. Ramakrishnan and S. A. Smolka}, year = {2010}, title = {A process calculus for Mobile Ad Hoc Networks}, journal = {Science of Computer Programming}, volume = {75}, pages = {440--469}, doi = {10.1016/j.scico.2009.07.008}, ) @article(VaradhanetAl00, author = {K. Varadhan and R. Govindan and D. Estrin}, year = {2000}, title = {Persistent Route Oscillations in Inter-domain Routing}, journal = {Computer Networks}, volume = {32}, number = {1}, pages = {1--16}, doi = {10.1016/S1389-1286(99)00108-5}, ) @inproceedings(Zave11, author = {P. Zave}, year = {2011}, title = {Experiences with Protocol Description}, booktitle = {Workshop on Rigorous Protocol Engineering (W-RiPE'11)}, )