Formal Models of the OSPF Routing Protocol
Copyright policy )Formal Models of the OSPF Routing Protocol
We present three formal models of the OSPF routing protocol. The first two are formalised in the timed process algebra T-AWN, which is not only tailored to routing protocols, but also specifies protocols in pseudo-code that is easily readable. The difference between the two models lies in the level of detail (level of abstraction). From the more abstract model we then generate the third model. It is based on networks of timed automata and can be executed in the model checker Uppaal.
In Proceedings MARS 2020, arXiv:2004.12403
- CSIRO Australia
- Australian National University Australia
- Commonwealth Scientific and Industrial Research Organisation Australia
Computer Science - Networking and Internet Architecture, Networking and Internet Architecture (cs.NI), FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Logic in Computer Science (cs.LO)
Computer Science - Networking and Internet Architecture, Networking and Internet Architecture (cs.NI), FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Logic in Computer Science (cs.LO)
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).1 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!