Study on OSPF Algebraic Formal Modelling Using ACP

Pedro Juan Roig, Salvador Alcaraz, Katja Gilly, Carlos Juiz


OSPF is a commonly used link state routing protocol in order to interconnect network devices inside an Autonomous System. This paper focuses on achieving a detailed modelling for OSPF by performing manual algebraic derivations according to Algebra of Communicating Processes (ACP) axioms. The aim of this detailed model is to get a realistic approach of OSPF dynamics by applying the timers involved and by describing the full Link State Advertisement (LSA) exchange process.



ACP; Formal protocol specification; Networking; OSPF.

Full Text: PDF


  • There are currently no refbacks.

Print ISSN: 1392-1215
Online ISSN: 2029-5731