Formal models of the OSPF routing protocol

Jack Drury; Peter Höfner; Weiyou Wang

doi:10.4204/EPTCS.316.4

Formal models of the OSPF routing protocol

Jack Drury, Peter Höfner, Weiyou Wang

Research output: Contribution to journal › Conference article › peer-review

2 Citations (Scopus)

Abstract

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.

Original language	English
Pages (from-to)	72-120
Number of pages	49
Journal	Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume	316
DOIs	https://doi.org/10.4204/EPTCS.316.4
Publication status	Published - 26 Apr 2020
Event	4th Workshop on Models for Formal Analysis of Real Systems, MARS 2020 - Dublin, Ireland Duration: 26 Apr 2020 → …

Access to Document

10.4204/EPTCS.316.4

Cite this

@article{7b0f797fa1a44056810e1f04226fbf58,

title = "Formal models of the OSPF routing protocol",

abstract = "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.",

author = "Jack Drury and Peter H{\"o}fner and Weiyou Wang",

note = "Publisher Copyright: {\textcopyright} J. Drury, P. H{\"o}fner & W. Wang; 4th Workshop on Models for Formal Analysis of Real Systems, MARS 2020 ; Conference date: 26-04-2020",

year = "2020",

month = apr,

day = "26",

doi = "10.4204/EPTCS.316.4",

language = "English",

volume = "316",

pages = "72--120",

journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

issn = "2075-2180",

publisher = "Open Publishing Association",

}

TY - JOUR

T1 - Formal models of the OSPF routing protocol

AU - Drury, Jack

AU - Höfner, Peter

AU - Wang, Weiyou

N1 - Publisher Copyright: © J. Drury, P. Höfner & W. Wang

PY - 2020/4/26

Y1 - 2020/4/26

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85085709188&partnerID=8YFLogxK

U2 - 10.4204/EPTCS.316.4

DO - 10.4204/EPTCS.316.4

M3 - Conference article

AN - SCOPUS:85085709188

SN - 2075-2180

VL - 316

SP - 72

EP - 120

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

T2 - 4th Workshop on Models for Formal Analysis of Real Systems, MARS 2020

Y2 - 26 April 2020

ER -

Formal models of the OSPF routing protocol

Abstract

Access to Document

Other files and links

Fingerprint

Cite this