J. Ahrenholz, C. Danilov, T. Henderson & J. Kim (2008):
CORE: A Real-Time Network Emulator.
In: IEEE Military Communications Conference, MILCOM'08,
doi:10.1109/MILCOM.2008.4753614.
G. Behrmann, A. David & K. G. Larsen (2004):
A Tutorial on Uppaal.
In: Marco Bernardo & Flavio Corradini: Formal Methods for the Design of Real-Time Systems,
Lecture Notes in Computer Science 3185.
Springer,
pp. 200–236,
doi:10.1007/978-3-540-30080-9_7.
Karthikeyan Bhargavan, Davor Obradovic & Carl A. Gunter (2002):
Formal Verification of Standards for Distance Vector Routing Protocols.
J. ACM 49(4),
pp. 538–576,
doi:10.1145/581771.581775.
B. Blanchet (2016):
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif.
Foundations and Trends in Privacy and Security 1(1-2),
pp. 1–135,
doi:10.1561/3300000004.
E. Bres, R. van Glabbeek & P. Höfner (2016):
A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract).
In: P. Thiemann: Programming Languages and Systems (ESOP'16),
Lecture Notes in Computer Science 9632.
Springer,
pp. 95–122,
doi:10.1007/978-3-662-49498-1_5.
E. Clarke, D. Kroening & F. Lerda (2004):
A Tool for Checking ANSI-C Programs.
In: K. Jensen & A. Podelski: Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04),
Lecture Notes in Computer Science 2988.
Springer,
pp. 168–176,
doi:10.1007/978-3-540-24730-2_15.
R. Coltun, D. Ferguson, J. Moy & A. Lindem (2008):
OSPF for IPv6.
RFC 5340, Network Working Group.
Available at http://www.ietf.org/rfc/rfc5340.txt.
L. De Moura & N. Bjørner (2008):
Z3: An Efficient SMT Solver.
In: C. R. Ramakrishnan & J. Rehof: Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08),
Lecture Notes in Computer Science 4963.
Springer,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
E. W. Dijkstra (1959):
A Note on Two Problems in Connexion with Graphs.
Numerische Mathematik 1(1),
pp. 269–271,
doi:10.1007/BF01386390.
J. Drury, P. Höfner & W. Wang (2020):
Formal Models of the OSPF Routing Protocol.
In: A. Fehnker & H. Garavel: Models for Formal Analysis of Real Systems (MARS'20),
Electronic Proceedings in Theoretical Computer Science 316.
Open Publishing Association,
pp. 72–120,
doi:10.4204/EPTCS.316.4.
E. A. Emerson (1990):
Temporal and Modal Logic.
In: Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics.
MIT Press,
pp. 995–1072,
doi:10.1016/B978-0-444-88074-1.50021-4.
A. Fehnker, R. J. van Glabbeek, P Höfner, A. K. McIver, M. Portmann & W. L. Tan (2012):
Automated Analysis of AODV using UPPAAL.
In: C. Flanagan & B. König: Tools and Algorithms for the Construction and Analysis of Systems (TACAS '12),
Lecture Notes in Computer Science 7214.
Springer,
pp. 173–187,
doi:10.1007/978-3-642-28756-5_13.
A. Fehnker, L. van Hoesel & A. Mader (2007):
Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks.
In: Integrated Formal Methods, IFM'07,
Lecture Notes in Computer Science 4591.
Springer,
pp. 253–272,
doi:10.1007/978-3-540-73210-5_14.
R. J. van Glabbeek, P. Höfner, W. L. Tan & M. Portmann (2013):
Sequence Numbers Do Not Guarantee Loop Freedom —AODV Can Yield Routing Loops—.
In: Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM '13).
ACM,
pp. 91–100,
doi:10.1145/2507924.2507943.
K. Havelund, K. G. Larsen & A. Skou (1999):
Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal.
In: J.-P. Katoen: Formal Methods for Real-Time and Probabilistic Systems (ARTS'99),
Lecture Notes in Computer Science 1601.
Springer,
pp. 277–298,
doi:10.1007/3-540-48778-6_17.
ISO/IEC/IEEE 8802-11 (2018):
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.
Available at https://www.iso.org/standard/73367.html.
K. G. Larsen, P. Pettersson & Wang Yi (1997):
UPPAAL in a Nutshell.
International Journal of Software Tools for Technology Transfer 1(1-2),
pp. 134–152,
doi:10.1007/s100090050010.
S.U.R Malik, S. K. Srinivasan & S. U. Khan (2012):
A Methodology for OSPF Routing Protocol Verification.
S. Meier, B. Schmidt, C. Cremers & D. Basin (2013):
The TAMARIN Prover for the Symbolic Analysis of Security Protocols.
In: N. Sharygina & H. Veith: Computer Aided Verification (CAV'13),
Lecture Notes in Computer Science 8044.
Springer,
pp. 696–701,
doi:10.1007/978-3-642-39799-8_48.
S. Miskovic & E. W. Knightly (2010):
Routing Primitives for Wireless Mesh Networks: Design, Analysis and Experiments.
In: INFOCOM'10.
IEEE,
pp. 2793–2801,
doi:10.1109/INFCOM.2010.5462111.
G. Nakibly, D. Gonikman, A. Kirshon & D. Boneh (2012):
Persistent OSPF Attacks.
G. Nakibly, A. Sosnovich, E. Menahem, A. Waizel & Y. Elovici (2014):
OSPF Vulnerability to Persistent Poisoning Attacks: A Systematic Analysis.
In: Computer Security Applications Conference,
ACSAC '14.
ACM,
pp. 336–345,
doi:10.1145/2664243.2664278.
R. de Renesse & A.H. Aghvami (2004):
Formal Verification of Ad Hoc Routing Protocols Using SPIN Model Checker.
In: IEEE MELECON'04.
IEEE,
pp. 1177 – 1182,
doi:10.1109/MELCON.2004.1348275.
O. Wibling, J. Parrow & A. N. Pears (2004):
Automatized Verification of Ad Hoc Routing Protocols.
In: Formal Techniques for Networked and Distributed Systems, FORTE'04,
Lecture Notes in Computer Science 3235.
Springer,
pp. 343–358,
doi:10.1007/978-3-540-30232-2_22.